Papers

Emil Post's productive sets are not even semi-computable, let alone computable, being thus essentially incomputable. Accordingly, formal languages whose set of words is a (completely) productive set are essentially undecidable. In this article, I elaborate on Post productivity from the viewpoint of formal language theory: I design formal grammars that emulate the construction of productive sets of natural numbers and are thus beyond Turing-decidability.

Lazy clause generation solvers learn from propagation explanations; the form of a Regular explanation therefore determines which clauses reach the learning engine. Standard decompositions introduce variables for automaton states and derive reasons from local table constraints. BDD and MDD propagators instead select individual diagram edges. We study the direct LCG explanation language for Regular: disequality literals of the form $X_i\neq v$. Here, one literal removes every automaton transition with the same position/value label, so an explanation is not an ordinary edge cut. We prove that explanations for value deletions are exactly label $s$–$t$ cuts in the layered DFA unfolding. This characterization establishes NP-completeness for minimum-weight explanations, gives a polynomial algorithm for inclusion-minimal explanations, and leads to an exact $O((U+n)4^{|Q|})$ dynamic program for small automata. A C++ benchmark compares label-cut explanations with Table-LCG and MDD-edge baselines on 250 generated instances. On average, minimal label cuts reduce projected explanation size from 22.2 to 5.5 literals and run in tens of microseconds. Minimal label cuts are therefore the practical default; the exact algorithm provides an oracle for small automata.

Language generation in the limit asks for valid unseen elements from every exhaustive positive presentation of an unknown infinite language. We characterize this task for arbitrary families over a countable universe. Generation is possible exactly when each target can be assigned a finite positive witness so that the targets activated by any finite sample have an infinite common intersection. The necessary direction follows from a universal normalization: a search through unconfirmed histories converts any successful generator into one depending only on the observed set. We then ask how large compatible witnesses must be. Positive separation width records the smallest uniform size bound, with two further levels for unbounded finite witnesses and the absence of any compatible finite-witness assignment. Every level occurs. Countable families admit singleton witnesses, explicit families realize every finite width, and a union of two families with infinite common cores requires unbounded finite witnesses. Finally, countable-support and finite-profile obstructions explain why local combinatorial data cannot determine generation in the limit. The characterization and full width hierarchy are checked in Lean, including the simplified normalization and a direct diagonal capture lemma. The accompanying Lean development is maintained at https://github.com/xiaoyulics/language-generation-characterization

Ensuring confidentiality in Cyber-Physical Systems is critical, especially when attackers exploit execution times to infer sensitiveinformation. Traditional opacity models are inadequate for timed systems, as verifying opacity in Timed Automata is undecidable. To address this challenge, we propose Execution-Time Opacity Logic (ETOL), a new formalism that specifies opacity by requiring that for every execution satisfying a secret formula, there exists another execution of the same duration that does not satisfy it. ETOL guarantees that timing observations cannot reveal confidential agent activities. We present a decidable and efficient verification framework based on zone-based model checking, supported by a dedicated algorithm that systematically identifies duration-equivalent executions. Our approach is validated through an ATM case study, showing that ETOL enables efficient verification of execution-time confidentiality under timing attacks. We also developed a prototype tool for the ETOL logic that supports symbolic model checking over timed systems. It allows users to verify ETOL formulas based on clock-constrained execution paths.

Recent advancements in transformer length generalization theory enable us to reliably predict when a transformer can learn to solve a task. In particular, the C-RASP hypothesis (a formalized version of the so-called RASP-l conjecture) posits that transformers length-generalize on a task if and only if a solution is expressible in the C-RASP language. While this hypothesis has strong empirical validation, theoretical problems arise from the fact that no computable length generalization bounds exist for C-RASP, alongside the discovery of seemingly contradictory experiments. To address these problems, we refine the C-RASP hypothesis utilizing the recently-proposed fragments C-RASP+ and C-RASP1. These fragments have computable length generalization bounds, though in the worst case requiring an extremely large (double exponential) sample size. It is an open question whether these sample size bounds are tight. In this paper, we resolve this open question by providing an exponentially tighter bound. In doing so, we show a polynomial length generalization bound for transformers if we adopt compressed strings, via a novel connection to power words. As an application, we show how this yields a fine-grained analysis of the C-RASP conjecture that resolves contradicting experimental evidence against it.

We study graph-based automata: nondeterministic finite automata obtained from edge-colored or oriented graphs by taking every vertex as both initial and accepting, and every edge as a pair of opposite transitions. The language of these automata corresponds to the set of edge-colored or oriented paths mapping to their corresponding graphs. We develop an analogous notion for trees and characterise the languages recognised by these models. For tree languages we prove the existence of a unique size- minimal graph and, more generally, a homomorphism-minimal graph for both word and tree languages using duality methods. In order to further motivate these models, we showcase a few results at the inter- section between graph theory and automata theory: We relate graph-based automata to reversible automata, give a decomposition of graph-based languages into reversible languages, and introduce the remanent language of an undirected graph as the inter- section of all its orientations. This remanent language captures structural information on the graph such as chromatic number.

In 1980 Bucher asked whether, given context-free languages $L\subseteq U$ with $U\setminus L$ infinite, there must be a context-free language $K$ between them for which both $K\setminus L$ and $U\setminus K$ are infinite. We give a negative answer. We first construct an infinite language $D$ with context-free complement such that, for every regular language $R$, either $D\cap R$ or $D\setminus R$ is finite. The words of $D$ encode computations of factorials; repetition of letters ensures that each finite automaton either accepts all but finitely many words of $D$ or rejects all but finitely many words of $D$, while a one-counter automaton recognizes errors in the encodings. We then construct $L$ and $U$ from the complement of $D$. A grammar argument shows that any context-free intermediate language $K$ would divide $D$ in the same way as some regular language. This proves the required impossibility. Both $L$ and $U$ can be taken over a binary alphabet.

For two distinct binary words of length $n$, the separating words problem asks for a small deterministic finite automaton that accepts exactly one of them. Chase proved a $\widetilde O(n^{1/3})$ upper bound using a complex-analytic estimate for sparse polynomials. We replace that estimate by a finite-difference argument and a second-order real recurrence cutoff. The resulting elementary proof gives an explicit bound of $O(n^{1/3}(\log n)^{7/3})$ states.

The Stranded Cellular Automata (SCA) model is a grid of cells such that each cell can contain 0, 1, or 2 strands, together with two cellular automata that control when and how strands turn and cross. It was developed to study patterns occurring in fiber arts. We define a notion of what it means for a braid, in the sense of an element of a braid group, to be represented by an SCA pattern, and provide several algorithms to determine when a braid has an SCA representation with certain additional properties.

Timed Partial Orders (TPOs), originally proposed for workflows, provide an interpretable framework for robot task specification with planning algorithms based on mixed-integer linear programming (MILP). However, TPOs are limited in expressivity, capturing only partial-order events with simple timing constraints. In this paper, we introduce Conditional TPOs (cTPOs), which extend TPOs with richer relative-timing constraints and conditional event activations based on environmental conditions. We show that planning for cTPOs also reduces to an MILP problem; however, the added expressivity results in significantly larger MILPs that can become computationally intractable. To address this challenge, we propose a decomposition algorithm that partitions a cTPO into smaller sub-TPOs, yielding a sequence of smaller MILP problems. We prove that this decomposition is complete and preserves plan optimality while improving the interpretability of complex tasks. Experimental results demonstrate the effectiveness of cTPOs as a task specification framework and the efficiency of our decomposition approach, achieving up to four orders of magnitude speedup over the monolithic MILP.

Finite automata can describe relations of unbounded arity that are exponentially larger than their descriptions. We prove that constraint satisfaction for such relations is solvable in polynomial time whenever their length slices are preserved by a common fixed edge operation on a finite domain. The algorithm computes compact representations of the complete solution relation and its projections. Its main ingredient is a polynomial-time compilation of nondeterministic finite automata into the fork witnesses and small projections required by the few-subpowers algorithm. In the Mal'tsev case, a direct proof is polynomial also when the domain and operation table are supplied as input, answering the Mal'tsev tractability question for automatic constraint satisfaction. We also characterize all invariant relations of a family of 3-edge algebras with neither Mal'tsev nor near-unanimity terms. Their normal forms combine Boolean activity constraints with affine value spaces and yield canonical quadratic-bit representations constructible from NFAs or arbitrary generators. For graphoid automata, these results give polynomial-time recognition without a graph-width restriction, effective boundary composition, and comparison of finite graph relations. The quadratic boundary bounds are optimal in the worst case. A fixed three-state example separates polynomial-time recognition from hard exact counting.

Observation consistency (OC) and modified observation consistency (MOC) are structural conditions used in hierarchical and modular supervisory control under partial observation. Their verification for languages generated by deterministic finite automata is PSPACE-hard, whereas decidability was open. We answer this question by showing that both problems are undecidable, that is, there are no algorithms verifying OC or MOC. On the positive side, we identify a decidable class defined by a restriction on the plant: if every cycle of the automaton contains a transition labeled by an observable high-level event, then verification of both conditions is PSPACE-complete.

The very first construction by J. Richard Büchi himself for complementing a Büchi automaton relies on a fundamental lemma about the division of an arbitrary infinite word into consecutive finite words, which was cleanly proven by invoking a specialized theorem of Ramsey. For that reason, constructions of similar nature have subsequently been labeled as Ramsey-based. Nevertheless, it suffices to have a weaker form of the lemma where the finite words come from a finite number of congruence classes, rather than arbitrary classes, that form a partition of the set of all finite words. The weaker lemma, with support of nicer properties from a congruence, can be proven without Ramsey's theorem. A commonly adopted improvement on such complementation constructions also requires the working of a congruence. This paper recounts the history and reviews using more contemporary terminology wherever possible the relevant concepts and results, to advocate renaming of Ramsey-based constructions as congruence-based constructions.

Cellular automata is a local computation paradigm where complex behavior can arise from local interactions between simple functions. This paradigm has been used to explain many systems such as biological processes, traffic simulation, computer networks, etc. In games, cellular automata have been used in games such as SimCity and for the generation of spatial content such as caves or dungeons. However, creating effective local rules is hard and unintuitive. Cellular automata can be effectively evolved, but may still be hard to interpret. In this work, we introduce the concept of programmable cellular automata, where we represent the system as Python code. We also modularize the cellular automata into local functions and a decision function. Local functions take a local neighborhood and return a value, while the decision function takes the output of the local functions and decides the value of the next state. Separating the cellular automata into modules written in Python helps with understanding how these systems are working. We also explore adding global functions where they take the whole state and compute a function from it. We tested generating levels for three different games from the PCG Benchmark. The results showed that global functions decrease the number of iterations that cellular automata need to solve a problem, and that we cannot find solutions for some problems with purely local functions. Looking into the generated functions, we can see common functions that have been used in different experiments, which not only helps us understand the generator but also helps us understand these games better and what is important for them.

Algebraic combinatorics often seeks bijections that explain identities between distributions object by object. Encoding combinatorial objects as words lets automata theory study such a bijection as a word-to-word computation and measure its memory, input access, and control of output order. This refines existence questions by asking which computational mechanisms a bijection requires. We develop this viewpoint for Dyck paths. Our motivating example is the $q,t$-Catalan polynomial. Let $D_n$ be the set of Dyck paths of semilength $n$, let $D=\bigcup_{n\ge 0}D_n$, and let $area, dinv, bounce \colon D\to\mathbb{N}$ be the standard statistics. Then, \[ C_n(q,t)=\sum_{P\in D_n}q^{area(P)}t^{bounce(P)} =\sum_{P\in D_n}q^{dinv(P)}t^{area(P)}. \] Haglund's zeta map $\zeta\colon D\to D$ gives a bijective proof: it preserves semilength and sends $(dinv,area)$ to $(area,bounce)$. By contrast, the full symmetry $C_n(q,t)=C_n(t,q)$ still lacks a direct explanation: no explicit, uniform, semilength-preserving bijection is known that swaps area and dinv on every Dyck path. Polyregular maps from automata theory provide a natural computational starting point, but we prove that neither $\zeta$ nor the classical height-sweep bijection witnessing Narayana symmetry is polyregular. The missing mechanism is global ordering by numerical levels whose range grows with the input. We call this a rank sort and introduce weighted-rank polyregular maps (WRP), extending polyregular maps by one such sort and containing both bijections. Nevertheless, WRP is a proper subclass of deterministic logspace. We prove that $\zeta^{-1}$ lies outside WRP and that no WRP map can realise a semilength-preserving area-dinv swap. Thus the rank-sorting strategy behind $\zeta$ cannot be extended within WRP to exchange the two statistics.

We consider the sequences of natural integers that can be computed by a deterministic transducer, with input in a structure A, output in N. and with memory the set of stacks of stacks of A. We show that these sequences are, exactly, the counting sequences of formal languages generated by unambiguous context-free indexed grammars (equivalently, the counting sequences of derivation trees of arbitrary context-free indexed grammars), with indexes in A. This general theorem applies, notably, to the set of natural integers endowed with the operation -1 and the non-zero predicate, showing that the polynomial recurrences count exactly the index-languages (where the parameter used for counting is the index itself).

We show that susceptibilities, an interpretability technique developed for neural networks, can identify the presence of algorithmic structure in Turing machines by probing the local loss landscape of a learning problem for noisy Turing machines introduced by Murfet and Troiani (arXiv:2504.08075). We prove that symmetries and path separation in the algorithm implemented by a Turing machine induce permutation symmetries and low-rank blocks in its susceptibility matrix. We study this empirically on a set of deterministic finite automata (DFAs) and demonstrate that algorithmic features can be recovered by principal component analysis and clustering methods in susceptibility space.

Language recognition by homomorphisms is a central construction of algebraic language theory. Initially studied for monoids and semigroups, it has subsequently been expanded to other algebraic structures. Our new categorical account is based on fibrations, which have already seen other applications in automata theory. Languages and surjective homomorphisms give indeed rise to two fibrations, and the notion of language recognition is stable under reindexing. We develop this framework in a category with a factorisation system and address two main technical questions in the fibrational setting. First, we provide sufficient conditions under which languages have syntactic quotients (which is a generalisation of syntactic congruences) and we show how such quotients can be described in some concrete cases using a result by Slomiński. Second, we introduce sufficient conditions under which (regular) languages are closed under certain J-limits and J-colimits.

Synchronization strings provide deterministic position labels for recovering coordinates after insertions and deletions. Haeupler and Shahrasbi introduced these objects, and subsequent work proved that four symbols suffice for some fixed parameter epsilon < 1, whereas two symbols cannot support arbitrarily long synchronization strings. We resolve the remaining ternary case: every length admits a ternary 2001/2002-synchronization string. Thus three is the exact minimum constant alphabet size. A computer-assisted refinement based on a larger 54-uniform family yields ternary epsilon-synchronization strings for every epsilon > 215/216. The previous four-symbol construction uses a ternary square-free backbone to exclude short repetitions and a fourth symbol to carry long-range synchronization marks. Our main technical contribution is a local-entropy transfer theorem: every square-free block-local source with a positive interval conditional min-entropy rate supports synchronization strings with a fixed gap. We instantiate this theorem using occurrence-wise branching in a Brinkhuis family. Every outcome remains ternary and square-free, while every long interval retains linear conditional min-entropy after all choices outside it are exposed. A deletion-ball estimate converts this entropy into an exponentially small probability of a near-complete common subsequence between adjacent intervals, and an asymmetric Lovasz Local Lemma enforces all interval constraints simultaneously. The same framework also yields exponentially many valid words, synchronization circles, and synchronization within a class of extremal square-free words. Adding constraints on distant intervals gives a Las Vegas construction in expected O(n^2 log^3(n+2)) time.

The target discounted-sum problem (TDS) asks, given a finite integer alphabet $\Sigma$, a rational discount factor $\lambda$, and a rational target $t$, whether some infinite sequence over $\Sigma$ has discounted sum exactly $t$. This problem remains open and underlies several open questions in automata theory, games, and Markov decision processes. We introduce and solve its stochastic counterpart, the stochastic target discounted-sum problem, which replaces existence by computation of the probability. We show that the probability that a random sequence generated by a finite Markov chain has discounted sum $t$ is rational and computable in pseudo-polynomial time. We further show how to decide, in polynomial time, whether the discounted-sum distribution of a Markov chain is atomless, and how to approximate to an arbitrary precision the probability that the discounted sum exceeds a rational threshold. Our techniques for the stochastic TDS problem allow us to make progress on TDS objectives in stochastic games, which are known to be as hard as the TDS problem. Restricting the maximizing player to finite-memory strategies, while allowing the minimizing player to use arbitrary strategies, we reduce the value problem and the synthesis problem to corresponding problems for safety objectives in stochastic games. This yields computable optimal values and deterministic optimal strategies with pseudo-polynomially bounded memory for stochastic games, and results in pseudo-polynomial-time algorithms for special cases of Markov decision processes and deterministic two-player games.

Let $L\subseteq\Sigma^*$ and fix a morphism $h:\Sigma^*\to M$ into a finite monoid. We study exact factorization and canonical presentation in the relative syntactic congruence $\theta_{L,h}:=\equiv_L\cap\ker h$. We separate unique factorization from finite direct presentation. An exhaustively computer-checked $36$-element quotient has a unique exact prime factorization for every live non-unit class, yet its valid prime-return rules contain an infinite family, so unique factorization does not imply the finite relative presentation property (FRP), even for a finite quotient. We lift the same defect to a nonregular context-free language with an infinite relative quotient and finite prime spectrum. To isolate the obstruction, we introduce the finite-state relative presentation property (FSRP), in which canonical valid right-hand-side languages are represented by finite residual controllers, and prove $\mathrm{FRP}\subsetneq\mathrm{FSRP}$. We then introduce prime-target left-division determinism (PTLD), which implies unique exact factorization, tail exactness, tail determinism, and a quadratic bound on valid rules. A nonregular deterministic context-free example with a finite group observer satisfies PTLD while lying outside every fixed $(k,\ell)$-substitutable class. Finally, for fixed $h$ we give a strong positive-data learner for the canonical PTLD presentation with polynomial-time hypothesis updates and a finite characteristic sample, together with a limit reconstruction of the canonical FSRP controller from weakly behaviorally correct CFG-valued learners.

Automated translation of natural language (NL) descriptions into Linear Temporal Logic over finite traces (LTLf) is a prerequisite for automated formal verification of a system's dynamic behavior. Several LLM-based methods have recently shown potential for this task. However, they struggle with the nuance of natural language descriptions, which can lead LLMs to only partially capture the intended meaning. To address this limitation, we propose NeuroSTAR (Automata-guided Neuro-symbolic Specification Formalization), an NL-to-LTLf framework that builds on two insights. First, it leverages multiple generators to obtain diverse LTLf candidates. Second, it uses an automata-theoretic semantic comparison based on DFA traces to identify behavioral disagreements that guide formula refinement. We evaluate NeuroSTAR and show that it improves NL-to-LTLf translation performance by 8-18 percentage points relative to the prior state-of-the-art (SoTA) on unambiguous benchmarks. We further study its applicability to a body of driving law text, a complex, realistic, and reference-free domain critical for autonomous-vehicle specification. This study shows that NeuroSTAR can capture the necessary temporal semantics in 83.9% of the driving law sections, which demonstrates the effectiveness of automata-guided reference-free refinement in formalization.

This chapter reconstructs the McCulloch-Pitts program as a physics of neural computation rather than the familiar cartoon of a binary neuron. The 1943 logical calculus is developed in both directions: given a net, characterize the propositions realized by its activity; given an admissible logical expression, construct a net that realizes it. We recover the original distinction between thresholded excitatory summation and absolute inhibitory veto-one the weighted-threshold form cannot preserve for arbitrarily large excitatory inputs-and read unit-time delay as the physical realization of logical depth. Recurrence is treated exactly: an autonomous, deterministic network of finitely many binary units has a finite state space, so every trajectory eventually enters a periodic orbit-a fact about finite-state dynamics, not unbounded Turing computation. A single threshold element realizes only linearly separable Boolean functions, whereas finite feedforward networks of them synthesize any Boolean function on a finite domain. We then follows McCulloch and Pitts beyond threshold logic. The 1945 heterarchy paper turns cyclic preference into an obstruction to representation by a scalar utility. The 1947 work on universals asks how a physical network can identify inputs related by nuisance transformations, developed here via group averaging and feedback canonicalization. The 1959 frog-retina study makes the adequate-stimulus question experimental, revealing parallel invariant operations before the brain proper. Spike-triggered analysis shows how a nonlinearly driven neuron can have a vanishing first-order average while second-order statistics recover its hidden selectivity: methodological failure can masquerade as physiological absence. Modern mathematical tools are used without projecting their notation onto the historical papers, and limitations of the idealization are stated explicitly.

Under compact symmetry, observable behavior reduces to an invariant operator algebra, but its dimension is not yet classical memory: some coordinates are dynamically frozen, some invisible to threshold tests, and some already classical. We develop an operator-algebraic theory that separates these effects through three filters. For one automaton, behavior is the Hilbert–Schmidt pairing between prefix-reachable states and suffix-observable effects, whose rank equals the real Hankel rank without controllability or observability assumptions. Maximizing this invariant over a symmetry-constrained dynamical class gives a structural capacity controlled by the symmetry commutant: its center stores isotypic populations frozen by reversible dynamics, its traceless multiplicity blocks carry movable noncommutative coordinates, dissipation removes the unary spectral loss inside those blocks, and covariant mobility releases relative populations subject to component conservation. Operational realization then determines which surviving coordinates force probabilistic states. For a fixed nontrivial invariant readout, full mobility gives an exact dichotomy in worst-case state cost: a commutative invariant algebra costs exactly its dimension, whereas a noncommutative multiplicity block raises the unrestricted cost by exactly one state. Thus noncommutativity has a one-state worst-case classical price. The known four-letter quadratic-plus-one law at trivial symmetry is the fully mobile endpoint of this principle. Schur–Weyl duality further shows that different preserved symmetries on the same tensor-power Hilbert space can change the worst memory scale from polynomial to exponential, while fixed-weight modules give an exact Catalan law at half filling, with structural capacity equal to the Catalan count minus its central-sector correction.

Anonymity is an information flow property that provides privacy protection in the sense of non-uniqueness of system information at certain moments with respect to observations. The notion of $K$-step anonymity in the context of discrete-event systems characterizes the scenario that the state estimates cannot be a singleton within at most $K$ observational steps prior to the current instant, while infinite-step anonymity is the same as $K$-step anonymity without considering the limit on $K$. In this paper, we lucubrate $K$- and infinite-step anonymity for partially-observed discrete-event systems modeled by non-deterministic finite-state automata. First, we define two strong types and two weak types of $K$- and infinite-step anonymity that are fundamentally different from the existing notions of $K$- and infinite-step anonymity due to the consideration of strong and weak anonymous projections. Then, we develop a new methodology by exploiting the concurrent-composition technique to verify these four types of anonymity. Based on the constructed concurrent compositions, verifiable necessary and sufficient conditions for the four types of anonymity are provided, along with their complexity analysis. Finally, the upper bounds on $K$ for $K$-step strong anonymity and weak anonymity are computed.

We show a subexponential lower bound on the reset threshold of synchronizing deterministic finite tree automata (DTA) over alphabets of just two symbols. This significantly improves the previous one, which was quadratic in the number of states. Our result also narrows the gap towards the lower bound for DTA over alphabets that grow linearly with the number of states, as well as the best known upper bound, both of which are currently exponential.

Inoue et al. have introduced the successful derivation game (SDG) on context-free grammars (CFGs), which is a generalization of classic heap-based games including subtraction games and Keyles, and shown that the least upper bound of the Grundy numbers in the SDG on a given CFG G is undecidable in general even when we restrict G to be a linear CFG. This paper shows that for the SDG on a right-linear grammar (RLG), we can construct a DFA for computing the Grundy number of a given position. In other words, for the SDG on an RLG, the set of positions with a given Grundy number c is regular. As a corollary, the least upper bound of the Grundy numbers in the SDG on a given RLG is decidable. We also investigate the complexity of computing the least upper bound of the Grundy numbers in the SDG on a given RLG, and it is shown to be PSPACE-complete.

Daviaud, Guillon, and Merlet proved that comparison of max-plus automata is undecidable under a fixed state bound of 553 and explicitly left the range from 2 to 552 states open. We resolve the two-state endpoint. More strongly, given an arbitrary finite max-plus automaton $A$ and a max-plus automaton $B$ with at most two states, it is decidable whether $[\![A]\!](w)\leq [\![B]\!](w)$ for every word $w$. The structural reason is a one-dimensional projective normal form for two-state dynamics. Outside an effective bounded region, a transition has one of three tail behaviors: it propagates the unbounded projective gap with gap-independent height increment, forgets the gap with gap-independent height increment, or reads the gap magnitude into the height increment and then forgets it. In particular, any transition whose output depends on the unbounded gap necessarily destroys that gap. This yields an exact one-counter realization of $B$. Effective semilinearity of context-free Parikh images then reduces comparison to Presburger arithmetic. As a consequence, two-state max-plus comparison, equivalence, and positivity are decidable.

LTLf, a finite word variant of LTL, can be reduced to LTL by introducing a new atomic proposition indicating the prefix of the infinite words that correspond to the finite words that the original LTLf formula was considering. Such a reduction was originally proposed by De Giacomo and Vardi (IJCAI'13). However, while any LTL formula reduced from LTLf describes an obligation property in the hierarchy of Manna and Pnueli (PODC'90), the aforementioned reduction does not provide an LTL formula that belongs to the syntactic obligation fragment of LTL. This note shows how the reduction was fixed in Spot in order to ensure that the resulting LTL formula is always a syntactic obligation. Doing so allows algorithms specialized to syntactic obligation to be used on LTLf formulas. For instance, in previous work (CAV'26) we described a specialized translation from syntactic obligations to minimal, weak, deterministic Büchi automata that would not be usable with the original reduction.

We revisit questions on separating words raised by Demaine, Eisenstat, Shallit, and Wilson, together with Ebrahimnejad's follow-up to their reversal problem. For length-$n$ pairs whose difference word has $d$ runs, we prove an $O(d\log n)$ bound, extending the Hamming-distance theorem of Demaine et al. For conjugate words, we give bounds controlled by the arithmetic of the shift. We resolve Demaine et al.'s Open Problem 2 by showing that the order of two words can change nondeterministic separation by an unbounded factor. Our reversal construction addresses Ebrahimnejad's follow-up to Open Problem 1: forward and reversed deterministic separation can differ by an unbounded factor. Since nondeterministic separation is invariant under reversal, the same construction also improves the lower bound in Open Problem 3.