scientific article; zbMATH DE number 7559493

DOI10.4230/LIPICS.CONCUR.2020.37MaRDI QIDQ5089304zbMATH OpenFDO

Authors Jérôme Leroux, Grégoire Sutre

Publication date 18 July 2022

Full work available at URL https://arxiv.org/abs/2007.09096

zbMATH Keywords

counter machineformal verificationinfinite-state systemreachability problemvector addition system

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• A Sharp Bound on Positive Solutions of Linear Diophantine Equations
• A structure to decide reachability in Petri nets
• An Algorithm for the General Petri Net Reachability Problem
• Automated Technology for Verification and Analysis
• CONCUR 2004 - Concurrency Theory
• Deterministic one-counter automata
• scientific article; zbMATH DE number 1223710 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• Langages à un compteur
• Minimal solutions of linear diophantine systems : bounds and algorithms
• New pumping technique for 2-dimensional VASS
• On the coverability problem for pushdown vector addition systems in one dimension
• On the reachability problem for 5-dimensional vector addition systems
• Reachability for two-counter machines with one test and one reset
• Reachability in Petri nets with inhibitor arcs
• Reachability in Succinct and Parametric One-Counter Automata
• Reachability in two-clock timed automata is PSPACE-complete
• Reachability in two-dimensional unary vector addition systems with states is NL-complete
• Reachability in two-dimensional vector addition systems with states is PSPACE-complete
• Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
• The general vector addition system reachability problem by Presburger inductive invariants
• The reachability problem for Petri nets is not elementary
• The Reachability Problem for Vector Addition System with One Zero-Test
• Vector addition system reachability problem, a short self-contained proof

Cited in

(7)

• The Reachability Problem for Vector Addition System with One Zero-Test
• The Reachability Problem for Two-Dimensional Vector Addition Systems with States
• Coverability in 2-VASS with one unary counter is in NP
• Flattability of priority vector addition systems
• Synchronized CTL over one-counter automata
• Monus semantics in vector addition systems with states
• Challenges of the reachability problem in infinite-state systems (invited paper)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5089304)