
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.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Probability in computer science (algorithm analysis, random structures, phase transitions, etc.), Hennessy-Milner logic, Markov processes, G.3, PROCESS SEMANTICS, internal non-determinism, Logic in Computer Science (cs.LO), non-deterministic labelled Markov processes, CONTINUOUS PROBABILITY, BISIMULATION, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), Continuous-time Markov processes on general state spaces, F.4.1, https://purl.org/becyt/ford/1.2, 60Jxx, bisimulations, G.3; F.4.1, https://purl.org/becyt/ford/1, MEASURE THEORY
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Probability in computer science (algorithm analysis, random structures, phase transitions, etc.), Hennessy-Milner logic, Markov processes, G.3, PROCESS SEMANTICS, internal non-determinism, Logic in Computer Science (cs.LO), non-deterministic labelled Markov processes, CONTINUOUS PROBABILITY, BISIMULATION, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), Continuous-time Markov processes on general state spaces, F.4.1, https://purl.org/becyt/ford/1.2, 60Jxx, bisimulations, G.3; F.4.1, https://purl.org/becyt/ford/1, MEASURE THEORY
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 22 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
