|
|
In this paper we discuss the use of logic for reachability analysis for
infinite-state systems. Infinite-state systems are formalized using
transition systems over a first-order structure. We establish a common
ground relating a large class of algorithms by analyzing the connections
between the symbolic representation of transition systems and formulas used
in various reachability algorithms. We consider in detail the so-called
\emph{guarded assignment systems} and \emph{local reachability algorithms}.
We show how an implementation of local reachability algorithms and a new
incremental algorithm for finding Hilbert's base in the system \Brain\
resulted in much faster reachability checking than in systems using
constraint libraries and decision procedures for Presburger's arithmetic.
Experimental results demonstrate that problems in protocol verification
which are beyond the reach of other existing systems can be solved
completely automatically.
|
© 2002-2003 Kurt Gödel Society, Norbert Preining. |
2003-07-09
 | |
Print this page