Quantitative Evaluation of Systems, International Conference on (2009)
Sept. 13, 2009 to Sept. 16, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2009.17
We extend the theory of labeled Markov processeswith internal nondeterminism, a fundamental conceptfor the further development of a process theory withabstraction on nondeterministic continuous probabilisticsystems. We define nondeterministic labeled Markovprocesses (NLMP) and provide both a state basedbisimulation and an event based bisimulation. We showthe relation between them, including that the largeststate bisimulation is also an event bisimulation. Wealso introduce a variation of the Hennessy-Milnerlogic that characterizes event bisimulation and that issound w.r.t. the state base bisimulation for arbitraryNLMP. This logic, however, is infinitary as it containsa denumerable ∨. We then introduce a finitary sublogicthat characterize both state and event bisimulation forimage finite NLMP whose underlying measure spaceis also analytic. Hence, in this setting, all notions ofbisimulation we deal with turn out to be equal.
bisimulation, nondeterminism, measurable, logical characterization
N. Wolovick, P. Celayes, P. S. Terraf and P. R. D'Argenio, "Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization," Quantitative Evaluation of Systems, International Conference on(QEST), Budapest, Hungary, 2009, pp. 11-20.