Abstract
A branching bisimulation for probabilistic systems that is preserved under parallel composition has been defined recently for the alternating model. We show that besides being compositional, it is decidable in polynomial time and it preserves the properties expressible in probabilistic Computation Tree Logic (pCTL). In the ground-complete axiomatization, only a single axiom is added to the axioms for strong bisimulation. We show that the Concurrent Alternating Bit protocol can be verified using the process algebra and a set of recursive rules. © Springer-Verlag Berlin Heidelberg 2009.
Cite
CITATION STYLE
Andova, S., & Georgievska, S. (2009). On compositionality, efficiency, and applicability of abstraction in probabilistic systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5404 LNCS, pp. 67–78). https://doi.org/10.1007/978-3-540-95891-8_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
