Symmetry limits power of two counter machines making reachability decidable
Symmetric two-counter machines
Formal Languages and Automata Theory
Summary
Counter machines are simple computer models that can normally do any computation, like a computer. This paper studies two-counter machines where the instructions don't change if you swap the two counters. The authors show this symmetry makes the machine less powerful, so much that it can be decided whether a certain state can be reached. They also explore what happens with three or more counters, finding some symmetrical cases still undecidable.
What this means in practice
- •For formal verification engineers: Identify classes of symmetric counter systems for which reachability checking is decidable to improve automated verification safety guarantees.
- •For automata theory designers: Use symmetry constraints in designing counter machines to ensure analyzable computational models with guaranteed decidability of reachability.
A theory result. No direct application yet.
Authors
Krzysztof Jaros, Łukasz Kamiński, Maja Kądziołka, Sławomir Lasota
Abstract
Counter machines are a particularly simple, Turing-complete model of computation. We study the expressive power of nondeterministic 2-counter machines which are symmetric, in that their set of update transitions is invariant under swapping of counters. Our model is an extension of symmetric 2-VASS, in that we allow modifying both counters within a single transition. As the main result we demonstrate a dramatic impact of symmetry: we show that symmetric 2-counter machines are not Turing-complete, by proving decidability of their reachability problem. We conjecture that the decidability extends to machines with 3 or more counters that are symmetric, meaning the set of update transitions is invariant under any permutation of counters. We leave this problem open for machines with 3 and more counters, while identifying a frontier of the impact of symmetry: we prove undecidability for 3-counter machines invariant under the cyclic permutation group of order 3.