Campus Event Calendar
Event Entry
What and Who
Model Checking with Abstraction Refinement for Well-structured Systems
Rayna Dimitrova
IMPRS
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 10 July 2006
08:30
330 Minutes
E1 4
024
Saarbrücken
Abstract
Predicate abstraction is a technique used for verification of
infinite-state systems. Methods for automatic construction of a
sufficiently precise abstraction are in general incomplete. Therefore, it
is worth identifying classes of systems for which iterative predicate
refinement is guaranteed to converge.
We study the class of well-structured transition systems, which is a
large class that contains many infinite-state models used in practice.
These are systems, for which a well-quasi ordering on the set of states
that is compatible with the transition relation exists. We consider two
classes: WSTS (well-structured transition systems) and WSLTS
(well-structured labeled transition systems), which differ in the notion
of compatibility, and we focus on the coverability problem - checking
reachability of an upward-closed set of error states. We present two
instantiations of the standard schema for forward abstract reachability
analysis with predicate refinement. One of them uses the classical
refinement based on computation of predecessors and we prove completeness
for WSLTS, which is a proper extension of the class of systems with finite
trace-equivalence for which this refinement is known to be complete. For
the more general class of WSTS we propose a new refinement operator and
prove completeness of the method for this class. Our main result is the
completeness of predicate abstraction refinement for these two classes.
The advantage of this approach for checking coverability for
well-structured systems is that not only the reachability analysis is
forward, but also the refinement is performed locally and takes into
account the abstract counterexample.
infinite-state systems. Methods for automatic construction of a
sufficiently precise abstraction are in general incomplete. Therefore, it
is worth identifying classes of systems for which iterative predicate
refinement is guaranteed to converge.
We study the class of well-structured transition systems, which is a
large class that contains many infinite-state models used in practice.
These are systems, for which a well-quasi ordering on the set of states
that is compatible with the transition relation exists. We consider two
classes: WSTS (well-structured transition systems) and WSLTS
(well-structured labeled transition systems), which differ in the notion
of compatibility, and we focus on the coverability problem - checking
reachability of an upward-closed set of error states. We present two
instantiations of the standard schema for forward abstract reachability
analysis with predicate refinement. One of them uses the classical
refinement based on computation of predecessors and we prove completeness
for WSLTS, which is a proper extension of the class of systems with finite
trace-equivalence for which this refinement is known to be complete. For
the more general class of WSTS we propose a new refinement operator and
prove completeness of the method for this class. Our main result is the
completeness of predicate abstraction refinement for these two classes.
The advantage of this approach for checking coverability for
well-structured systems is that not only the reachability analysis is
forward, but also the refinement is performed locally and takes into
account the abstract counterexample.
Contact
Kerstin Kathy Meyer-Ross
226
--email hidden
passcode not visible
logged in users only
Jennifer Gerling, 07/03/2006 09:25
Jennifer Gerling, 06/26/2006 13:15
Jennifer Gerling, 06/26/2006 11:44 -- Created document.
Jennifer Gerling, 06/26/2006 13:15
Jennifer Gerling, 06/26/2006 11:44 -- Created document.