2025/07/21 by Dietrich Kuske, Kuske, Dietrich
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2507.15733
openalex publication_date 2025/07/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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).