Fair Equivalence Relations

10 years 9 months ago
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 B¨uchi condition is sufficiently strong (that is, a fair system that uses Rabin or Streett fairness can be translated to an equivalent B¨uchi 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: © bisimulation, game-bisimulation, and  -bisimulation. We show that while gamebisimulation and  -bisimulation have the same expressiveness hierarc...
Orna Kupferman, Nir Piterman, Moshe Y. Vardi
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Authors Orna Kupferman, Nir Piterman, Moshe Y. Vardi
Comments (0)