Partial Order Reduction for Probabilistic Branching Time

Producción CyT

Artículo

Autoría

Christel Baier ; D'ARGENIO, PEDRO RUBEN ; Marcus Größer

Fecha

2006

Editorial y Lugar de Edición

ELSEVIER SCIENCE BV

Revista

Electronic Notes in Theoretical Computer Science, vol. 153 (pp. 97-116) - ISSN 1571-0661
ELSEVIER SCIENCE BV

ISSN

1571-0661

Resumen Información suministrada por el agente en SIGEVA

In the past, partial order reduction has been used successfully to combat the state explosion problem in the context of model checking for non-probabilistic systems. For both linear time and branching time specifications, methods have been developed to apply partial order reduction in the context of model checking. Only recently, results were published that give criteria on applying partial order reduction for verifying quantitative linear time properties for probabilistic systems. This paper p... In the past, partial order reduction has been used successfully to combat the state explosion problem in the context of model checking for non-probabilistic systems. For both linear time and branching time specifications, methods have been developed to apply partial order reduction in the context of model checking. Only recently, results were published that give criteria on applying partial order reduction for verifying quantitative linear time properties for probabilistic systems. This paper presents partial order reduction criteria for Markov decision processes and branching time properties, such as formulas of probabilistic computation tree logic. Moreover, we provide a comparison of the results established so far about reduction conditions for Markov decision processes.

Ver más Ver menos

Palabras Clave

PARTIAL ORDEN REDUCTIONPROBABILISTIC MODEL CHECKING