D’Argenio, Pedro R.; Sánchez Terraf, Pedro; Wolovick, Nicolás Bisimulations for non-deterministic labelled Markov processes. (English) Zbl 1234.68316 Math. Struct. Comput. Sci. 22, No. 1, 43-68 (2012). Summary: 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 \(\vee\). 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. Cited in 9 Documents MSC: 68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 60J25 Continuous-time Markov processes on general state spaces Keywords:bisimulations; Markov processes; internal non-determinism; Hennessy-Milner logic; non-deterministic labelled Markov processes Software:MoDeST PDFBibTeX XMLCite \textit{P. R. D'Argenio} et al., Math. Struct. Comput. Sci. 22, No. 1, 43--68 (2012; Zbl 1234.68316) Full Text: DOI arXiv References: [1] van Glabeek, Handbook of Process Algebra pp 3– (2001) [2] DOI: 10.1007/978-1-4612-4190-4 [3] DOI: 10.1006/inco.2001.2962 · Zbl 1096.68103 [4] DOI: 10.1016/S1567-8326(02)00068-1 · Zbl 1053.68065 [5] Clarke, Model Checking (1999) [6] DOI: 10.1109/QEST.2009.17 [7] Cattani, Springer-Verlag Lecture Notes in Computer Science 3441 pp 125– (2005) [8] DOI: 10.1016/j.ic.2005.07.002 · Zbl 1106.68073 [9] DOI: 10.1016/j.ic.2005.02.004 · Zbl 1110.68083 [10] Bravetti, Springer-Verlag Lecture Notes in Computer Science 2925 pp 44– (2004) [11] DOI: 10.1109/TSE.2006.104 · Zbl 05341944 [12] Billingsley, Probability and Measure (1995) [13] Vardi, Proceedings 26th FOCS pp 327– (1985) [14] Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming (1994) · Zbl 0829.90134 [15] Parma, Springer-Verlag Lecture Notes in Computer Science 4423 pp 287– (2007) · Zbl 1195.68072 [16] Naimpally, Topological Commentary 8 (2003) [17] Milner, Communication and Concurrency (1989) [18] DOI: 10.1016/0890-5401(91)90030-6 · Zbl 0756.68035 [19] Giry, Springer-Verlag Lecture Notes in Mathematics 915 pp 68– (1981) This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.