Fair Simulation
---------------

The simulation preorder for labeled transition systems is defined
locally as a game that relates states with their immediate successor
states. 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 extend 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 fully abstract semantics and has a logical 
characterization: 
S fairly simulates I iff every fair computation tree embedded in the 
unrolling of I can be embedded also in the unrolling of S or, 
equivalently, iff every Fair-Universal-Alternation-Free Mu-Calculus
formula satisfied by I is satisfied also by S.
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.