Abstraction in Directed Model Checking

Stefan Edelkamp, Alberto Lluch Lafuente

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearch

Abstract

Abstraction is one of the most important issues to cope with large and infinite state spaces in model checking and to reduce the verification efforts. The abstract system is smaller than the original one and if the abstract system satisfies a correctness specification, so does the concrete one. However, abstractions may introduce a behavior violating the specification that is not present in the original system.
This paper bypasses this problem by proposing the combination of abstraction with heuristic search to improve error detection. The abstract system is explored in order to create a database that stores the exact distances from abstract states to the set of abstract error states. To check, whether or not the abstract behavior is present in the original system, effcient exploration algorithms exploit the database as a guidance.
Original languageEnglish
Title of host publicationProceedings of the 1st ICAPS Workshop on Connecting Planning Theory with Practice
Publication date2004
Publication statusPublished - 2004
Externally publishedYes
Event1st International Conference on Automated Planning and Scheduling Workshop on Connecting Planning Theory with Practice - Whistler, Canada
Duration: 3 Jun 20047 Jun 2004
Conference number: 1

Conference

Conference1st International Conference on Automated Planning and Scheduling Workshop on Connecting Planning Theory with Practice
Number1
CountryCanada
CityWhistler
Period03/06/200407/06/2004

Cite this