The coverability problem is decidable for the class of well-structured 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 monotonie 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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Geeraerts, G., Raskin, J. F., & Van Begin, L. (2005). Expand, enlarge and check. . . made efficient. In Lecture Notes in Computer Science (Vol. 3576, pp. 394–407). Springer Verlag. https://doi.org/10.1007/11513988_38
Mendeley helps you to discover research relevant for your work.