*
Thomas A. Henzinger,
Orna Kupferman, and Sriram K. Rajamani*

The simulation preorder for labeled transition systems is defined
locally, and operationally, as a game that relates states with their
immediate successor states. Simulation enjoys many appealing
properties. First, simulation has a denotational characterization:
system *S* simulates system *I* iff every computation tree
embedded in the unrolling of *I* can be embedded also in the
unrolling of *S*. Second, simulation has a logical
characterization: *S* simulates *I* iff every universal
branching-time formula satisfied by *S* is satisfied also by
*I*. It follows that simulation is a suitable notion of
implementation, and it is the coarsest abstraction of a system that
preserves universal branching-time properties. Third, based on its
local definition, simulation between finite-state systems can be
checked in polynomial time. Finally, simulation implies trace
containment, which cannot be defined locally and requires polynomial
space for verification. Hence simulation is widely used both in
manual and in automatic verification.

Liveness assumptions about transition systems are typically modeled
using fairness constraints. Existing notions of simulation for fair
transition systems, however, are not local, and as a result, many
appealing properties of the simulation preorder are lost. We propose
a new view of fair simulation by extending the local definition of
simulation to account for fairness: system *S* *fairly
simulates* system *I* iff in the simulation game, there is a
strategy that matches with each fair computation of *I* a fair
computation of *S*. Our definition enjoys a denotational
characterization and has a logical characterization: *S* fairly
simulates *I* iff every fair computation tree (whose infinite
paths are fair) embedded in the unrolling of *I* can be embedded
also in the unrolling of *S* or, equivalently, iff every Fair-UAM
formula satisfied by *S* is satisfied also by *I* (UAM is
the universal fragment of the alternation-free mu-calculus). The
locality of the definition leads us to a polynomial-time algorithm for
checking fair simulation for finite-state systems with weak and strong
fairness constraints. Finally, fair simulation implies fair trace
containment, and is therefore useful as an efficiently-computable
local criterion for proving linear-time abstraction hierarchies of
fair systems.

*Information and Computation* 173:64-81, 2002.
A preliminary version appeared in the
*Proceedings of the
Ninth International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 1243,
Springer, 1997, pp. 273-287.

Download inofficial, sometimes updated PostScript / PDF document. © 1997 Springer, 2002 Academic Press.