@inproceedings{255ce68175964ca1b110d70d8fc1ce61,
title = "Semi-linear VASR for Over-Approximate Semi-linear Transition System Reachability",
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{\textquoteright}s SVASR-reflection can be computed in polynomial time.",
keywords = "Linear Integer Arithmetic, Vector Addition Systems",
author = "Nikhil Pimpalkhare and Zachary Kincaid",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.; 18th International Conference on Reachability Problems, RP 2024 ; Conference date: 25-09-2024 Through 27-09-2024",
year = "2024",
doi = "10.1007/978-3-031-72621-7_11",
language = "English (US)",
isbn = "9783031726200",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "154--166",
editor = "Laura Kov{\'a}cs and Ana Sokolova",
booktitle = "Reachability Problems - 18th International Conference, RP 2024, Proceedings",
address = "Germany",
}