Abstract
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 language | English |
---|---|
Title of host publication | CONCUR 2011 – Concurrency Theory : 22nd International Conference, CONCUR 2011 Aachen, Germany, September 6-9, 2011 Proceedings |
Volume | 6901 |
Publisher | Springer |
Publication date | 2011 |
Pages | 108-123 |
ISBN (Print) | 978-3-642-23216-9 |
ISBN (Electronic) | 978-3-642-23217-6 |
DOIs | |
Publication status | Published - 2011 |
Event | 22nd International Conference on Concurrency Theory - Aachen, Germany Duration: 5 Sept 2011 → 10 Sept 2011 Conference number: 22 http://concur2011.rwth-aachen.de/ |
Conference
Conference | 22nd International Conference on Concurrency Theory |
---|---|
Number | 22 |
Country/Territory | Germany |
City | Aachen |
Period | 05/09/2011 → 10/09/2011 |
Internet address |
Series | Lecture Notes in Computer Science |
---|---|
Number | 6901 |
ISSN | 0302-9743 |