Jeudi 19 janvier, 11h salle 1D23

Silvia Crafa (Padua)

A spectrum of behavioral relations over LTSs on probability distributions

Abstract: Probabilistic nondeterministic processes are commonly modeled as probabilistic LTSs (PLTSs, a.k.a. probabilistic automata). A number of logical characterizations of the main behavioral relations on PLTSs have been studied. In particular, Parma and Segala define a probabilistic Hennessy-Milner logic interpreted over distributions, whose logical equivalence/preorder when re- stricted to Dirac distributions coincide with standard bisimulation/simulation be- tween the states of a PLTS. This result is here extended by studying the full log- ical equivalence/preorder between distributions in terms of a notion of bisimula- tion/simulation defined on a LTS of probability distributions (DLTS). We show that the standard spectrum of behavioral relations on nonprobabilistic LTSs as well as its logical characterization in terms of Hennessy-Milner logic scales to the probabilistic setting when considering DLTSs. It is joint work with Francesco Ranzato, presented at CONCUR 2011