Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS

Laurent Van Begin
ULB
Friday, 28 May, 2004 (All day)
NO

In this talk, we will present a general schema called "Expand-Enlarge and Check" from which new efficient algorithms for the coverability problem of WSTS can be constructed. Well-structured transition systems (WSTS for short) are a general class of infinite state systems for which decidability results rely on the existence of a well-quasi-ordering between states that is compatible with the transitions. In particular, the coverabiliy problem (reachability of an upward-closed set of states, relative to the wqo), is decidable for that class of systems. Popular examples of WSTS are Petri nets, monotonic extensions of Petri nets, and lossy fifo systems. For all those systems, the coverability problem can be answered by a simple backward algorithm. Unfortunately, this general backward algorithm may be highly inefficient because it often has to manipulate sets of states that are unreachable and difficult to represent compactly. In the late 60s, Karp and Miller have defined a procedure that uses forward reachability and acceleration to decide the coverability problem of Petri nets. The advantage of the forward approach is that it has to manipulate sets of reachable states that are usually easier to represent compactly. Several attempts to generalize this approach to other classes of WSTS have failled. We show here that our schema allows us to define forward algorithms that decide coverability for classes of systems for which the Karp and Miller procedure can not be generalized. In particular, we present a direct application of our schema to monotonic extensions of Petri nets. Our result has important applications in parametric verification and allows us to prove a completness result for a recent algorithm proposed by Henzinger et al for the analysis of multi-threaded programs.

This is a joint work with Gilles Geeraerts and J-F Raskin.