Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Lei Song; Lijun Zhang; Jens Christian Godskesen

doi:10.1007/978-3-642-23217-6_8

Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Lei Song, Lijun Zhang, Jens Christian Godskesen

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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 language	English
Title of host publication	CONCUR'11 Proceedings of the 22nd international conference on Concurrency theory
Number of pages	15
Publisher	Springer
Publication date	5 Sep 2011
Pages	108-123
ISBN (Print)	978-3-642-23216-9
DOIs	https://doi.org/10.1007/978-3-642-23217-6_8
Publication status	Published - 5 Sep 2011
Event	22nd International Conference on Concurrency Theory 2011 (CONCUR 2011) - Aachen, Germany Duration: 5 Sep 2011 → 10 Sep 2011 Conference number: 22nd http://concur2011.rwth-aachen.de/

Conference

Conference	22nd International Conference on Concurrency Theory 2011 (CONCUR 2011)
Number	22nd
Country/Territory	Germany
City	Aachen
Period	05/09/2011 → 10/09/2011
Internet address	http://concur2011.rwth-aachen.de/

Access to Document

10.1007/978-3-642-23217-6_8

Bisimulations Meet PCTL Equivalences for Probabilistic AutomataAccepted author manuscript, 343 KB

http://dx.doi.org/10.1007/978-3-642-23217-6_8

Cite this

@inproceedings{8e478ad1a0764bbebf0eaef07b0365c5,

title = "Bisimulations Meet PCTL Equivalences for Probabilistic Automata",

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.",

author = "Lei Song and Lijun Zhang and Godskesen, {Jens Christian}",

year = "2011",

month = sep,

day = "5",

doi = "10.1007/978-3-642-23217-6_8",

language = "English",

isbn = "978-3-642-23216-9 ",

pages = "108--123",

booktitle = "CONCUR'11 Proceedings of the 22nd international conference on Concurrency theory",

publisher = "Springer",

address = "Germany",

note = "22nd International Conference on Concurrency Theory 2011 (CONCUR 2011), CONCUR 2011 ; Conference date: 05-09-2011 Through 10-09-2011",

url = "http://concur2011.rwth-aachen.de/",

}

TY - GEN

T1 - Bisimulations Meet PCTL Equivalences for Probabilistic Automata

AU - Song, Lei

AU - Zhang, Lijun

AU - Godskesen, Jens Christian

N1 - Conference code: 22nd

PY - 2011/9/5

Y1 - 2011/9/5

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-23217-6_8

DO - 10.1007/978-3-642-23217-6_8

M3 - Article in proceedings

SN - 978-3-642-23216-9

SP - 108

EP - 123

BT - CONCUR'11 Proceedings of the 22nd international conference on Concurrency theory

PB - Springer

T2 - 22nd International Conference on Concurrency Theory 2011 (CONCUR 2011)

Y2 - 5 September 2011 through 10 September 2011

ER -

Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Abstract

Conference

Access to Document

Fingerprint

Cite this