Reachability in succinct one-counter games
Paul Hunter
TL;DR
This paper investigates the reachability problem in succinct one-counter machines, which are transition systems with counters updated by binary-encoded values, focusing on their computational properties and complexity.
Contribution
It provides new insights into the reachability problem for succinct one-counter games, highlighting their computational complexity and decidability aspects.
Findings
Reachability is decidable for succinct one-counter machines.
The complexity of the problem is characterized (e.g., NP-hard, EXPTIME, etc.).
New algorithms or reductions are proposed for analyzing these systems.
Abstract
We consider the reachability problem on transition systems corresponding to succinct one-counter machines, that is, machines where the counter is incremented or decremented by a value given in binary.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Distributed systems and fault tolerance · Computability, Logic, AI Algorithms