Abstract
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 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.
This work has been partially supported by the FRFC grant 2.4530.02. of the National Belgian Fund for Scientific Research (FNRS).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General Decidability Theorems for Infinite-state Systems. In: Proc. of LICS 1996, pp. 313–321. IEEE, Los Alamitos (1996)
Abdulla, P., Annichini, A., Bouajjani, A.: Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 208–222. Springer, Heidelberg (1999)
Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. Form. Methods Syst. Des. 25(1), 39–65 (2004)
Ciardo, G.: Petri nets with marking-dependent arc multiplicity: properties and analysis. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 179–198. Springer, Heidelberg (1994)
Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking Symbolic State Explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 298–310. Springer, Heidelberg (2001)
Emerson, E.A., Namjoshi, K.S.: On Model Checking for Non-deterministic Infinite-state Systems. In: Proc. of LICS 1998, pp. 70–80. IEEE, Los Alamitos (1998)
Esparza, J., Finkel, A., Mayr, R.: On the Verification of Broadcast Protocols. In: Proc. of LICS 1999, pp. 352–359. IEEE, Los Alamitos (1999)
Finkel, A.: The minimal coverability graph for Petri nets. In: Rozenberg, G. (ed.) APN 1993. LNCS, vol. 674, pp. 210–243. Springer, Heidelberg (1993)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)
Finkel, A., Geeraerts, G., Raskin, J.-F., Van Begin, L.: A counter-example to the minimal coverability tree algorithm, Technical report ULB 535, http://www.ulb.ac.be/di/ssd/ggeeraer/papers/FGRV05-Coverability.pdf
Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 287–298. Springer, Heidelberg (2004)
Henzinger, T.A., Kupferman, O., Qadeer, S.: From prehistoric to postmodern symbolic model checking. Formal Methods in System Design 23(3), 303–327 (2003)
Schnoebelen, P.: Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Information Processing Letters 83(5), 251–261 (2002)
Van Begin, L.: Efficient Verification of Counting Abstractions for Parametric systems. PhD thesis, Université Libre de Bruxelles, Belgium (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geeraerts, G., Raskin, JF., Van Begin, L. (2005). Expand, Enlarge and Check... Made Efficient. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_38
Download citation
DOI: https://doi.org/10.1007/11513988_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)