Formal Languages and Automata Theory Papers@FormalLanguages
Nov 11
The Left Ripple of Byte-Pair Encoding: Certified Lookbehind for Every Dictionary

Nicklas NidhΓΆgg
arxiv.org/abs/2611.13061 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙲𝙻 𝚌𝚜.π™³πš‚ 𝚌𝚜.𝙿𝙻]
Berglund and van der Merwe formalized byte-pair encoding and bounded how far an appended string can change a tokenization, leaving the converse open: how far can a string prepended on the left change it, which dictionaries make that ripple infinite, and can it be computed efficiently when finite? We answer all three for every dictionary. The origin radius, how far a prepend can change covering spans, is decided with radius certificates by a product of two runs of the automaton that guesses the final tokens, in time polynomial in the dictionary written out, and it is infinite exactly when one periodic word has two canonical tilings with no common boundary. Under their ordering condition it is infinite exactly when some rule (t, t) finds its two copies adjacent at its own stage, and such a rule makes any dictionary infinite. A finite radius makes every window of a width read off the radii have a cut, and the radius is finite exactly when such cuts are dense. The token machine completes f
0
0
0
24
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 10
Two barriers for minimal time firing squads, with applications to four and five states

Kia Keng Giam
arxiv.org/abs/2611.11080 [𝚌𝚜.𝙡𝙻 πš—πš•πš’πš—.𝙲𝙢]
A minimal-time solution of the firing squad synchronization problem synchronizes every line of n cells at time 2n minus 2. Six states suffice; whether five do has been open since 1987. Every line agrees with the half line until its right ends echo returns. For minimal time solutions with any number of states, we prove that cells at distance j behind the half lines front become time-periodic only after time (1.5 minus epsilon)j, for every epsilon greater than 0 and infinitely many j, and that the half line is never periodic in time and space on a wedge at its left border, hence not eventually regular in our sense. With certified satisfiability checks, we exclude four states using the lines of lengths 2 to 5 and parts of the next five, and show that every five state minimal time solution uses at least 15 non quiescent neighbourhoods on its half lines first 78 anti-diagonals. We give five state rules synchronizing exactly the lengths 2 to 14.
0
0
1
47
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 10
Towards A Parametrized Complexity of Determinization

Ivan Baburin, Ryan Cotterell
arxiv.org/abs/2611.10911 [𝚌𝚜.𝙡𝙻]
Given a nondeterministic finite automaton (NFA), we want to estimate the difficulty of finding an equivalent deterministic finite automaton (DFA). We demonstrate that computing the state complexity of an NFA within polynomial precision is PSPACE-hard, and furthermore the same holds for the complexity of the subset construction, Brzozowski's algorithm, or, indeed, any determinization algorithm which runs at least as fast. This result implies that making any a priori estimate of the running time of the major determinization algorithms is inherently hard. To circumvent thisβ€”in the spirit of parametrized complexityβ€”we try to identify complexity measures which can guarantee efficient determinization. Our main idea rests on linking the complexity of the subset construction to transition monoids using the semigroup complexity. We show that the semigroup complexity by itself can be reasonably approximated for certain classes of NFAs, and then introduce subset complexityβ€”a refinement of the sem
0
1
0
54
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 10
Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches

MikoΕ‚aj BojaΕ„czyk, Antonio Casares, Sven Manthe, PaweΕ‚ Parys
arxiv.org/abs/2611.10136 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙻𝙾]
Rabin's Tree Theorem says that the MSO theory of the infinite binary tree 2* is decidable. Shelah showed that MSO logic becomes undecidable if this tree is extended to 2≀ω, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in 2≀ω by restricting set quantification to Borel sets. We make some progress in this direction, by identifying a suitable automaton model, and showing that most of the automata-theoretic approach to Rabin's Theorem can be extended to the new framework. The only missing part is a conjecture about finite-memory determinacy in certain games. This paper states and explores the conjecture. We prove it in some restricted cases, and give lower bounds on the memory required in those games.
0
0
0
20
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 9
Word Subtraction Games

Yusuke Inoue, Hiroki Inazu
arxiv.org/abs/2611.09157 [𝚌𝚜.𝙡𝙻]
This note is a self-contained text on word subtraction games, combinatorial games in which players alternately remove a nonempty suffix belonging to a prescribed subtraction set from the current word. It collects and develops basic results on these games from the viewpoints of combinatorial game theory and formal language theory. We focus on the relationship between subtraction sets and the resulting languages of winning and losing positions. The topics include finite, regular, and context-free subtraction sets, as well as several variants and further developments.
0
0
1
35
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 9
Shortest Synchronizing Words on Product Automata

Henning Fernau, Igor Rystsov
arxiv.org/abs/2611.09136 [𝚌𝚜.𝙡𝙻]
We consider some operations on finite automata graphs, in particular various product, union and merge operations, and investigate how they relate to the parameter rt, the length of a shortest synchronizing word. We derive some lower and upper bounds for the operations that we study. We also examine several classes of automata (for instance, partially ordered, commutative or idempotent automata) that are preserved under these operations and show in which way the parameter rt behaves in these automata classes. Also, we consider automata classes that can be constructed by combining automata from better known classes; in particular, these new classes of automata will also satisfy the bound of the famous Černý conjecture. This also motivates us to study even more closure properties. In particular, we show that certain automata classes related to synchronization form pseudo-varieties. We also commence a similar study concerning the length of shortest homing sequences of Mealy automata.
0
1
1
64
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 6
Reliability-Aware Z-Grammars and Z-Automata over a Credible-Grade Semiring

Sherzod Turaev, Nor Haniza Sarmin, Wan Heng Fong
arxiv.org/abs/2611.07781 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙻𝙾]
Fuzzy grammars and weighted automata usually attach to each word a single grade, which records how strongly the word is generated but not how far that record can be trusted. We study weighted grammars and finite automata whose weights are scalar grade-reliability pairs inspired by Z-numbers. Sequential composition multiplies both components, while aggregation selects a derivation by its credible grade, the product of grade and reliability, with ties resolved by grade. On the canonical carrier, in which the weights of zero grade or zero reliability are identified with zero, the resulting structure is a commutative selective semiring, isomorphic to a subsemiring of a lexicographically ordered product, and its credible-grade projection is a homomorphism onto the Viterbi semiring. We compare several alternative combination rules and identify the carriers on which the relevant algebraic laws hold. Standard results on weighted automata then yield a rational characterization and closure prope
0
0
1
16
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 5
Quadratic reset bounds for finite maximal prefix codes

Samrath Singh Chadha
arxiv.org/abs/2611.05675 [𝚌𝚜.𝙡𝙻]
Let C be a finite maximal prefix code of maximum codeword length kβ‰₯2. We prove that, whenever the literal decoder of C is synchronizing, it has a reset word of length at most (k-1)(4k-5). The bound is independent of the alphabet and the number of decoder states. Its main ingredient is a short-detection theorem: a linear observation of the decoder, with terminal weight constant on states of depth k-1, is either identically zero or nonzero on a word of length at most 2k-3. The proof uses a first-return decomposition in noncommuting variables and cancellation of a highest-degree coefficient. For codes whose codeword lengths are k-1 and k, we prove the sharper bound 2(k-1)Β²-1 and characterize equality. The binary code with the single short word aᡏ⁻¹ attains this bound for every kβ‰₯2; an age representation and a potential on circular arcs give the matching lower bound. Both upper bounds yield polynomial-time constructions in the explicit code size. The mathematical results and the algorithms
0
0
0
29
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 3
Regular Separability for Bidirected VASS

Łukasz Orlikowski, Georg Zetzsche
arxiv.org/abs/2611.03313 [𝚌𝚜.𝙡𝙻]
The regular separability problem asks, given two languages, whether there exists a regular language that contains one of them and is disjoint from the other. We study regular separability for bidirected VASS. We first show that the problem remains Ackermann-complete when the input consists of two languages recognised by bidrected VASS. To find a subclass of VASS in which the problem has lower complexity we define alphabetically bidirected VASS as ones where bidirectedness is also visible in the input letters. Our main result establishes that regular separability for alphabetically bidirected VASS is EXPSPACE-complete. The key to this result is that, in this setting, regular separability coincides with disjointness. As a first ingredient in this equivalence, we also show that for alphabetically bidirected Z-VASS, regular separability and disjointness are equivalent. Consequently, regular separability for these systems is in polynomial-time. In fact, it is log-space inter-reducible with
0
0
0
31
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 3
The Scope Grammar of Natural-Language Rules: Counting and Enumerating Readings modulo Logical Equivalence

Sherzod Turaev, Mary John
arxiv.org/abs/2611.01825 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙲𝙻 𝚌𝚜.𝙻𝙾]
A rule written for people fixes its atomic conditions and connectives but leaves open how the connectives are bracketed, and each bracketing is a different logical reading that an autoformalizer must resolve or expose. We study the scope grammar, a deliberately ambiguous context-free grammar whose derivation trees are the readings of a connective skeleton and whose quotient by logical equivalence is what matters downstream. A skeleton with k binary connectives has Cβ‚– derivation trees, the k-th Catalan number, but far fewer logically distinct readings. For the positive, repetition-free fragment we make the gap exact: through the uniqueness of the read-once normal form we characterize the realizable normal forms by lowest common ancestors and count them with a two-label recurrence over the operator word, verified against exhaustive enumeration up to eleven atoms. The count is invariant under reversal and ∧/∨ duality; a skeleton is ambiguous if and only if it uses both ∧ and ∨, a one-pass
0
0
0
23
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 3
Classification of non-Leibnizian Strings

Furkan Semih DΓΌndar
arxiv.org/abs/2611.01625 [𝚌𝚜.𝙡𝙻]
Leibnizian ideas in foundations of physics has enjoyed a renewed interest. Cyclic string ontology in Wolfram Model multiway rewriting systems has been found to encode finite dimensional quantum systems where what are called as Leibnizian strings have been employed. It has then become important to classify strings in terms of their ability to correspond to a monadic interpretation Γ  la Leibniz. The definition of Leibnizian strings are rather quite non-linear and for that purpose we classify non-Leibnizian strings for which there is a simpler criterion on maximal neighborhoods of characters. If a string is not non-Leibnizian then it must be Leibnizian. We found out three canonical forms of non-Leibnizian strings and noted that two of them are context-free languages whereas one is not.
0
0
0
15
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 3
On Small Universal Reversible Turing Machines

T. Yokoyama
arxiv.org/abs/2611.00153 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙻𝙾]
πŸ’¬Code: github.com/yokoyama-lab/s…
A reversible Turing machine (RTM) is a Turing machine in which every instantaneous description has at most one predecessor. Writing URTM(m,n) for a universal RTM with m states and n symbols, we construct URTM(3,600), URTM(4,41), URTM(5,37), URTM(6,30), URTM(7,28), URTM(8,21), and URTM(85,2); each of them has fewer states or fewer symbols than each of the nine URTMs in Morita's book (2017). They come from improved versions of Morita's conversions to three states, to four states, and to two symbols; for example, the improved conversion to three states uses O(mnΒ²) symbols instead of O(mΒ²nΒ³). We also show that the halting problem of RTMs with at most two states is decidable for finite instantaneous descriptions, so that no RTM with at most two states is universal under any notion of universality that reduces the halting problem of Turing machines to it by a computable encoding into finite instantaneous descriptions; in particular, there is no URTM with at most two states in our formalizati
0
0
1
79
Formal Languages and Automata Theory Papers@FormalLanguages
Nov 2
General semiring conditions for weighted L* termination

Noah Bertram, Daniel Luckhardt, Alexandra Silva
arxiv.org/abs/2610.41184 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙻𝙾]
Weighted automata learning has been well-studied over (semi)rings which have a dimension theory. In this work, we investigate active learning for weighted automata over semirings that lack such a structure. We first show that the principal ideal domain variant of the L* algorithm also terminates for a larger class of semirings containing Noetherian semirings, commutative rings, and bounded distributed lattices. We then present a variant of this algorithm for learning deterministic weighted automata, and prove that this algorithm terminates for commutative semirings.
0
1
2
127
Formal Languages and Automata Theory Papers@FormalLanguages
Oct 30
Reachability in Five-Dimensional Vector Addition Systems Is PSPACE-Complete

Weijun Chen, Bo Fu, Yuxi Fu
arxiv.org/abs/2610.40012 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙲𝙲]
Vector addition systems (VAS) are a fundamental model of concurrent computation in which transitions update nonnegative integer counters by adding integer vectors, provided all counters remain nonnegative. Closely related to Petri nets, VAS are the single-state counterpart of vector addition systems with states (VASS), which use finitely many states to restrict the available transitions. A classical simulation of d-VASS by (d+3)-VAS connects their reachability problems, but the complexity-theoretic picture of fixed-dimensional VAS remains largely unclear. While reachability in 2-VASS is PSPACE-complete under binary encoding, the best known upper bound for 5-VAS was only elementary. We prove that every reachable 5-VAS instance has a reachability witness of length polynomial in its unary size. Consequently, 5-VAS reachability is NL-complete under unary encoding and PSPACE-complete under binary encoding. We also establish a polynomial factorization of the reachability relation of every d-
0
0
1
61
Formal Languages and Automata Theory Papers@FormalLanguages
Oct 30
Block-exchange descent for insertion: commuting projections and minimum masks

Haobo Ma, Wenlin Zhang, Charles E. Hughes
arxiv.org/abs/2610.39941 [𝚌𝚜.𝙡𝙻 πš–πšŠπšπš‘.𝙲𝙾]
πŸ’¬Code: github.com/the-omega-inst…
For fixed nonempty words u,v, the minimum insertion degree of a shuffle is the least number of inserted-source runs among its representations. We prove that, after a block exchange from a minimum mask of degree r, the minimum over masks with commuting source projections is exactly r-1; a larger decrease occurs precisely when a noncommuting mask has fewer runs. If either source is unary, every such exchange is exact. We prove an explicit repair for an infinite periodic degree-three family. Computer-assisted results establish first-mask descent through combined length seventeen over every alphabet, degree-three first-mask descent through length thirty, and a uniform repair of all degree-three failures through length thirty, including all further letter identifications. Counterexamples to arbitrary, first, and last minimum-mask choices explain the need for alternative masks. Finally, we prove that minimum iteration depths have no gaps for arbitrary languages. General block-exchange descen
0
0
0
29
Formal Languages and Automata Theory Papers@FormalLanguages
Oct 30
Exact Avoid-or-Compress Extrema for Dense Reachable Images: Defects Four and Five

Qichao Wang, Daoyu Dong
arxiv.org/abs/2610.39833 [𝚌𝚜.𝙡𝙻 πš–πšŠπšπš‘.𝙲𝙾]
Let S be a reachable image of a strongly connected synchronizing automaton and βˆ…β‰  A⊊ S. We determine the maximum shortest avoid-or-compress length over binary and arbitrary finite alphabets for m=n-|S|=4 and m=5. The exact values are min(n-|A|,11) and min(n-|A|,14), respectively. Uniform binary constructions attain both bounds. For the upper bounds, short-pair graphs and actual-image constraints reduce all parameters to finite necessary domains. Exhaustive checks exclude the domains, apart from a single relaxation eliminated by a multipartite overlap lemma. The largest calculation covers 3,206,988 domains.
0
0
0
22
Formal Languages and Automata Theory Papers@FormalLanguages
Oct 30
Tree Equivalence of Higher-Order Recursion Schemes Is Undecidable

Mingkun Xiao, Yixuan Sun
arxiv.org/abs/2610.39678 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙻𝙾]
Higher-order recursion schemes (HORS) are finite, simply typed recursive programs that generate potentially infinite trees. Their monadic second-order model-checking problem is decidable. We prove that tree equivalence of deterministic HORS is undecidable and, more precisely, Π⁰₁-complete under total computable many-one reductions. The lower bound holds for safe, productive schemes of order at most four over the fixed ranked alphabet Ξ£β‚‚={e:0,d:2}, consisting of one nullary and one binary symbol. Adapting the counter-guard witness of Boiret, Piorkowski, and Schmude, we generate all candidate executions of a two-counter machine by producing both continuations at every counter test. An integer weight is nonzero exactly on legal prefixes. Functions at fixed simple types represent the polynomial of growing degree. A shift recurrence updates them without storing a separate step counter, allowing the witness to be implemented by safe applicative HORS rules. At candidate halts, the intermediat
0
0
0
38
Formal Languages and Automata Theory Papers@FormalLanguages
Oct 27
Verse: Semantics and Verification of Hybrid Multi-Agent Scenarios

Yangge Li, Katherine Braught, Alex Yuan, Sayan Mitra
arxiv.org/abs/2610.35680 [𝚌𝚜.𝙡𝙻]
Verifying cyber-physical systems with many interacting agents remains difficult because interactions are mediated by sensors, individual decisions are constrained by environment (map) structure, and the resulting mode space scales combinatorially. We present Verse, a framework for writing agents, maps, and sensors in a familiar programming language syntax, with a formal semantics for the resulting scenarios. A compiler translates each scenario to a hybrid automaton whose executions correspond exactly to the runs of the scenario. Reachability analysis on this automaton builds an execution tree from two post operators, one for continuous flow over a time step and one for a single agent's mode change, and checks safety assertions at every vertex. The tree expands only the modes that are reached, without enumerating the global mode space. Experiments highlight expressive modeling across cars and drones, 2D/3D maps (including OpenDRIVE imports), noisy sensors, and multiple simultaneous safe
0
0
0
31
Formal Languages and Automata Theory Papers@FormalLanguages
Oct 27
Locally eventually onto cellular automata

Jan Kristian Haugland, Nadia S. Larsen, Tron Omland, Henrikke G. Rustad
arxiv.org/abs/2610.33131 [𝚌𝚜.𝙡𝙻 𝚌𝚜.𝙳𝙼 πš–πšŠπšπš‘.𝙲𝙾 πš–πšŠπšπš‘.π™³πš‚ πš—πš•πš’πš—.𝙲𝙢]
We give a new checkable criterion to ensure that a one-dimensional cellular automaton on a finite alphabet is locally eventually onto. In this setting, openness is equivalent to being n-to-1 for some n and therefore implies surjectivity. Bipermutive cellular automata are known to be locally eventually onto, while open cellular automata that are neither bipermutive nor bijective appear to have received less attention. Building on Sutner's work with de Bruijn graphs, we describe a method for deciding openness and at the same time determining n. We then introduce the notion of block-regularity of local rules as a generalization of bipermutivity and prove that it implies openness. We further identify two conditions that, together with block-regularity, ensure that every nonempty cylinder set is mapped onto the whole configuration space after a finite number of iterations, and hence that the cellular automaton is locally eventually onto. The appendix provides the algorithms that check these
0
0
1
52
Formal Languages and Automata Theory Papers@FormalLanguages
Oct 27
Formal Grammars and Generating Functions: From Algebraic Structure to Non-Algebraic and Non-Derivable Series

Zhijun Wang
arxiv.org/abs/2610.33111 [𝚌𝚜.𝙡𝙻]
This paper investigates how the algebraic and analytic properties of ordinary length generating functions constrain the grammatical and computational complexity of formal languages. We review the Chomsky-Schutzenberger representation, DSV translations for unambiguous context-free grammars, and their stack-indexed extensions, distinguishing finite algebraic systems from more general constructions. Examples and a diagonal argument demonstrate that even a rational generating function need not determine a language's grammatical class. Our central computability result establishes that, for a recursively enumerable language, computability of its length-counting sequence is equivalent to decidability of membership. Consequently, if a recursively enumerable language has a D-finite length generating function over Q(z), it is decidable; equivalently, undecidable recursively enumerable languages cannot have D-finite length generating functions. We then examine coefficient growth and singularities
0
0
0
21
Load more