Abstract
This paper introduces Semi-Linear Integer Vector Addition Systems with Resets (SVASR). A SVASR is a labeled transition system in which the states are finite-dimensional integer-valued vectors and which transitions from one state to another by applying an orthogonal projection followed by a translation drawn from a semi-linear set. We give a polynomial-time reduction of SVASR reachability to that of Integer Vector Addition Systems with Resets.
We then consider the use of SVASRs for over-approximating the reachability relation of transition systems in which the transition relation is a semi-linear set. We show that any semi-linear transition system has a “best” SVASR that simulates its behavior, called its SVASR-reflection. The dimension of the SVASR-reflection of a semi-linear transition system T with states is exponential in the number of states; however, we show that the over-approximate reachability induced by T’s SVASR-reflection can be computed in polynomial time.
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
Notes
- 1.
We restrict our attention to transition systems in which the state space is a finite-dimensional module over the integers.
References
Blondin, M., Haase, C., Mazowiecki, F., Raskin, M.: Affine extensions of integer vector addition systems with states. Logical Methods Comput. Sci. 17(3) (2021). https://doi.org/10.46298/lmcs-17(3:1)2021
Chistikov, D., Haase, C., Halfon, S.: Context-free commutative grammars with integer counters and resets. Theor. Comput. Sci. 735, 147–161 (2018). https://doi.org/10.1016/j.tcs.2016.06.017. https://www.sciencedirect.com/science/article/pii/S0304397516302535. Reachability Problems 2014: Special Issue
Haase, C., Halfon, S.: Integer vector addition systems with states. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 112–124. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11439-2_9
Lazic, R.: The reachability problem for vector addition systems with a stack is not elementary (2013). https://arxiv.org/abs/1310.1767
Levatich, M., Bjørner, N., Piskac, R., Shoham, S.: Solving \(\text{ LIA}^\star \) using approximations. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 360–378. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-39322-9_17
Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing, STOC 1981, pp. 238–246. Association for Computing Machinery, New York (1981). https://doi.org/10.1145/800076.802477
Parikh, R.J.: On context-free languages. J. ACM 13(4), 570–581 (1966). https://doi.org/10.1145/321356.321364
Pimpalkhare, N., Kincaid, Z.: Monotone procedure summarization via vector addition systems and inductive potentials. https://nikhilpim.github.io/images/oopsla24.pdf
Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 268–280. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_25
Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 97–115. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_7
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Pimpalkhare, N., Kincaid, Z. (2024). Semi-linear VASR for Over-Approximate Semi-linear Transition System Reachability. In: Kovács, L., Sokolova, A. (eds) Reachability Problems. RP 2024. Lecture Notes in Computer Science, vol 15050. Springer, Cham. https://doi.org/10.1007/978-3-031-72621-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-031-72621-7_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-72620-0
Online ISBN: 978-3-031-72621-7
eBook Packages: Computer ScienceComputer Science (R0)