The theory of reachability in trace-pushdown systems

TL;DR

This paper studies pushdown systems with trace-based stacks, identifying a class where reachability and first-order theory are decidable, extending prior results on multi-stack systems.

Contribution

It introduces a class of trace-pushdown systems enabling decidability of their configuration graph's first-order theory, broadening understanding of reachability in complex automata.

Findings

Decidability of the first-order theory for certain trace-pushdown systems

Extension of decidability results to systems with trace-based stacks

Connection to valence automata over graph monoids

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).