Paper accepted at FoSSaCS 2014

Title: Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS Rules

Authors: Pedro R. D'Argenio, Daniel Gebler, Matias David Lee.

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 nondeterministic transition system specifications. The novelty in our approach is to employ multi-sorted algebras to axiomatize separately nondeterministic choice, probabilistic choice and their interactions. Furthermore, we generalize this method to axiomatize the strong and convex metric bisimulation distance of PTSS.

Powered by Drupal