Partial Order Reduction for Probabilistic Branching Time

TitlePartial Order Reduction for Probabilistic Branching Time
Publication TypeJournal Article
Year of Publication2006
AuthorsBaier, C, D'Argenio, PR, Größer, M
JournalElectr. Notes Theor. Comput. Sci.
AbstractIn 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.
PDF (Full text): 
Powered by Drupal