Abstract
Expand, enlarge, and check (EEC) is a successful heuristic for the coverability problem of well-structured transition systems. EEC constructs a sequence of under- and over-approximations with the property that the presence of a bug is eventually exhibited by some under-approximation and the absence of a bug is eventually exhibited by some over-approximation.
In this paper, we consider the application of EEC to the coverability problem for branching vector addition systems (BVAS), an expressive model that subsumes Petri nets. We describe an EEC algorithm for BVAS, and prove its termination and correctness. We prove an upper bound on the number of iterations for our EEC algorithm, both for BVAS and, as a special case, vector addition systems (or Petri nets). We show that in addition to practical effectiveness, the EEC heuristic is asymptotically optimal. For BVAS, it requires at most doubly-exponentially many iterations, thus matching the optimal 2EXPTIME upper bound. For Petri nets, it can be implemented in EXPSPACE, again matching the optimal bound. We have implemented our algorithm and used it to verify safety properties of concurrent programs with asynchronous tasks.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. In: POPL, pp. 203–214 (2012)
Bozzelli, L., Ganty, P.: Complexity analysis of the backward coverability algorithm for VASS. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 96–109. Springer, Heidelberg (2011)
Charles, P., Grothoff, C., Saraswat, V., Donawa, C., Kielstra, A., Ebcioglu, K., von Praun, C., Sarkar, V.: X10: an object-oriented approach to non-uniform cluster computing. SIGPLAN Not. 40(10), 519–538 (2005)
Cunningham, R.: Eel: Tools for debugging, visualization, and verification of event-driven software. Master’s thesis, UCLA (2005)
Demri, S., Jurdzinski, M., Lachish, O., Lazic, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci. 79(1), 23–38 (2013)
Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. In: ACM Transactions on Programming Languages and Systems (2012)
Geeraerts, G., Raskin, J.-F., Begin, L.V.: Expand, enlarge and check: New algorithms for the coverability problem of wsts. J. Comput. Syst. Sci. 72(1), 180–203 (2006)
Halstead, R.H.: Multilisp: a language for concurrent symbolic computation. ACM Transactions on Programming Languages and Systems 7, 501–538 (1985)
Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL 2007, pp. 339–350. ACM Press (2007)
Kaiser, A., Kroening, D., Wahl, T.: Efficient coverability analysis by proof minimization. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 500–515. Springer, Heidelberg (2012)
Karp, R., Miller, R.: Parallel program schemata. Journal of Comput. Syst. Sci. 3(2), 147–195 (1969)
Kitchin, D., Quark, A., Cook, W., Misra, J.: The Orc programming language. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol. 5522, pp. 1–25. Springer, Heidelberg (2009)
Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 158–173. Springer, Heidelberg (2013)
Leijen, D., Schulte, W., Burckhardt, S.: The design of a task parallel library. In: OOPSLA 2009, pp. 227–242. ACM (2009)
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6(2), 223–231 (1978)
Verma, K., Goubault-Larrecq, J.: Karp-Miller trees for a branching extension of VASS. Discrete Mathematics & Theoretical Computer Science 7(1), 217–230 (2005)
Verma, K.N., Goubault-Larrecq, J.: Alternating two-way AC-tree automata. Inf. Comput. 205(6), 817–869 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Majumdar, R., Wang, Z. (2013). Expand, Enlarge, and Check for Branching Vector Addition Systems. In: D’Argenio, P.R., Melgratti, H. (eds) CONCUR 2013 – Concurrency Theory. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-40184-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40183-1
Online ISBN: 978-3-642-40184-8
eBook Packages: Computer ScienceComputer Science (R0)