Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2011

View graph of relations

Probabilistic automata (PA) [20] have been successfully applied in the 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 PCTL [11] and its extension PCTL∗ [4]. Various behavioral equivalences are proposed for PAs, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the behavioral equivalences are well-known to be strictly stronger than the logical equivalences induced by PCTL or PCTL∗. This paper introduces novel notions of strong bisimulation relations, which characterizes PCTL and PCTL∗ exactly.We also extend weak bisimulations characterizing PCTL and PCTL∗ without next operator, respectively. Thus, our paper bridges the gap between logical and behavioral equivalences in this setting.
Original languageEnglish
Title of host publicationCONCUR 2011 – Concurrency Theory : 22nd International Conference, CONCUR 2011 Aachen, Germany, September 6-9, 2011 Proceedings
Volume6901
PublisherSpringer
Publication date2011
Pages108-123
ISBN (print)978-3-642-23216-9
ISBN (electronic)978-3-642-23217-6
DOIs
StatePublished

Conference

Conference22nd International Conference on Concurrency Theory
Number22
CountryGermany
CityAachen
Period05/09/1110/09/11
Internet addresshttp://concur2011.rwth-aachen.de/
NameLecture Notes in Computer Science
Number6901
ISSN (Print)0302-9743
CitationsWeb of Science® Times Cited: No match on DOI
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

ID: 6305741