Sonja Georgievska (Eindhoven University of Technologies, The Netherlands)

 

Retaining the Probabilities in Probabilistic Testing Theory

 

The may/must testing theory for concurrent processes is based on the criterion that two processes are equivalent if and only if they cannot be distinguished when interacting with their environment, which is an arbitrary process itself.  The present work considers the probabilistic may/must testing theory for processes having external, internal, and probabilistic choice. We observe that the underlying testing equivalence is too strong and distinguishes between processes that are observationally equivalent. The problem arises from an observation that the classical compose-and-schedule approach yields unrealistic overestimation of the probabilities, a phenomenon that has been recently well studied from the point of view of compositionality (de Alfaro/Henzinger/Jhala 2001, Cheung/Lynch/Segala/Vaandrager 2006), in the context of randomized protocols (Chatzikokolakis/Palamidessi 2007), and in probabilistic model checking (Giro/D'Argenio/Ferrer Fioriti 2009). To that end, we propose a new testing semantics, aiming at preserving the probability information in a parallel context. The resulting testing equivalence is insensitive to the exact moment of occurring of the internal and probabilistic choices. We also give an alternative characterization of the testing preorder as a probabilistic ready-trace preorder.