Semi-linear VASR for Over-Approximate Semi-linear Transition System Reachability

Nikhil Pimpalkhare, Zachary Kincaid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationReachability Problems - 18th International Conference, RP 2024, Proceedings
EditorsLaura Kovács, Ana Sokolova
PublisherSpringer Science and Business Media Deutschland GmbH
Pages154-166
Number of pages13
ISBN (Print)9783031726200
DOIs
StatePublished - 2024
Event18th International Conference on Reachability Problems, RP 2024 - Vienna, Austria
Duration: Sep 25 2024Sep 27 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume15050 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Conference on Reachability Problems, RP 2024
Country/TerritoryAustria
CityVienna
Period9/25/249/27/24

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Keywords

  • Linear Integer Arithmetic
  • Vector Addition Systems

Fingerprint

Dive into the research topics of 'Semi-linear VASR for Over-Approximate Semi-linear Transition System Reachability'. Together they form a unique fingerprint.

Cite this