Nov 20, 2012: Daniel Gebler: Compositionality of Strict and Approximate Behavioral Equivalences in Probabilistic Transition System Specifications

November 20, 2012Compositionality of Strict and Approximate Behavioral Equivalences in Probabilistic Transition System Specifications
Room: Zi 5126Daniel Gebler
12:30-13:30

We present a Plotkin style SOS specification format for Segala-type probabilistic transition systems that guarantees that probabilistic bisimilarity is a congruence for any operator defined in this format. For many practical applications probabilistic bisimilarity is too sensitive to the exact probabilities of transitions and thus a slight perturbation of the probabilities would make two systems non-bisimilar. ε-bisimilarity relaxes probabilistic bisimilarity by allowing that related states evolve into related sets of states for which the probabilistic mass may differ up to ε. We provide an appropriate SOS specification rule format that guarantees that ε-bisimilarity is compositional. Furthermore we present a method to decompose probabilsitic HML formulae which allows to derive systematically SOS specification formats for any logically characterized behavioral relation.

(Slides are available here: http://www.few.vu.nl/~gebler/)