Published by the Department of Computer Science, The University of Chicago.

Abstract

We extend the notion of bisimulation to Kripke structures with fairness. We define equivalences that preserve fairness and are akin to bisimulation. Specifically we define an equivalence and show that it is complete in the sense that it is the coarsest equivalence that preserves the logic CTL* interpreted with respect to the fair paths. The addition of fairness might cause two Kripke structures, which can be distinguished by a CTL* formula, to become indistinguishable by any CTL formula. We define a weaker equivalence that is the weakest equivalence preserving CTL interpreted on the fair paths. As a consequence of our proofs, we also obtain characterizations of states in the fair structure in terms of CTL* and CTL formulae.

• Preformatted versions of the article
  • DVI (75,012 bytes)
  • PostScript (401,036 bytes)
  • PDF (177,735 bytes)
  • Audio by AsTeR (to appear)
• Source materials for custom formatting
  • LaTeX (cj99-12.tex, 53,663 bytes)
  • BIBTeX (cj99-12.bib, 188,969 bytes)
  • Parameter settings for custom formatting (cjropts.tex, 165 bytes)
  • Self citation in BIBTeX (294 bytes)
• Online discussion
• Instructions for Readers

DOI: 10.4086/cjtcs.1999.012

---

Article 11 Volume 2000, Article 1
Volume 1999 Published articles