Please use this identifier to cite or link to this item: doi:10.22028/D291-25903
Title: Model checking with abstraction refinement for well-structured systems
Author(s): Dimitrova, Rayana
Language: English
Year of Publication: 2006
SWD key words: Abstraktion
Unendlicher Zustandsraum
Free key words: abstraction
infinite-state system
DDC notations: 004 Computer science, internet
Publikation type: Other
Abstract: Abstraction plays an important role in the verification of infinite-state systems. One of the most promising and popular abstraction techniques is predicate abstraction. The right abstraction, i.e. the one that is sufficiently precise to prove or disprove the property under consideration, is automatically constructed by iterative abstraction refinement. The abstract-check-refine loop is not guaranteed to terminate in general. This results in the construction of semi-algorithms that may not terminate on some inputs. For the class of well-structured transition systems, a large class of infinitestate systems, general decidability results hold. These are transition systems equipped with a well-quasi ordering on the set of states which is compatible with the transition relation. In particular coverability, i.e. reachability of an upward-closed set, is known to be decidable for this class of systems. In this work we study the verification of well-structured systems w.r.t. the coverability property by means of predicate abstraction and refinement. We investigate the conditions under which the abstract-check-refine loop is guaranteed to terminate on instances of this class, provide a model checking method based on predicate abstraction and abstraction refinement and prove its completeness for this class of systems.
nicht vorhanden
Link to this record: urn:nbn:de:bsz:291-scidok-13339
Date of registration: 16-Nov-2007
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
Diplomarbeit_9772_Dimi_Raya_2006.pdf418,35 kBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.