Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-25903
Titel: | Model checking with abstraction refinement for well-structured systems |
VerfasserIn: | Dimitrova, Rayana |
Sprache: | Englisch |
Erscheinungsjahr: | 2006 |
Kontrollierte Schlagwörter: | Abstraktion Unendlicher Zustandsraum Verifikation |
Freie Schlagwörter: | abstraction verification infinite-state system |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Sonstiges |
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 zu diesem Datensatz: | urn:nbn:de:bsz:291-scidok-13339 hdl:20.500.11880/25959 http://dx.doi.org/10.22028/D291-25903 |
Datum des Eintrags: | 16-Nov-2007 |
Fakultät: | MI - Fakultät für Mathematik und Informatik |
Fachrichtung: | MI - Informatik |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
Diplomarbeit_9772_Dimi_Raya_2006.pdf | 418,35 kB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.