pith. machine review for the scientific record. sign in

arxiv: 2603.11648 · v2 · submitted 2026-03-12 · 💻 cs.FL · cs.CC

Recognition: no theorem link

Visibly Recursive Automata

K\'evin Dubrulle , V\'eronique Bruy\`ere , Guillermo A. P\'erez , Ga\"etan Staquet
Authors on Pith no claims yet

Pith reviewed 2026-05-15 12:20 UTC · model grok-4.3

classification 💻 cs.FL cs.CC
keywords visibly recursive automataprocedural automatacodeterminismcomplementationautomata theoryrecursive callslanguage operations
0
0 comments X

The pith

Visibly recursive automata extend procedural automata while codeterminism enables efficient complementation.

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

The paper introduces visibly recursive automata as collections of ordinary finite automata that call one another. Calls become visible by partitioning the input alphabet into call, return, and internal symbols. This model is shown to recognize a strictly larger class of languages than systems of procedural automata. Full determinism restricts the languages that can be accepted, so the authors define codeterminism as a weaker condition that preserves the full expressive power. Codeterminism then yields practical algorithms for standard operations, including complementation.

Core claim

Visibly recursive automata consist of a finite collection of classical automata whose transitions may invoke other automata in the collection. The visibility condition is enforced solely by the input alphabet. The resulting class strictly contains the languages of systems of procedural automata. Codeterminism, a relaxed form of determinism, does not reduce expressiveness yet supports polynomial-time decision procedures such as complementation.

What carries the argument

Visibly recursive automaton, a finite set of classical automata linked by visible recursive calls enforced through alphabet partitioning.

If this is right

  • Union, intersection, and other Boolean operations have the same complexity as for finite automata.
  • Emptiness and membership remain decidable in polynomial time.
  • Complementation of codeterministic VRAs can be implemented in polynomial time.
  • The model remains strictly more expressive than procedural automata even when codeterministic.

Where Pith is reading between the lines

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

  • Codeterminism offers a template for preserving expressiveness while restoring algorithmic tractability in other models of recursive computation.
  • The visibility mechanism may support modular verification of recursive programs whose call structure appears directly in the input.
  • The strict extension result opens the possibility of new separation theorems between recursive language classes.

Load-bearing premise

The visibility of recursive calls can be enforced through the input alphabet without introducing hidden states that would collapse the model to ordinary pushdown automata.

What would settle it

A concrete language that is accepted by some visibly recursive automaton but by no system of procedural automata, or a codeterministic VRA whose complement cannot be constructed in polynomial time.

Figures

Figures reproduced from arXiv: 2603.11648 by Ga\"etan Staquet, Guillermo A. P\'erez, K\'evin Dubrulle, V\'eronique Bruy\`ere.

Figure 1
Figure 1. Figure 1: Example of a VRA and a recursive run of it. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustration of the semantics of a VRA on [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Set of recursive languages of three automata [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A deterministic VRA with no equivalent SPA. [PITH_FULL_IMAGE:figures/full_fig_p018_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: A two-state deterministic VPA. The stacked run on w can alternatively be written ⟨q0, σ0⟩ w−→ ⟨qn, σn⟩. We denote by Π(A) the set of stacked runs of A. A word w is accepted by A if there is an accepting stacked run on w, i.e., that begins in an initial configuration ⟨qo, ε⟩ with qo ∈ I and ends in a final configuration ⟨qf , ε⟩ with qf ∈ F. The language Le(A) of A is the set of all words accepted by A: Le(… view at source ↗
Figure 6
Figure 6. Figure 6: Illustration of Theorem 1. p ′ r[γ] −−→ p ∈ δret. By construction, it follows that g J (q) K−→ g J (p) ∈ δ J , with K = ⟨q ′ , p′ , c, r⟩. As w ′ ∈ WM (Σe), by structural induction, we have ⟨g K(q ′ ), ε⟩ w ′ −→ ⟨g K(p ′ ), ε⟩ ∈ Π(A), meaning that w ′ ∈ Le(AK) because g K(q ′ ) ∈ I K and g K(p ′ ) ∈ F K. By Proposition 1, as f(K) = ⟨c, r⟩, we have the recursive run ⟨g J (q), ε⟩ cw′ r −−−→ ⟨g J (p), ε⟩ ∈ Π(… view at source ↗
Figure 7
Figure 7. Figure 7: Illustration of Theorem 2. G Codeterminism and Completeness Decision Problems In this appendix, we study the complexity class of deciding whether a VRA is codeterministic or complete. Note that these complexities rely on closure prop￾erties and decision problems as discussed in Section 4. G.1 Codeterminism Decision Problem Theorem 5. Deciding whether a VRA is codeterministic is PTIME-complete. Proof. To ch… view at source ↗
read the original abstract

As an alternative to visibly pushdown automata, we introduce visibly recursive automata (VRAs), composed of a set of classical automata that can call each other. VRAs are a strict extension of so-called systems of procedural automata, a model proposed by Frohme and Steffen. We study the complexity of standard language-theoretic operations and classical decision problems for VRAs. Since the class of deterministic VRAs forms a strict subclass in terms of expressiveness, we propose a (weaker) notion that does not restrict expressive power and which we call codeterminism. Codeterminism comes with many desirable algorithmic properties that we demonstrate by using it, e.g., as a stepping stone towards implementing complementation of VRAs.

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

2 major / 1 minor

Summary. The paper introduces visibly recursive automata (VRAs) as a model consisting of a collection of classical finite automata that invoke each other, with recursion visibility enforced by partitioning the input alphabet into call, return, and internal symbols. It claims that VRAs form a strict extension of systems of procedural automata (Frohme and Steffen), studies the complexity of language operations and decision problems, and proposes codeterminism as a weaker determinism notion that preserves full expressiveness while enabling desirable algorithms, demonstrated via its use in implementing complementation.

Significance. If the strict-extension claim and the algorithmic properties of codeterminism hold, the work offers a modular alternative to visibly pushdown automata with potentially efficient complementation and other operations, which could be useful in verification of recursive systems. The concrete demonstration of codeterminism for complementation is a positive aspect if the preservation of expressiveness is rigorously shown.

major comments (2)
  1. [§2] §2 (Definition of VRAs): The strict-extension claim over procedural automata depends on the alphabet partition alone enforcing visibility without hidden state. However, if the call-transition relation permits multiple target modules or return behaviors not uniquely determined by the call symbol, the model can encode nondeterministic module selection, which risks collapsing expressiveness toward ordinary recursive automata and falsifies both the strict-extension claim and the algorithmic guarantees for codeterminism.
  2. [Complementation section] Complementation section (likely §5): The argument that codeterminism preserves full expressiveness while enabling complementation is load-bearing for the algorithmic contribution. The manuscript must supply an explicit construction or proof that every VRA language has an equivalent codeterministic VRA, otherwise the stepping-stone claim for complementation does not go through.
minor comments (1)
  1. [References] The citation to Frohme and Steffen should be expanded with full bibliographic details (venue, year, title) in the references section.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thorough review and valuable feedback on our submission. The two major comments raise important points about the definition and the codeterminism construction; we address each below and will revise the manuscript to incorporate clarifications and the requested explicit proof.

read point-by-point responses

  1. Referee: §2 (Definition of VRAs): The strict-extension claim over procedural automata depends on the alphabet partition alone enforcing visibility without hidden state. However, if the call-transition relation permits multiple target modules or return behaviors not uniquely determined by the call symbol, the model can encode nondeterministic module selection, which risks collapsing expressiveness toward ordinary recursive automata and falsifies both the strict-extension claim and the algorithmic guarantees for codeterminism.

    Authors: We agree that the strict-extension property relies on the visibility mechanism. In the definition of VRAs, the input alphabet is partitioned into call, return, and internal symbols, and the transition relation is defined so that each call symbol uniquely identifies the target module (with no hidden state or nondeterministic choice of module). Return symbols similarly determine the return behavior uniquely from the call symbol. This is what distinguishes VRAs from general recursive automata and ensures the strict extension over procedural automata. We will add an explicit paragraph in the revised §2 stating this uniqueness property and proving that it prevents encoding of nondeterministic module selection. revision: yes

  2. Referee: Complementation section (likely §5): The argument that codeterminism preserves full expressiveness while enabling complementation is load-bearing for the algorithmic contribution. The manuscript must supply an explicit construction or proof that every VRA language has an equivalent codeterministic VRA, otherwise the stepping-stone claim for complementation does not go through.

    Authors: We acknowledge that the current manuscript only sketches the preservation of expressiveness and relies on it for the complementation algorithm. We will add a dedicated subsection with an explicit inductive construction: given any VRA, we build an equivalent codeterministic VRA by augmenting each module with a finite set of auxiliary states that track the necessary history to enforce the codeterministic acceptance condition on returns and calls, without restricting the accepted language. The construction is effective and polynomial in the number of modules. This will be included in the revised complementation section together with the proof that the resulting automaton remains codeterministic and accepts the same language. revision: yes

Circularity Check

0 steps flagged

No significant circularity; definitions and extension are independent

full rationale

The paper defines VRAs directly as sets of classical automata with mutual calls, partitioned input alphabet for visibility, and claims strict extension over the external model of procedural automata (Frohme and Steffen). Codeterminism is introduced as an explicit weaker condition on determinism that preserves expressiveness by construction of the definition, then applied to operations like complementation. No equations reduce a prediction to a fitted parameter, no load-bearing self-citation chains, and no ansatz or renaming that collapses the central claims back to inputs. The derivation remains self-contained with external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claims rest on standard definitions from automata theory with no fitted numerical parameters; new entities are the VRA model and codeterminism notion, introduced without independent empirical evidence.

axioms (1)
  • standard math Classical definitions of finite automata and recursive call mechanisms
    Invoked to define the base components of VRAs.
invented entities (2)
  • Visibly Recursive Automata (VRAs) no independent evidence
    purpose: Model composed of calling classical automata with visible recursion
    Newly defined model claimed to strictly extend procedural automata.
  • Codeterminism no independent evidence
    purpose: Weaker determinism notion preserving expressiveness and enabling algorithms like complementation
    Newly proposed property used as stepping stone for complementation.

pith-pipeline@v0.9.0 · 5424 in / 1213 out tokens · 35575 ms · 2026-05-15T12:20:52.006734+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

36 extracted references · 36 canonical work pages

  1. [1]

    In: Diekert, V., Volkov, M.V., Voronkov, A

    Alur, R.: Marrying words and trees. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) Computer Science - Theory and Applications, Second International Sympo- sium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-7, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4649, p. 5. Springer (2007).https://doi.org/10.1007/978-...

    work page doi:10.1007/978-3-540-74510-5_3 2007

  2. [2]

    ACM Trans

    Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Program. Lang. Syst.27(4), 786–818 (2005).https://doi.org/10.1145/1075382.1075387

    work page doi:10.1145/1075382.1075387 2005

  3. [3]

    In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M

    Alur, R., Kumar, V., Madhusudan, P., Viswanathan, M.: Congruences for visi- bly pushdown languages. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings. Lec- ture Notes in Computer Science, vol. 3580, p...

    work page doi:10.1007/11523468_89 2005

  4. [4]

    In: Babai, L

    Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) Pro- ceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004. pp. 202–211. ACM (2004).https://doi.org/10.1145/ 1007352.1007390

    work page arXiv 2004

  5. [5]

    Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM56(3), 16:1–16:43 (2009).https://doi.org/10.1145/1516512.1516518

    work page doi:10.1145/1516512.1516518 2009

  6. [6]

    Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987).https://doi.org/10.1016/0890-5401(87)90052-6

    work page doi:10.1016/0890-5401(87)90052-6 1987

  7. [7]

    In: Brauer, W., Ehrig, H., Karhum¨ aki, J., Salomaa, A

    Berstel, J., Boasson, L.: Balanced grammars and their languages. In: Brauer, W., Ehrig, H., Karhum¨ aki, J., Salomaa, A. (eds.) Formal and Natural Computing - Essays Dedicated to Grzegorz Rozenberg [on occasion of his 60th birthday, March 14, 2002], Lecture Notes in Computer Science, vol. 2300, pp. 3–25. Springer (2002). https://doi.org/10.1007/3-540-45711-9_1

    work page doi:10.1007/3-540-45711-9_1 2002

  8. [8]

    In: Mazurkiewicz, A.W., Winkowski, J

    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown au- tomata: Application to model-checking. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) CONCUR ’97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings. Lecture Notes in Computer Science, vol. 1243, pp. 135–150. Springer (1997).https://doi.or...

    work page doi:10.1007/3-540-63141-0_10 1997

  9. [9]

    In: Sankaranarayanan, S., Sharygina, N

    Bruy` ere, V., P´ erez, G.A., Staquet, G.: Validating streaming JSON documents with learned VPAs. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algo- rithms for the Construction and Analysis of Systems - 29th International Confer- ence, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Pa...

    work page doi:10.1007/978-3-031-30823-9_14 2023

  10. [10]

    In: Atluri, V

    Chen, H., Wagner, D.A.: MOPS: an infrastructure for examining security prop- erties of software. In: Atluri, V. (ed.) Proceedings of the 9th ACM Conference on Computer and Communications Security, CCS 2002, Washington, DC, USA, November 18-22, 2002. pp. 235–244. ACM (2002).https://doi.org/10.1145/ 586110.586142

    work page arXiv 2002

  11. [11]

    ACM Trans

    Chiari, M., Mandrioli, D., Pontiggia, F., Pradella, M.: A model checker for operator precedence languages. ACM Trans. Program. Lang. Syst.45(3), 19:1–19:66 (2023). https://doi.org/10.1145/3608443 14 K. Dubrulle, V. Bruy` ere, G. A. P´ erez, G. Staquet

    work page doi:10.1145/3608443 2023

  12. [12]

    In: Silva, A., Leino, K.R.M

    Chiari, M., Mandrioli, D., Pradella, M.: Model-checking structured context-free languages. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 387–410. Springer (2021).https://doi.org/10.1007/978-...

    work page doi:10.1007/978-3-030-81688-9_18 2021

  13. [13]

    Dubrulle, K.: Visibly system of procedural automata validating JSON documents, https://github.com/BlueTorche/VSPA

    work page

  14. [14]

    Master’s thesis, UMONS - Universit´ e de Mons [Facult´ e Poly- technique de Mons], Mons, Belgium (June 2025)

    Dubrulle, K.: Mutually recursive procedural systems - streaming validation of JSON documents. Master’s thesis, UMONS - Universit´ e de Mons [Facult´ e Poly- technique de Mons], Mons, Belgium (June 2025)

    work page 2025

  15. [15]

    In: Kobayashi, N., Pierce, B.C

    Esparza, J., Kucera, A., Schwoon, S.: Model-checking LTL with regular valuations for pushdown systems. In: Kobayashi, N., Pierce, B.C. (eds.) Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2215, pp. 316–339. Springer (2001).https://d...

    work page doi:10.1007/3-540-45500-0_16 2001

  16. [16]

    International Journal on Software Tools for Technology Transfer (2026).https://doi.org/10.1007/ s10009-026-00839-z

    Fortz, S., Ghassemi, F., Henry, L., Howar, F., Neele, T., Rot, J., Suilen, M.: A research agenda for active automata learning. International Journal on Software Tools for Technology Transfer (2026).https://doi.org/10.1007/ s10009-026-00839-z

    work page 2026

  17. [17]

    Frohme, M., Steffen, B.: Compositional learning of mutually recursive procedural systems. Int. J. Softw. Tools Technol. Transf.23(4), 521–543 (2021).https://doi. org/10.1007/S10009-021-00634-Y

    work page doi:10.1007/s10009-021-00634-y 2021

  18. [18]

    Gallier, J.H., La Torre, S., Mukhopadhyay, S.: Deterministic finite automata with recursive calls and DPDAs. Inf. Process. Lett.87(4), 187–193 (2003).https:// doi.org/10.1016/S0020-0190(03)00281-3

    work page doi:10.1016/s0020-0190(03)00281-3 2003

  19. [19]

    Pearson international edition, Addison- Wesley (2007)

    Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, lan- guages, and computation, 3rd Edition. Pearson international edition, Addison- Wesley (2007)

    work page 2007

  20. [20]

    Addison-Wesley (1979)

    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979)

    work page 1979

  21. [21]

    Isberner, M.: Foundations of active automata learning: an algorithmic perspec- tive. Ph.D. thesis, Technical University Dortmund, Germany (2015),https:// hdl.handle.net/2003/34282

    work page 2015

  22. [22]

    Jia, X., Tan, G.: V-Star: Learning visibly pushdown grammars from program in- puts. Proc. ACM Program. Lang.8(PLDI), 2003–2026 (2024).https://doi.org/ 10.1145/3656458

    work page doi:10.1145/3656458 2003

  23. [23]

    In: Williamson, C.L., Zurko, M.E., Patel-Schneider, P.F., Shenoy, P.J

    Kumar, V., Madhusudan, P., Viswanathan, M.: Visibly pushdown automata for streaming XML. In: Williamson, C.L., Zurko, M.E., Patel-Schneider, P.F., Shenoy, P.J. (eds.) Proceedings of the 16th International Conference on World Wide Web, WWW 2007, Banff, Alberta, Canada, May 8-12, 2007. pp. 1053–1062. ACM (2007). https://doi.org/10.1145/1242572.1242714

    work page doi:10.1145/1242572.1242714 2007

  24. [24]

    Lange, M.: P-hardness of the emptiness problem for visibly pushdown languages. Inf. Process. Lett.111(7), 338–341 (2011).https://doi.org/10.1016/J.IPL. 2010.12.013

    work page doi:10.1016/j.ipl 2011

  25. [25]

    Proceedings of the VLDB Endowment19(3), 509–522 (2025)

    Le Glaunec, A., Li, A.W., Mamouras, K.: Streaming validation of JSON documents against schemas. Proceedings of the VLDB Endowment19(3), 509–522 (2025)

    work page 2025

  26. [26]

    In: Fazekas, S.Z

    Martynova, O.: Exact descriptional complexity of determinization of input-driven pushdown automata. In: Fazekas, S.Z. (ed.) Implementation and Application of Automata - 28th International Conference, CIAA 2024, Akita, Japan, September 3-6, 2024, Proceedings. Lecture Notes in Computer Science, vol. 15015, pp. 249–

    work page 2024

  27. [27]

    Springer (2024).https://doi.org/10.1007/978-3-031-71112-1_18 Visibly Recursive Automata 15

    work page doi:10.1007/978-3-031-71112-1_18 2024

  28. [28]

    In: Seffah, A., Penzenstadler, B., Alves, C., Peng, X

    Nguyen, H., Touili, T.: CARET model checking for pushdown systems. In: Seffah, A., Penzenstadler, B., Alves, C., Peng, X. (eds.) Proceedings of the Symposium on Applied Computing, SAC 2017, Marrakech, Morocco, April 3-7, 2017. pp. 1393–

    work page 2017

  29. [29]

    ACM (2017).https://doi.org/10.1145/3019612.3019829

    work page doi:10.1145/3019612.3019829 2017

  30. [30]

    SIGACT News45(2), 47–67 (2014).https://doi.org/10.1145/2636805.2636821

    Okhotin, A., Salomaa, K.: Complexity of input-driven pushdown automata. SIGACT News45(2), 47–67 (2014).https://doi.org/10.1145/2636805.2636821

    work page doi:10.1145/2636805.2636821 2014

  31. [31]

    PWS Publishing Company (1997)

    Sipser, M.: Introduction to the theory of computation. PWS Publishing Company (1997)

    work page 1997

  32. [32]

    Song, F., Touili, T.: Pushdown model checking for malware detection. Int. J. Softw. Tools Technol. Transf.16(2), 147–173 (2014).https://doi.org/10.1007/ S10009-013-0290-1

    work page 2014

  33. [33]

    Com- mun

    Woods, W.A.: Transition network grammars for natural language analysis. Com- mun. ACM13(10), 591–606 (1970).https://doi.org/10.1145/355598.362773

    work page doi:10.1145/355598.362773 1970

  34. [34]

    Yu, S., Zhuang, Q., Salomaa, K.: The state complexities of some basic operations on regular languages. Theor. Comput. Sci.125(2), 315–328 (1994).https://doi. org/10.1016/0304-3975(92)00011-F 16 K. Dubrulle, V. Bruy` ere, G. A. P´ erez, G. Staquet A Basic Properties of VRAs In this appendix, we first highlight a basic property of VRAs that can help to bett...

    work page doi:10.1016/0304-3975(92)00011-f 1994

  35. [35]

    This impliesq 4 =q ′ 3 andq 5 =q ′

    Additionally, from the configuration⟨q 0, ε⟩, the recursive run onccmust be unique, therefore⟨q 2, q4 ·q 5⟩=⟨q ′ 2, q′ 3 ·q ′ 5⟩. This impliesq 4 =q ′ 3 andq 5 =q ′

    work page

  36. [36]

    Thus, we can deduce the existence of the following recursive run: ⟨q0, ε⟩ cc− → ⟨q2, q4 ·q 5⟩ ar− → ⟨q4, q5⟩=⟨q ′ 3, q′ 5⟩ ar− → ⟨q′ 5, ε⟩ ∈Π(B). Since this recursive run is accepting, it follows thatccarar∈ eL(B), which is a contradiction sinceccarar /∈eL(A).⊓ ⊔ C Systems of Procedural Automata Frohme and Steffen introduced in [17] the model ofsystem of ...

    work page