Bisimulations meet PCTL equivalences for probabilistic automata

Research output: Contribution to journalJournal article – Annual report year: 2013Researchpeer-review

View graph of relations

Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL*. Various behavioral equivalences are proposed, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the equivalences are well-known to be sound, but not complete with respect to the logical equivalences induced by PCTL or PCTL*. The desire of a both sound and complete behavioral equivalence has been pointed out by Segala in [34], but remains open throughout the years. In this paper we introduce novel notions of strong bisimulation relations, which characterize PCTL and PCTL* exactly. We extend weak bisimulations that characterize PCTL and PCTL* without next operator, respectively. Further, we also extend the framework to simulation preorders. Thus, our paper bridges the gap between logical and behavioral equivalences and preorders in this setting.
Original languageEnglish
Article number7
JournalLogical Methods in Computer Science
Volume9
Issue number2
Number of pages34
ISSN1860-5974
DOIs
Publication statusPublished - 2013

Bibliographical note

The article is licensed under a Creative Commons license.

CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

  • Bioinformatics, Computational efficiency, Model checking, Fault tolerance

Download statistics

No data available

ID: 56434574