Abstract
We present an abstract interpretation based approach to solve the coverability problem of well-structured transition systems. Our approach distinguishes from other attempts in that (1) we solve this problem for the whole class of well-structured transition systems using a forward algorithm. So, our algorithm has to deal with possibly infinite downward closed sets. (2) Whereas other approaches have a non generic representation for downward closed sets of states, which turns out to be hard to devise in practice, we introduce a generic representation requiring no additional effort of implementation.
Supported by the FRFC project “Centre Fédéré en Vérification” funded by the Belgian National Science Foundation (FNRS) under grant nr 2.4530.02.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–236 (1994)
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of LICS, pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127, 91–101 (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)
Delzanno, G., Raskin, J.F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 173–187. Springer, Heidelberg (2002)
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast acceleration of symbolic transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proceedings of LICS, pp. 352–359. IEEE Computer Society Press, Los Alamitos (1999)
Reisig, W.: Petri Nets. An introduction. Springer, Heidelberg (1986)
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)
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)
Raskin, J.F., Van Begin, L.: Petri nets with non-blocking arcs are difficult to analyse. In: Proceedings of INFINITY. ENTCS, vol. 96. Elsevier, Amsterdam (2003)
Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: Proc. of LICS, pp. 70–80. IEEE Computer Society Press, Los Alamitos (1998)
Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2(3), 326–336 (1952)
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)
Abdulla, P., Deneux, J., Mahata, P., Nylen, A.: Forward reachability analysis of timed petri nets. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 343–362. Springer, Heidelberg (2004)
Ganty, P., Raskin, J.F., Van Begin, L.: A complete abstract interpretation framework for coverability properties of WSTS. Technical Report 2005.57, Centre Fédéré en Vérification, CFV (2005)
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS, pp. 313–321. IEEE Computer Society Press, Los Alamitos (1996)
Delzanno, G., Raskin, J.F., Begin, L.V.: Covering sharing trees: a compact data structure for parameterized verification. Software Tools for Technology Transfer (STTT) 5, 268–297 (2004)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256, 63–92 (2001)
Finkel, A.: Reduction and covering of infinite reachability trees. Inf. Comput. 89, 144–179 (1990)
Esparza, J., Ganty, P., Schwoon, S.: Locality-based abstractions. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 118–134. Springer, Heidelberg (2005)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers 35, 677–691 (1986)
Van Begin, L.: Efficient Verification of Counting Abstractions for Parametric Systems. PhD thesis, Université Libre de Bruxelles (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
Ganty, P., Raskin, JF., Van Begin, L. (2005). A Complete Abstract Interpretation Framework for Coverability Properties of WSTS . In: Emerson, E.A., Namjoshi, K.S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2006. Lecture Notes in Computer Science, vol 3855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11609773_4
Download citation
DOI: https://doi.org/10.1007/11609773_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31139-3
Online ISBN: 978-3-540-31622-0
eBook Packages: Computer ScienceComputer Science (R0)