Partial Order Reduction in Directed Model Checking

Alberto Lluch Lafuente, Stefan Leue, Stefan Edelkamp

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Partial order reduction is a very succesful technique for avoiding the state explosion problem that is inherent to explicit state model checking of asynchronous concurrent systems. It exploits the commutativity of concurrently executed transitions in interleaved system runs in order to reduce the size of the explored state space. Directed model checking on the other hand addresses the state explosion problem by using guided search techniques during state space exploration. As a consequence, shorter errors trails are found and less search effort is required than when using standard depth-first or breadth-first search. We analyze how to combine directed model checking with partial order reduction methods and give experimental results on how the combination of both techniques performs.
Original languageEnglish
Title of host publicationModel Checking Software : 9th International SPIN Workshop Grenoble, France, April 11–13, 2002 Proceedings
Publication date2002
Pages95-138
ISBN (Print)978-3-540-43477-1
ISBN (Electronic)978-3-540-46017-6
DOIs
Publication statusPublished - 2002
Externally publishedYes
Event9th International SPIN Workshop on Model Checking Software - Grenoble, France
Duration: 11 Apr 200213 Apr 2002
Conference number: 9

Conference

Conference9th International SPIN Workshop on Model Checking Software
Number9
CountryFrance
CityGrenoble
Period11/04/200213/04/2002
SeriesLecture Notes in Computer Science
Volume2318
ISSN0302-9743

Fingerprint Dive into the research topics of 'Partial Order Reduction in Directed Model Checking'. Together they form a unique fingerprint.

Cite this