Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS Rules
| Title | Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS Rules |
| Publication Type | Book Chapter |
| Year of Publication | 2014 |
| Authors | D'Argenio, PR, Gebler, D, Lee, MD |
| Editor | Muscholl, A |
| Book Title | Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings |
| Series Title | Lecture Notes in Computer Science |
| Volume | 8412 |
| Publisher | Springer |
| ISBN Number | 978-3-642-54829-1 |
| Abstract | Probabilistic transition system specifications (PTSS) provide structural operational semantics for reactive probabilistic labeled transition systems. Bisimulation equivalences and bisimulation metrics are fundamental notions to describe behavioral relations and distances of states, respectively. We provide a method to generate from a PTSS a sound and ground-complete equational axiomatization for strong and convex bisimilarity. The construction is based on the method of Aceto, Bloom and Vaandrager developed for non-deterministic transition system specifications. The novelty in our approach is to employ many-sorted algebras to axiomatize separately non-deterministic choice, probabilistic choice and their interaction. Furthermore, we generalize this method to axiomatize the strong and convex metric bisimulation distance of PTSS. |
| DOI | 10.1007/978-3-642-54830-7_19 |
PDF (Full text):
