Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games

We tackle the problem of non robustness of simulation and bisimulation when dealing with probabilistic processes. It is important to ignore tiny deviations in probabilities because these often come from experience or estimations. A few approaches have been proposed to treat this issue, for example metrics to quantify the non bisimilarity (or closeness) of processes. Relaxing the definition of simulation and bisimulation is another avenue which we follow. We define a new semantics to a known simple logic for probabilistic processes and show that it characterises a notion of -simulation. We also define two-players games that correspond to these notions: the existence of a winning strategy for one of the players determines -(bi)simulation. Of course, for all the notions defined, letting = 0 gives back the usual notions of logical equivalence, simulation and bisimulation. However, in contrast to what happens when = 0, two-way -simulation for > 0 is not equal to bisimulation. Next w...

• Type: Conference
• Year: 2008
• Where: QEST
• Authors: Josée Desharnais, François Laviolette, Mathieu Tracol
• Keywords: Bisimulation, Non Robustness, Probabilistic Processes, QEST 2008, Quantitative Evaluation Of Systems