Speaker: Sonja Georgievska and Nikola Trcka (FM, TU/e)
Title: Branching bisimulation congruence for probabilistic

Abstract:
(Labelled) transition systems are a well established formalism for
the modelling of qualitative aspects of systems. A transition system
is a directed graph in which nodes represent states of the system,
and labels on arrows represent the actions that the system can
perform when going from one state to another. In the setting with
the internal action tau the main equivalence on transition systems
is branching bisimulation. To model quantitative behaviour
transition systems are extended to probabilistic transition systems
that include special states in which the next state is chosen
randomly. We show that the existing notion of branching bisimulation
for probabilistic transition systems is not compatible with parallel
composition and present an adaptation that is a congruence relation,
i.e. compatible with all the operators.