a1 FaMAF, Universidad Nacional de Córdoba and CONICET, Medina Allende s/n (Ciudad Universitaria), X5000HUA – Córdoba, Argentina Email: firstname.lastname@example.org
a2 FaMAF, Universidad Nacional de Córdoba, CONICET and CIEM, Medina Allende s/n (Ciudad Universitaria), X5000HUA – Córdoba, Argentina Email: email@example.com
a3 FaMAF, Universidad Nacional de Córdoba, Medina Allende s/n (Ciudad Universitaria), X5000HUA – Córdoba, Argentina Email: firstname.lastname@example.org
We extend the theory of labelled Markov processes to include internal non-determinism, which is a fundamental concept for the further development of a process theory with abstraction on non-deterministic continuous probabilistic systems. We define non-deterministic labelled Markov processes (NLMP) and provide three definitions of bisimulations: a bisimulation following a traditional characterisation; a state-based bisimulation tailored to our ‘measurable’ non-determinism; and an event-based bisimulation. We show the relations between them, including the fact that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy–Milner logic that characterises event bisimulation and is sound with respect to the other bisimulations for an arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable . We then introduce a finitary sublogic that characterises all bisimulations for an image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all the notions of bisimulation we consider turn out to be equal. Finally, we show that all these bisimulation notions are different in the general case. The counterexamples that separate them turn out to be non-probabilistic NLMPs.
(Received May 28 2010)
(Revised April 25 2011)
(Online publication September 26 2011)
† Supported by ANPCyT PICT 26135, ANPCyT PICT-PAE 2272, SeCyT-UNC and CONICET.