Fair Equivalence Relations
Equivalence between designs is a fundamental notion in verification.
The linear and branching approaches to verification induce different
notions of equivalence. When the designs are modeled by fair
state-transition systems, equivalence in the linear paradigm
corresponds to fair trace equivalence, and in the branching paradigm
corresponds to fair bisimulation.
In this work we study the expressive power of various types of
fairness conditions. For the linear paradigm, it is known that the
Buchi condition is sufficiently strong (that is, a fair system that
uses Rabin or Streett fairness can be translated to an equivalent
Buchi system). We show that in the branching paradigm the
expressiveness hierarchy depends on the types of fair bisimulation one
chooses to use. We consider three types of fair bisimulation studied
in the literature: \exists-bisimulation, game-bisimulation, and
\forall-bisimulation. We show that while game-bisimulation and
\forall-bisimulation have the same expressiveness hierarchy as tree
automata, \exists-bisimulation induces a different hierarchy. This
hierarchy lies between the hierarchies of word and tree automata, and
it collapses at Rabin conditions of index one, and Streett conditions
of index two.
@inproceedings{KPV00,
author = "O. Kupferman and N. Piterman and M.Y. Vardi",
title = "Fair Equivalence Relations",
booktitle = "Proc. 20th Conference on the foundations of
software technology and theoretical computer
science",
series = "Lecture Notes in Computer Science",
volume = 1974,
pages = "151-163",
month = "December",
year = 2000
}
PDF