pith. sign in

arxiv: 2507.15733 · v2 · submitted 2025-07-21 · 💻 cs.FL

The theory of reachability in trace-pushdown systems

Dietrich Kuske This is my paper

Pith reviewed 2026-05-19 04:19 UTC · model grok-4.3

classification 💻 cs.FL
keywords trace-pushdown systemsMazurkiewicz tracesconfiguration graphsfirst-order theorydecidabilityreachabilitygraph monoidsdependence alphabet
0
0 comments X

The pith

Certain trace-pushdown systems defined by restricted graph monoids make the first-order theory of reachability in their configuration graphs decidable.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies pushdown systems whose stacks hold Mazurkiewicz traces instead of ordinary words. These systems generalize multi-stack machines and arise as valence automata over graph monoids. It isolates a subclass, obtained by placing suitable restrictions on the underlying graph monoid or dependence alphabet, for which the first-order theory of the configuration graph augmented with reachability is decidable. This extends earlier decidability results that required stronger restrictions on the alphabet while still covering only general pushdown systems.

Core claim

The author shows that trace-pushdown systems whose dependence alphabets satisfy the identified restrictions admit a decidable first-order theory of their configuration graphs when reachability is included as a primitive relation. The proof proceeds by reducing the theory to known decidable fragments via the structural properties enforced by those restrictions.

What carries the argument

The restricted class of trace-pushdown systems, obtained by imposing conditions on the graph monoid or dependence alphabet, which makes the first-order theory of the configuration graph with reachability decidable.

If this is right

  • Verification problems expressible in first-order logic over configurations become decidable for this class of systems.
  • The result covers models that include concurrent or multi-stack behavior under the stated alphabet restrictions.
  • It provides a uniform decision procedure that complements the alphabet-restricted case for ordinary pushdown systems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same restrictions might yield decidability results for related models such as certain classes of vector addition systems with states.
  • One could test whether relaxing a single condition in the definition of the class immediately produces an undecidable instance.

Load-bearing premise

The systems must belong to the restricted class defined by the paper's conditions on the graph monoid or dependence alphabet.

What would settle it

An explicit trace-pushdown system satisfying the paper's restrictions for which the first-order theory of its configuration graph with reachability is shown to be undecidable would refute the claim.

read the original 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).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper studies pushdown systems in which the stack alphabet is replaced by a Mazurkiewicz trace (equivalently, valence automata over graph monoids). These systems generalize ordinary pushdown automata and multi-stack systems. The central claim is that there exists a non-trivial class of such systems, obtained by imposing suitable restrictions on the underlying dependence alphabet or graph monoid, for which the first-order theory of the configuration graph augmented with the reachability predicate is decidable. The result is presented as complementing the decidability theorem of D'Osualdo, Meyer and Zetzsche for ordinary pushdown systems under a severe restriction on the dependence alphabet.

Significance. If the identified class is non-trivial and the decidability proof is effective and self-contained, the result would constitute a meaningful contribution to the decidability landscape for reachability and logical theories in concurrent systems. It would provide a concrete bridge between the theory of valence automata over graph monoids and the study of trace-based storage, potentially enabling new verification techniques for systems whose concurrency is captured by partial commutation. The manuscript's explicit construction of the class and its reduction to a decidable fragment, building directly on cited prior work without circularity, strengthens the assessment.

minor comments (3)
  1. §3 (Definition of the restricted class): the precise syntactic or algebraic restrictions on the dependence alphabet that guarantee decidability should be stated as a single, easily checkable condition rather than distributed across several lemmas.
  2. §4.2 (Reduction to FO theory): the effectiveness of the automata construction that interprets reachability should be made explicit by giving the state complexity or the size of the resulting formula in terms of the input system.
  3. Figure 1: the diagram illustrating the configuration graph for a small trace-pushdown system would benefit from explicit labels on the edges showing the trace operations performed.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. The referee's description of the contribution accurately reflects the manuscript's focus on trace-pushdown systems and the decidability result for the first-order theory with reachability, as a complement to the work of D'Osualdo, Meyer, and Zetzsche.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper identifies a restricted class of trace-pushdown systems (valence automata over graph monoids with suitable dependence alphabet restrictions) and proves decidability of the first-order theory of the configuration graph augmented with reachability. The central result is established via direct automata constructions and logical interpretations that reduce to known decidable fragments, building on externally cited prior work by different authors (D'Osualdo et al.) without any reduction of the target theorem to self-definitions, fitted inputs renamed as predictions, or load-bearing self-citations. The class definition and effectiveness claims are presented as independent of the final decidability statement.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The result rests on standard background from automata theory, trace theory, and first-order logic; no free parameters or invented entities are visible in the abstract.

axioms (2)
  • standard math Mazurkiewicz traces and graph monoids form the algebraic basis for the stack content.
    The abstract explicitly builds on these established structures from prior literature.
  • standard math First-order logic with reachability predicate is the query language whose decidability is studied.
    Standard in the theory of configuration graphs and verification.

pith-pipeline@v0.9.0 · 5594 in / 1257 out tokens · 50834 ms · 2026-05-19T04:19:44.415170+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

35 extracted references · 35 canonical work pages

  1. [1]

    In: LICS’00

    Blumensath, A., Grädel, E.: Automatic Structures. In: LICS’00. pp. 51–62. IEEE Computer Society Press (2000)

    work page 2000

  2. [2]

    Theory of Computing Systems37(6), 641–674 (2004)

    Blumensath, A., Grädel, E.: Finite presentations of infinite structures: Automata and interpretations. Theory of Computing Systems37(6), 641–674 (2004)

    work page 2004

  3. [3]

    Lecture Notes in Mathematics vol

    Cartier, P., Foata, D.: Problèmes combinatoires de commutation et réarrange- ments. Lecture Notes in Mathematics vol. 85, Springer, Berlin - Heidelberg - New York (1969)

    work page 1969

  4. [4]

    Courcelle,B.,Engelfriet,J.:Graphstructureandmonadicsecond-orderlogic.Cam- bridge University Press (2012)

    work page 2012

  5. [5]

    World Scientific Publ

    Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific Publ. Co. (1995)

    work page 1995

  6. [6]

    In: LICS’16

    D’Osualdo, E., Meyer, R., Zetzsche, G.: First-order logic with reachability for infinite-state systems. In: LICS’16. pp. 457–466. ACM (2016)

    work page 2016

  7. [7]

    Inter- national Journal of Algebra and Computation18(08), 1345–1364 (2008)

    Elder, M., Kambites, M., Ostheimer, G.: On groups and counter automata. Inter- national Journal of Algebra and Computation18(08), 1345–1364 (2008)

    work page 2008

  8. [8]

    Theoretical Computer Science320(2-3), 175–185 (2004)

    Elston, G., Ostheimer, G.: On groups whose word problem is solved by a counter automaton. Theoretical Computer Science320(2-3), 175–185 (2004)

    work page 2004

  9. [9]

    Gilman, R.: Formal Languages and Infinite Groups, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 25. DIMACS (1996)

    work page 1996

  10. [10]

    Theoretical Computer Science 19, 331–335 (1982)

    Hodgson, B.: On direct products of automaton decidable theories. Theoretical Computer Science 19, 331–335 (1982)

    work page 1982

  11. [11]

    Theoretical Computer Science 2(3), 271–294 (1976)

    Ibarra, O., Sahni, S., Kim., C.: Finite automata with multiplication. Theoretical Computer Science 2(3), 271–294 (1976)

    work page 1976

  12. [12]

    Acta Informatica 38, 117–129 (2001)

    Ito, M., Martín-Vide, C., Mitrana, V.: Group weighted finite transducers. Acta Informatica 38, 117–129 (2001)

    work page 2001

  13. [13]

    Communications in Alge- bra 37, 193–208 (2009)

    Kambites, M.: Formal languages and groups as memory. Communications in Alge- bra 37, 193–208 (2009)

    work page 2009

  14. [14]

    In: Logic and Computational Complexity

    Khoussainov, B., Nerode, A.: Automatic presentations of structures. In: Logic and Computational Complexity. pp. 367–392. Lecture Notes in Comp. Science vol. 960, Springer (1995)

    work page 1995

  15. [15]

    In: Shan- non, C., McCarthy, J

    Kleene, S.: Representation of events in nerve nets and finite automata. In: Shan- non, C., McCarthy, J. (eds.) Automata Studies, pp. 3–40. Annals of Mathematics Studies vol. 34, Princeton University Press (1956)

    work page 1956

  16. [16]

    In: FCT’23

    Köcher, C., Kuske, D.: Forwards- and backwards-reachability for cooperating multi-pushdown systems. In: FCT’23. pp. 318–332. Lecture Notes in Comp. Science vol. 14252, Springer (2023)

    work page 2023

  17. [17]

    Journal of Computer and System Sciences148 (2025), article no

    Köcher, C., Kuske, D.: Backwards-reachability for cooperating multi-pushdown systems. Journal of Computer and System Sciences148 (2025), article no. 103601

    work page 2025

  18. [18]

    Köcher, C., Kuske, D.: Reachability in trace-pushdown systems (2025), submitted, the paper can be obtained at http://eiche.theoinf.tu-ilmenau.de/kuske

    work page 2025

  19. [19]

    Theoretical Computer Sci- ence 374, 127–148 (2007)

    Kuske, D.: Weighted asynchronous cellular automata. Theoretical Computer Sci- ence 374, 127–148 (2007)

    work page 2007

  20. [20]

    In: CAI 2009

    Kuske, D.: Theories of automatic structures and their complexity. In: CAI 2009. pp. 81–98. Lecture Notes in Comp. Science vol. 5725, Springer (2009)

    work page 2009

  21. [21]

    In: FSTTCS’23

    Kuske, D.: A class of rational trace relations closed under composition. In: FSTTCS’23. pp. 20:1–20:20. Leibniz International Proceedings in Informatics (LIPIcs) vol. 284, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

    work page 2023

  22. [22]

    In: CiE’25

    Kuske, D.: The theory of reachability in trace-pushdown systems. In: CiE’25. pp. 283–298. Lecture Notes in Comp. Science. vol. 15764, Springer (2025) 22 Dietrich Kuske

    work page 2025

  23. [23]

    Jour- nal of Symbolic Logic75(2), 678–710 (2010)

    Kuske, D., Lohrey, M.: Some natural decision problems in automatic graphs. Jour- nal of Symbolic Logic75(2), 678–710 (2010)

    work page 2010

  24. [24]

    R.A.I.R.O

    Métivier, Y.: Une condition suffisante de reconnaissabilité dans un monoide par- tiellement commutatif. R.A.I.R.O. - Informatique Théorique et Applications20, 121–127 (1986)

    work page 1986

  25. [25]

    Discrete Applied Mathematics 108(3), 287–300 (2001)

    Mitrana, V., Stiebe, R.: Extended finite automata over groups. Discrete Applied Mathematics 108(3), 287–300 (2001)

    work page 2001

  26. [26]

    In: MFCS’99

    Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. In: MFCS’99. pp. 81–91. Lecture Notes in Comp. Science vol. 1672, Springer (1999)

    work page 1999

  27. [27]

    Ochmański, E.: Regular behaviour of concurrent systems. Bull. Europ. Assoc. for Theor. Comp. Science27, 56–67 (1985)

    work page 1985

  28. [28]

    Boll Amer

    Post, E.: A variant of a recursively unsolvable problem. Boll Amer. Math. Soc. 52(4), 264–269 (1946)

    work page 1946

  29. [29]

    Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc.141, 1–35 (1969)

    work page 1969

  30. [30]

    Information and Computation207(11), 1329–1339 (2009)

    Render, E., Kambites, M.: Rational subsets of polycyclic monoids and valence automata. Information and Computation207(11), 1329–1339 (2009)

    work page 2009

  31. [31]

    Render, E.: Rational Monoid and Semigroup Automata. Ph.D. thesis, University of Manchester (2010)

    work page 2010

  32. [32]

    Rubin, S.: Automatic Structures. Ph.D. thesis, University of Auckland (2004)

    work page 2004

  33. [33]

    Bul- letin of Symbolic Logic14, 169–209 (2008)

    Rubin, S.: Automata presenting structures: A survey of the finite string case. Bul- letin of Symbolic Logic14, 169–209 (2008)

    work page 2008

  34. [34]

    In: RP’15

    Zetzsche, G.: The emptiness problem for valence automata or: Another decidable extension of Petri nets. In: RP’15. pp. 166–178. Lecture Notes in Comp. Science vol. 9328, Springer (2015)

    work page 2015

  35. [35]

    Zetzsche, G.: The emptiness problem for valence automata over graph monoids. Inf. Comput. 277 (2021), article no. 104583

    work page 2021