Abstract
We introduce a logic for specifying trace properties of vector addition systems (VAS). This logic can express linear relations among pumping segments occurring in a trace. Given a VAS and a formula in the logic, we investigate the question whether the VAS contains a trace satisfying the formula. Our main contribution is an exponential space upper bound for this problem. The proof is based on a small model property for the logic. Compared to similar logics that are solvable in exponential space, a distinguishing feature of our logic is its ability to express non-context-freeness of the trace language of a VAS. This allows us to show that the context-freeness problem for VAS, whose complexity was not established so far, is ExpSpace-complete.
This work was supported by the ANR project ReacHard (ANR-11-BS02-001).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Atig, M.F., Habermehl, P.: On Yen’s path logic for Petri nets. Int. J. Found. Comput. Sci. 22(4), 783–799 (2011)
Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 108–119. Springer, Heidelberg (2011)
Demri, S.: On selective unboundedness of VASS. In: Proc. INFINITY. EPTCS, vol. 39, pp. 1–15 (2010)
Esparza, J., Nielsen, M.: Decidability issues for Petri nets - a survey. Bulletin of the EATCS 52, 244–262 (1994)
Karp, R.M., Miller, R.E.: Parallel program schemata. Journal of Computer and System Sciences 3(2), 147–195 (1969)
Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: Proc. STOC, pp. 267–281. ACM (1982)
Leroux, J.: Vector addition system reversible reachability problem. Logical Methods in Computer Science 9(1) (2013)
Leroux, J., Penelle, V., Sutre, G.: On the context-freeness problem for vector addition systems. In: Proc. LICS. IEEE (to appear, 2013)
Lipton, R.J.: The reachability problem requires exponential space. Technical Report 62, Yale University (1976)
Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proc. STOC, pp. 238–246. ACM (1981)
Mayr, E.W., Meyer, A.R.: The complexity of the finite containment problem for Petri nets. J. ACM 28(3), 561–576 (1981)
Pottier, L.: Minimal solutions of linear diophantine systems: Bounds and algorithms. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 162–173. Springer, Heidelberg (1991)
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6(2), 223–231 (1978)
Schwer, S.R.: The context-freeness of the languages associated with vector addition systems is decidable. Theor. Comput. Sci. 98(2), 199–247 (1992)
Valk, R., Jantzen, M.: The residue of vector sets with applications to decidability problems in Petri nets. Acta Inf. 21, 643–674 (1985)
Valk, R., Vidal-Naquet, G.: Petri nets and regular languages. Journal of Computer and System Sciences 23(3), 299–325 (1981)
Yen, H.-C.: A unified approach for deciding the existence of certain Petri net paths. Inf. Comput. 96(1), 119–137 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leroux, J., Praveen, M., Sutre, G. (2013). A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness. 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_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-40184-8_11
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)