Quantitative Evaluation of Systems, International Conference on (2009)

Budapest, Hungary

Sept. 13, 2009 to Sept. 16, 2009

ISBN: 978-0-7695-3808-2

pp: 11-20

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2009.17

ABSTRACT

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.

INDEX TERMS

bisimulation, nondeterminism, measurable, logical characterization

CITATION

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.

doi:10.1109/QEST.2009.17

CITATIONS

SEARCH