Expand, Enlarge and Check... Made Efficient

10 years 1 months ago
Expand, Enlarge and Check... Made Efficient
Abstract. The coverability problem is decidable for the class of wellstructured transition systems. Until recently, the only known algorithm to solve this problem was based on symbolic backward reachability. In a recent paper, we have introduced the theory underlying a new algorithmic solution, called ‘Expand, Enlarge and Check’, which can be implemented in a forward manner. In this paper, we provide additional concepts and algorithms to turn this theory into efficient forward algorithms for monotonic extensions of Petri nets and Lossy Channels Systems. We have implemented a prototype and applied it on a large set of examples. This prototype outperforms a previous fine tuned prototype based on backward symbolic exploration and shows the practical interest of our new algorithmic solution. The data used in the experiments and more relevant information about ‘Expand, Enlarge and Check’ can be found at:
Gilles Geeraerts, Jean-François Raskin, Lau
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CAV
Authors Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin
Comments (0)