Specification and verification of timed lazy systems

Abstract

In this paper CCS is equipped with a simple operational semantics that allows us to describe and reason about the performance of systems which proceed by reacting to external stimuli. Based on the new operational semantics, lazy performance equivalence is introduced as a natural extension of the standard interleaving bisimulation. It turns out to be preserved by all CCS contexts. The problem of automatically checking lazy performance equivalence is also tackled. Because of the lazy character of our calculus, an infinite transition graph is associated with every non-trivial CCS term. Nevertheless, lazy performance equivalence can be provided with an alternative finite characterization and existing algorithms for checking bisimulation based semantics can be applied to the latter.