Symmetry Reduction and Heuristic Search for Error Detection in Model Checking

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

Abstract

The state explosion problem is the main limitation of model checking. Symmetries in the system being verified can be exploited in order to avoid this problem by defining an equivalence (symmetry) relation on the states of the system, which induces a semantically equivalent quotient system of smaller size. On the other hand, heuristic search algorithms can be applied to improve the bug finding capabilities of model checking. Such algorithms use
heuristic functions to guide the exploration. Bestfirst
is used for accelerating the search, while A* guarantees optimal error trails if combined with admissible estimates. We analyze some aspects of combining both approaches, concentrating on the problem of finding the optimal path to the equivalence class of a given error state. Experimental
results evaluate our approach.
Original languageEnglish
Title of host publicationProceedings of the 2nd Workshop on Model Checking and Artificial Intelligence
PublisherAAAI Press
Publication date2003
Publication statusPublished - 2003
Externally publishedYes
Event2nd Workshop on Model Checking and Artificial Intelligence - Acapulco, Mexico
Duration: 10 Aug 2003 → …
Conference number: 2

Conference

Conference2nd Workshop on Model Checking and Artificial Intelligence
Number2
CountryMexico
CityAcapulco
Period10/08/2003 → …

Fingerprint Dive into the research topics of 'Symmetry Reduction and Heuristic Search for Error Detection in Model Checking'. Together they form a unique fingerprint.

Cite this