Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization

TitleNondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization
Publication TypeConference Paper
Year of Publication2009
AuthorsD'Argenio, PR, Wolovick, N, Sánchez Terraf, P, Celayes, P
Conference NameQEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems
PublisherIEEE Computer Society
ISBN Number978-0-7695-3808-2
AbstractWe 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.
PDF (Full text): 
Powered by Drupal