Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization
| Title | Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization |
| Publication Type | Conference Paper |
| Year of Publication | 2009 |
| Authors | D'Argenio, PR, Wolovick, N, Sánchez Terraf, P, Celayes, P |
| Conference Name | QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems |
| Publisher | IEEE Computer Society |
| ISBN Number | 978-0-7695-3808-2 |
| 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. |
| DOI | 10.1109/QEST.2009.17 |
PDF (Full text):
