Science and Technology Production
Article
Authorship
Christel Baier
;
D'ARGENIO, PEDRO RUBEN
;
Marcus Größer
Date
2006
Publishing House and Editing Place
ELSEVIER SCIENCE BV
Magazine
Electronic Notes in Theoretical Computer Science,
vol. 153
(pp. 97-116)
- ISSN 1571-0661
ELSEVIER SCIENCE BV
ELSEVIER SCIENCE BV
ISSN
1571-0661
Summary
Information provided by the agent in
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.
Show more
Show less
Key Words
PARTIAL ORDEN REDUCTIONPROBABILISTIC MODEL CHECKING