Conference paper
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
IT University of Copenhagen1
Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark2
Department of Informatics and Mathematical Modeling, Technical University of Denmark3
Department of Information Technology, Technical University of Denmark4
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.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2011 |
| Pages: | 108-123 |
| Proceedings: | 22nd International Conference on Concurrency Theory |
| Series: | Lecture Notes in Computer Science |
| Journal subtitle: | 22nd International Conference, Concur 2011 Aachen, Germany, September 6-9, 2011 Proceedings |
| ISBN: | 3642232167 , 3642232175 , 9783642232169 and 9783642232176 |
| ISSN: | 16113349 and 03029743 |
| Types: | Conference paper |
| DOI: | 10.1007/978-3-642-23217-6_8 |
