pith. sign in

arxiv: 2210.08298 · v5 · submitted 2022-10-15 · 💻 cs.FL

Myhill-Nerode Theorem for Higher-Dimensional Automata

Uli Fahrenberg , Krzysztof Ziemia\'nski This is my paper

Pith reviewed 2026-05-24 11:11 UTC · model grok-4.3

classification 💻 cs.FL
keywords higher-dimensional automataMyhill-Nerode theoremregular languagesprefix quotientdeterministic HDAsconcurrency modelingautomata with interfaces
0
0 comments X

The pith

A language recognized by a higher-dimensional automaton is regular if and only if its prefix quotient is finite.

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

The paper proves an extension of the classical Myhill-Nerode theorem to higher-dimensional automata, which add structure to model true concurrency rather than just interleaving. It shows that regularity of a language is equivalent to the language having only finitely many distinct prefixes up to future behavior. The same framework yields an internal characterization of those languages that admit deterministic recognition and extends the results to automata equipped with interfaces. A sympathetic reader would care because the theorem supplies a structural test for regularity that does not require constructing an automaton explicitly.

Core claim

We establish a Myhill-Nerode type theorem for higher-dimensional automata (HDAs), stating that a language is regular if and only if it has finite prefix quotient. We also introduce deterministic HDAs and show that not all HDAs are determinizable, that is, there exist regular languages that cannot be recognised by a deterministic HDA. Using our theorem, we develop an internal characterisation of deterministic languages. Lastly, we develop analogues of the Myhill-Nerode construction and of determinacy for HDAs with interfaces.

What carries the argument

The prefix quotient of an HDA language, which partitions words according to the sets of possible future extensions they admit.

If this is right

  • Regularity of an HDA language can be decided by checking finiteness of its prefix quotient.
  • There exist regular HDA languages with no deterministic HDA recognizer.
  • Deterministic HDA languages admit an internal characterization derived from the finite-quotient property.
  • The Myhill-Nerode construction and the determinacy result both lift to HDAs equipped with interfaces.

Where Pith is reading between the lines

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

  • The finite-quotient test could be turned into a practical minimization procedure for HDAs that avoids explicit state explosion from concurrency.
  • The non-determinizability result suggests that verification algorithms for concurrent systems may need to retain nondeterminism even when the underlying language is regular.
  • Interface-aware versions of the theorem may connect to compositional reasoning about open concurrent systems.

Load-bearing premise

The definitions of regularity and of prefix quotient for HDAs are set up so that the classical equivalence proof carries over without further restrictions on the higher-dimensional cells.

What would settle it

An explicit HDA language whose prefix quotient is infinite yet which satisfies the paper's definition of regularity, or vice versa.

Figures

Figures reproduced from arXiv: 2210.08298 by Krzysztof Ziemia\'nski, Uli Fahrenberg.

Figure 1
Figure 1. Figure 1: Petri net and HDA models distinguishing interleaving from non-interleaving concurrency. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Activity intervals (top) and corresponding iposets (bottom), see Example 2.1. Full arrows [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Sparse decomposition of ipomset into starters and terminators. [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A two-dimensional HDA X on Σ = {a, b}, see Example 4.2. Example 4.2 [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: HDA Y consisting of three squares glued along common faces. Example 4.6. The event ipomsets of the five sparse accepting paths in the HDA X of [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: HDA MN(L) of Example 5.5, showing names of cells instead of labels (labels are target interfaces of names). Tables show essential cells together with prefix quotients. Example 5.5. Let L = {[ a b ] , abc}↓ = {[ a b ] , ab, ba, abc} [PITH_FULL_IMAGE:figures/full_fig_p015_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Two HDAs recognising the language of Example 5.23. On the left side, start/accept edges [PITH_FULL_IMAGE:figures/full_fig_p020_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: An example of an iHDA. Cells are marked with their event iconclists. [PITH_FULL_IMAGE:figures/full_fig_p025_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: iFree(L) for L = {[ a b ] , abc}↓, see Example 8.7. 8.3. iMN(L) The iHDA iFree(L) is infinite as soon as L is. (It contains at least one accept cell for every element of L.) Analogously to the construction in Section 5.1, we introduce an equivalence relation depending on L. Now however, the relation is not defined on ipomsets but directly on iFree(L). In order for the quotient iHDA to be well-defined, we w… view at source ↗
Figure 10
Figure 10. Figure 10: iMN(L) for L = {•a•} ∪ {[ •aa• b ] n | n ≥ 1}↓, see Example 8.13. 8.5. iMN(L) recognises L For a cell x ∈ iMN(L) denote x \L := P \ Z L for any (P, Z) ∈ x. This clearly does not depend on the choice of a representative. Lemma 8.14. Assume that x ∈ iMN(L)[SUT ], A ⊆ U − S, B ⊆ U − T. Then 1. Q ∈ x \L =⇒ A↑U ∗ Q ∈ δ 0 A (x) \L, 2. U↓B ∗ Q ∈ x \L ⇐⇒ Q ∈ δ 1 B (x) \L. Proof: Fix (P, Z) ∈ x. Recall that (SQ, S… view at source ↗
read the original abstract

We establish a Myhill-Nerode type theorem for higher-dimensional automata (HDAs), stating that a language is regular if and only if it has finite prefix quotient. HDAs extend standard automata with additional structure, making it possible to distinguish between interleavings and concurrency. We also introduce deterministic HDAs and show that not all HDAs are determinizable, that is, there exist regular languages that cannot be recognised by a deterministic HDA. Using our theorem, we develop an internal characterisation of deterministic languages. Lastly, we develop analogues of the Myhill-Nerode construction and of determinacy for HDAs with interfaces.

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 / 2 minor

Summary. The paper establishes a Myhill-Nerode theorem for higher-dimensional automata (HDAs): a language is regular (accepted by some HDA) if and only if its prefix quotient is finite. It introduces deterministic HDAs, proves that not every regular language is accepted by a deterministic HDA, derives an internal characterization of deterministic languages from the theorem, and develops analogues of the Myhill-Nerode construction and determinacy for HDAs with interfaces.

Significance. If the central equivalence holds, the result supplies a language-theoretic characterization of regularity for a model that distinguishes true concurrency from interleaving, extending classical automata theory in a direct and usable way. The non-determinizability result is a substantive distinction from ordinary finite automata. The internal characterization and the interface extensions increase the theorem's applicability. The paper's strength lies in adapting the classical bijection construction without introducing extra restrictions on higher-dimensional cells.

minor comments (2)
  1. [Abstract] Abstract: the statement of the main theorem and the non-determinizability result would be clearer if the abstract briefly indicated that the proof adapts the standard state-equivalence construction.
  2. The definitions of prefix quotient and deterministic acceptance (presumably in the sections following the introduction) would benefit from one concrete low-dimensional example that illustrates how the higher-dimensional cells affect the equivalence classes.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive report, the accurate summary of our contributions, and the recommendation to accept the paper. The assessment correctly identifies the main results on the Myhill-Nerode theorem for HDAs, the separation between deterministic and nondeterministic HDAs, the internal characterization, and the extensions to interfaces.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's central result is a direct adaptation of the classical Myhill-Nerode theorem to HDAs, where regularity is defined via acceptance by HDAs and the prefix quotient is defined on the language such that the standard bijection between states and equivalence classes lifts without additional restrictions. The proof constructs the equivalence explicitly from these definitions rather than reducing to any fitted input, self-citation chain, or renamed prior result. The separate non-determinizability result and internal characterisation of deterministic languages are derived consequences that do not feed back into the core equivalence. No load-bearing step reduces by construction to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The result rests on the standard definitions of HDAs and languages already present in the literature; no new free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Standard definitions of higher-dimensional automata and their languages from prior work
    The theorem is stated relative to those definitions.

pith-pipeline@v0.9.0 · 5626 in / 1054 out tokens · 20668 ms · 2026-05-24T11:11:34.741682+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

33 extracted references · 33 canonical work pages · 1 internal anchor

  1. [1]

    Modeling Concurrency with Geometry

    Pratt VR. Modeling Concurrency with Geometry. In: POPL. ACM Press, New York City, 1991 pp. 311–322

    work page 1991

  2. [2]

    Bisimulations for Higher Dimensional Automata

    van Glabbeek RJ. Bisimulations for Higher Dimensional Automata. Email message, 1991. http:// theory.stanford.edu/~rvg/hda

    work page 1991

  3. [3]

    On the Expressiveness of Higher Dimensional Automata

    van Glabbeek RJ. On the Expressiveness of Higher Dimensional Automata. Theoretical Computer Sci- ence, 2006. 356(3):265–290. See also [31]

    work page 2006

  4. [4]

    Kommunikation mit Automaten

    Petri CA. Kommunikation mit Automaten. Number 2 in Schriften des IIM. Institut für Instrumentelle Mathematik, Bonn, 1962

    work page 1962

  5. [5]

    Petri Nets, Event Structures and Domains, Part I

    Nielsen M, Plotkin GD, Winskel G. Petri Nets, Event Structures and Domains, Part I. Theoretical Com- puter Science, 1981. 13:85–108

    work page 1981

  6. [6]

    Configuration Structures

    van Glabbeek RJ, Plotkin GD. Configuration Structures. In: LICS. IEEE Computer Society, 1995 pp. 199–209. doi:10.1109/LICS.1995.523257. URL http://doi.ieeecomputersociety.org/10.1109/ LICS.1995.523257

    work page doi:10.1109/lics.1995.523257 1995

  7. [7]

    Configuration Structures, Event Structures and Petri Nets

    van Glabbeek RJ, Plotkin GD. Configuration Structures, Event Structures and Petri Nets. Theoretical Computer Science, 2009. 410(41):4111–4159. doi:10.1016/j.tcs.2009.06.014. URL http://dx.doi. org/10.1016/j.tcs.2009.06.014. 1https://ulifahrenberg.github.io/pomsetproject/ 258 U. Fahrenberg and K. Ziemia´ nski/ Myhill-Nerode Theorem for Higher-Dimensional Automata

    work page doi:10.1016/j.tcs.2009.06.014 2009

  8. [8]

    Categories of Asynchronous Systems

    Bednarczyk MA. Categories of Asynchronous Systems. Ph.D. thesis, University of Sussex, UK, 1987

    work page 1987

  9. [9]

    Concurrent Machines

    Shields MW. Concurrent Machines. Comput. J., 1985. 28(5):449–465

    work page 1985

  10. [10]

    Chu Spaces and their Interpretation as Concurrent Objects

    Pratt VR. Chu Spaces and their Interpretation as Concurrent Objects. In: Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science , pp. 392–405. Springer, 1995

    work page 1995

  11. [11]

    Refinement of actions and equivalence notions for concurrent systems

    van Glabbeek RJ, Goltz U. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 2001. 37(4/5):229–327

    work page 2001

  12. [12]

    Transition And Cancellation In Concurrency And Branching Time

    Pratt VR. Transition And Cancellation In Concurrency And Branching Time. Mathematical Structures in Computer Science, 2003. 13(4):485–529

    work page 2003

  13. [13]

    ST-Structures

    Johansen C. ST-Structures. Journal of Logic and Algebraic Methods in Programming, 2015. 85(6):1201–

    work page 2015

  14. [14]

    Extensions of Configuration Structures

    doi:\url{10.1016/j.jlamp.2015.10.009}. https://arxiv.org/abs/1406.0641

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1016/j.jlamp.2015.10.009 2015

  15. [15]

    Languages of Higher-Dimensional Automata

    Fahrenberg U, Johansen C, Struth G, Ziemia ´nski K. Languages of Higher-Dimensional Automata. Math- ematical Structures in Computer Science , 2021. 31(5):575–613. doi:10.1017/S0960129521000293. https://arxiv.org/abs/2103.07557, URL https://doi.org/10.1017/S0960129521000293

    work page doi:10.1017/s0960129521000293 2021

  16. [16]

    A Kleene Theorem for Higher-Dimensional Au- tomata

    Fahrenberg U, Johansen C, Struth G, Ziemia ´nski K. A Kleene Theorem for Higher-Dimensional Au- tomata. In: Klin B, Lasota S, Muscholl A (eds.), CONCUR, volume 243 of Leibniz International Pro- ceedings in Informatics (LIPIcs). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. ISBN 978-3-95977- 246-4, 2022 pp. 29:1–29:18. doi:10.4230/LIPIcs.CONCUR.2022.2...

    work page doi:10.4230/lipics.concur.2022.29 2022

  17. [17]

    Kleene Theorem for Higher-Dimensional Automata

    Fahrenberg U, Johansen C, Struth G, Ziemia ´nski K. Kleene Theorem for Higher-Dimensional Automata. CoRR, 2022. abs/2202.03791. https://arxiv.org/abs/2202.03791. Long version of [15], 2202. 03791, URL https://arxiv.org/abs/2202.03791

    work page arXiv 2022

  18. [18]

    A Myhill-Nerode Theorem for Higher-Dimensional Automata

    Fahrenberg U, Ziemia ´nski K. A Myhill-Nerode Theorem for Higher-Dimensional Automata. In: Gomes L, Lorenz R (eds.), PETRI NETS, volume 13929 of Lecture Notes in Computer Science . Springer, 2023 pp. 167–188. doi:10.1007/978-3-031-33620-1\_9. URL https://doi.org/10.1007/ 978-3-031-33620-1_9

    work page doi:10.1007/978-3-031-33620-1 2023

  19. [19]

    Interval Orders and Interval Graphs: A Study of Partially Ordered Sets

    Fishburn PC. Interval Orders and Interval Graphs: A Study of Partially Ordered Sets. Wiley, 1985. ISBN 9780471812845

    work page 1985

  20. [20]

    On partial languages

    Grabowski J. On partial languages. Fundamentae Informatica, 1981. 4(2):427

    work page 1981

  21. [21]

    Posets With Interfaces as a Model for Concurrency

    Fahrenberg U, Johansen C, Struth G, Ziemia ´nski K. Posets With Interfaces as a Model for Concurrency. Information and Computation, 2022. 285(B):104914. doi:10.1016/j.ic.2022.104914. https://arxiv. org/abs/2106.10895, URL https://doi.org/10.1016/j.ic.2022.104914

    work page doi:10.1016/j.ic.2022.104914 2022

  22. [22]

    Structure of Concurrency

    Janicki R, Koutny M. Structure of Concurrency. Theoretical Computer Science , 1993. 112(1):5–52. doi:10.1016/0304-3975(93)90238-O. URL https://doi.org/10.1016/0304-3975(93)90238-O

    work page doi:10.1016/0304-3975(93)90238-o 1993

  23. [23]

    Operational Semantics, Interval Orders and Sequences of Antichains

    Janicki R, Koutny M. Operational Semantics, Interval Orders and Sequences of Antichains. Fundamentae Informatica, 2019. 169(1-2):31–55. doi:10.3233/FI-2019-1838. URL https://doi.org/10.3233/ FI-2019-1838

    work page doi:10.3233/fi-2019-1838 2019

  24. [24]

    Closure and Decision Properties for Higher- Dimensional Automata

    Amrane A, Bazille H, Fahrenberg U, Ziemia ´nski K. Closure and Decision Properties for Higher- Dimensional Automata. In: Ábrahám E, Dubslaff C, Tarifa SLT (eds.), ICTAC, volume 14446 of Lecture Notes in Computer Science. Springer, 2023 pp. 295–312. doi:10.1007/978-3-031-47963-2\_18. https: //arxiv.org/abs/2305.02873, URL https://doi.org/10.1007/978-3-031-...

    work page doi:10.1007/978-3-031-47963-2 2023

  25. [25]

    Partial Higher-dimensional Automata

    Fahrenberg U, Legay A. Partial Higher-dimensional Automata. In: Moss LS, Sobocinski P (eds.), CALCO, volume 35 of Leibniz International Proceedings in Informatics . Schloss Dagstuhl - Leibniz- Zentrum für Informatik. ISBN 978-3-939897-84-2, 2015 pp. 101–115. doi:10.4230/LIPIcs.CALCO. 2015.101. URL http://dx.doi.org/10.4230/LIPIcs.CALCO.2015.101

    work page doi:10.4230/lipics.calco 2015

  26. [26]

    Trees in Partial Higher Dimensional Automata

    Dubut J. Trees in Partial Higher Dimensional Automata. In: Boja ´nczyk M, Simpson A (eds.), FOSSACS, volume 11425 of Lecture Notes in Computer Science. Springer. ISBN 978-3-030-17126-1, 2019 pp. 224–

    work page 2019

  27. [27]

    URL https://doi.org/10.1007/978-3-030-17127-8_ 13

    doi:10.1007/978-3-030-17127-8\_13. URL https://doi.org/10.1007/978-3-030-17127-8_ 13

    work page doi:10.1007/978-3-030-17127-8

  28. [28]

    When a Little Nondeterminism Goes a Long Way: An Introduction to History- Determinism

    Boker U, Lehtinen K. When a Little Nondeterminism Goes a Long Way: An Introduction to History- Determinism. ACM SIGLOG News, 2023. 10(1):24–51. doi:10.1145/3584676.3584682. URL https: //doi.org/10.1145/3584676.3584682

    work page doi:10.1145/3584676.3584682 2023

  29. [29]

    Residual Finite State Automata

    Denis F, Lemay A, Terlutte A. Residual Finite State Automata. In: Ferreira A, Reichel H (eds.), STACS, volume 2010 of Lecture Notes in Computer Science . Springer, 2001 pp. 144–157. doi: 10.1007/3-540-44693-1\_13. URL https://doi.org/10.1007/3-540-44693-1_13

    work page doi:10.1007/3-540-44693-1 2010

  30. [30]

    Learning regular sets from queries and counterexamples

    Angluin D. Learning Regular Sets from Queries and Counterexamples. Information and Computa- tion, 1987. 75(2):87–106. doi:10.1016/0890-5401(87)90052-6. URL https://doi.org/10.1016/ 0890-5401(87)90052-6

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

  31. [31]

    Angluin-Style Learning of NFA

    Bollig B, Habermehl P, Kern C, Leucker M. Angluin-Style Learning of NFA. In: Boutilier C (ed.), IJCAI. 2009 pp. 1004–1009. URL http://ijcai.org/Proceedings/09/Papers/170.pdf

    work page 2009

  32. [32]

    Learning Pomset Automata

    van Heerdt G, Kappé T, Rot J, Silva A. Learning Pomset Automata. In: Kiefer S, Tasson C (eds.), FOSSACS, volume 12650 of Lecture Notes in Computer Science . Springer, 2021 pp. 510–530. doi:10. 1007/978-3-030-71995-1\_26. URL https://doi.org/10.1007/978-3-030-71995-1_26

    work page doi:10.1007/978-3-030-71995-1_26 2021

  33. [33]

    On the Expressiveness of Higher Dimensional Automata

    van Glabbeek RJ. Erratum to “On the Expressiveness of Higher Dimensional Automata”. Theoretical Computer Science, 2006. 368(1-2):168–194

    work page 2006