Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Lei Song, Lijun Zhang, Jens Christian Godskesen

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Abstract

Probabilistic automata (PA) have beensuccessfully applied in the formal verification of concurrent andstochastic systems. Efficient model checking algorithms have beenstudied, where the most often used logics for expressing propertiesare based on PCTL and its extensionPCTL*. Variousbehavioral equivalences are proposed for PAs, asa powerful tool for abstraction and compositional minimization forPAs. Unfortunately, the behavioral equivalencesare well-known to be strictly stronger than the logical equivalences inducedby PCTL or PCTL*. This paper introduces novel notions of strongbisimulation relations, which characterizes PCTL and PCTL*exactly. We also extend weak bisimulations characterizingPCTL and PCTL* without next operator, respectively. Thus, ourpaper bridges the gap between logical and behavioral equivalences inthis setting.

Original languageEnglish
Title of host publicationCONCUR'11 Proceedings of the 22nd international conference on Concurrency theory
Number of pages15
PublisherSpringer
Publication date5 Sept 2011
Pages108-123
ISBN (Print)978-3-642-23216-9
DOIs
Publication statusPublished - 5 Sept 2011
Event22nd International Conference on Concurrency Theory 2011 (CONCUR 2011) - Aachen, Germany
Duration: 5 Sept 201110 Sept 2011
Conference number: 22nd
http://concur2011.rwth-aachen.de/

Conference

Conference22nd International Conference on Concurrency Theory 2011 (CONCUR 2011)
Number22nd
Country/TerritoryGermany
CityAachen
Period05/09/201110/09/2011
Internet address

Fingerprint

Dive into the research topics of 'Bisimulations Meet PCTL Equivalences for Probabilistic Automata'. Together they form a unique fingerprint.

Cite this