The theory of reachability in trace-pushdown systems
Formal Languages and Automata Theory
2026-05-05 v2
Abstract
We consider pushdown systems that store, instead of a single word, a Mazurkiewicz trace on its stack. These systems are special cases of valence automata over graph monoids and subsume multi-stack systems. We identify a class of such systems that allow to decide the first-order theory of their configuration graph with reachability. This result complements results by D'Osualdo, Meyer, and Zetzsche (namely the decidability for arbitrary pushdown systems under a severe restriction on the dependence alphabet).
Keywords
Cite
@article{arxiv.2507.15733,
title = {The theory of reachability in trace-pushdown systems},
author = {Dietrich Kuske},
journal= {arXiv preprint arXiv:2507.15733},
year = {2026}
}