Artículo
Bisimulations for non-deterministic labelled Markov processes
Fecha de publicación:
02/2012
Editorial:
Cambridge University Press
Revista:
Mathematical Structures In Computer Science
ISSN:
0960-1295
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
We extend the theory of labelled Markov processes to include internal non-determinism, which is a fundamental concept for the further development of a process theory with abstraction on non-deterministic continuous probabilistic systems. We define non-deterministic labelled Markov processes (NLMP) and provide three definitions of bisimulations: a bisimulation following a traditional characterisation; a state-based bisimulation tailored to our 'measurable' non-determinism; and an event-based bisimulation. We show the relations between them, including the fact that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy-Milner logic that characterises event bisimulation and is sound with respect to the other bisimulations for an arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable. We then introduce a finitary sublogic that characterises all bisimulations for an image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all the notions of bisimulation we consider turn out to be equal. Finally, we show that all these bisimulation notions are different in the general case. The counterexamples that separate them turn out to be non-probabilistic NLMPs.
Palabras clave:
PROCESS SEMANTICS
,
CONTINUOUS PROBABILITY
,
BISIMULATION
,
MEASURE THEORY
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(CCT - CORDOBA)
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Citación
D'argenio, Pedro Ruben; Sanchez Terraf, Pedro Octavio; Wolovick, Nicolás; Bisimulations for non-deterministic labelled Markov processes; Cambridge University Press; Mathematical Structures In Computer Science; 22; 1; 2-2012; 43-68
Compartir
Altmétricas