2010/11/15 by Pedro D'Argenio, Pedro R. D’Argenio, Pedro Sánchez Terraf +4
Computer Science · #60Jxx #Bayesian Modeling and Causal Inference #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #G.3 #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling #acm:60Jxx #cs.LO #msc:60Jxx
paper · pdf · doi:10.48550/arxiv.1011.3362
arxiv created 2010/11/15 · openalex publication_date 2010/11/15 · arxiv updated 2015/03/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We extend the theory of labeled Markov processes with internal nondeterminism, a fundamental concept for the further development of a process theory with abstraction on nondeterministic continuous probabilistic systems. We define nondeterministic labeled Markov processes (NLMP) and provide three definition of bisimulations: a bisimulation following a traditional characterization, a state based bisimulation tailored to our "measurable" non-determinism, and an event based bisimulation. We show the relation between them, including that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy-Milner logic that characterizes event bisimulation and that is sound w.r.t. the other bisimulations for arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable ∨. We then introduce a finitary sublogic that characterize all bisimulations for image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all notions of bisimulation we deal with turn out to be equal. Finally, we show that all notions of bisimulations are different in the general case. The counterexamples that separate them turn to be non-probabilistic NLMP.