## Fair Bisimulation

*
Thomas A. Henzinger
and Sriram K. Rajamani*

Bisimulations enjoy numerous applications in the analysis of labeled
transition systems. Many of these applications are based on two central
observations: first, bisimilar systems satisfy the same branching-time
properties; second, bisimilarity can be checked efficiently for finite-state
systems. The local character of bisimulation, however, makes it difficult to
address liveness concerns. Indeed, the definitions of fair bisimulation that
have been proposed in the literature sacrifice locality, and with it, also
efficient checkability. We put forward a new definition of fair bisimulation
which does not suffer from this drawback.

The bisimilarity of two systems can be viewed in terms of a game played
between a protagonist and an adversary. In each step of the infinite
bisimulation game, the adversary chooses one system, makes a move, and the
protagonist matches it with a move of the other system. Consistent with this
game-based view, we call two fair transition systems bisimilar if in the
bisimulation game, the infinite path produced in the first system is fair iff
the infinite path produced in the second system is fair.

We show that this notion of fair bisimulation enjoys the following
properties. First, fairly bisimilar systems satisfy the same formulas of the
logics Fair-AFMC (the fair alternation-free mu-calculus) and Fair-CTL*.
Therefore, fair bisimulations can serve as property-preserving abstractions
for these logics and weaker ones, such as Fair-CTL and LTL. Indeed,
Fair-AFMC provides an exact logical characterization of fair bisimilarity.
Second, it can be checked in time polynomial in the number of states if two
systems are fairly bisimilar. This is in stark contrast to all trace-based
equivalences, which are traditionally used for addressing liveness but
require exponential time for checking.

*Proceedings of the
Sixth International Conference on Tools and Algorithms for the
Construction and Analysis of Systems*
(TACAS),
Lecture Notes in Computer Science 1785,
Springer, 2000, pp. 299-314.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2000 Springer.