形式语言与自动机理论

We study the task of disambiguation of finite state automata, namely, converting an automaton into an equivalent, unambiguous one. We do this by developing a novel and simple algorithmic framework that generalizes the subset construction…

Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to…

Modern sequence models are increasingly deployed as agents that interleave token generation with calls to external tools. We give an exact, architecture-level account of when such tool access increases computational expressivity. We model…

Automata on linear orderings are finite-state automata introduced by Bruy\`ere and Carton as a broad generalization of finite, infinite and transfinite-word automata. In this context, a word is defined as a function from a linear ordering…

We present an algebraic method for analyzing probabilistic programs with counters and discrete states, Generalized Constant Probability (GCP) programs. We define the operational semantics of GCP in terms of the runs of a type of…

We show that any overlap-free morphism is a $k$-power-free morphism for all integers $k\geq 3$.

Symmetric difference automata (XNFA) are a variant of standard finite automata in which an input word is accepted iff the number of accepting runs is odd. Equivalently, these are weighted automata over the two-element field. We study the…

A two-dimensional automaton is able to move its input head through its input word in four directions: upward, downward, leftward, and rightward. If we prevent the input head from moving upward, then we obtain a three-way two-dimensional…

We study a finite-state symbolic controller for systems in which the admissible visible transitions are fixed in advance and each visible state carries a minimum dwell requirement. The resulting model, which we call a destination-labeled…

Vector Addition System with States (VASS) are a ubiquitous model of infinite-state systems consisting of a set of non-negative counters which can be incremented and decremented. It is known that the reachability problem for VASS is…

Suppose we have a deterministic finite-state transducer $A$ and an infinite word $x$, and run $A$ on $x$ to obtain an infinite word $A(x)$. Which properties of $x$ are guaranteed to also hold for $A(x)$? In this paper, we study this…

Finite-state transducers and Wheeler automata are two well-established frameworks in formal language theory. While transducers extend finite-state automata by associating output words to input words, Wheeler automata are automata whose…

B\"uchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of B\"uchi automata where every strongly connected component is either deterministic or inherently weak. It was…

In the past literature, families of two-way finite automata and pushdown automata having limited state complexity (i.e., the total number of inner states) and stack-state complexity (i.e., the total number of inner states multiplied by the…

Parallel Communicating Finite Automata (PCFA) are systems of several finite automata that can communicate by requesting the state of another automaton. As an attempt to make PCFA as defined in [8] and [2] more realistic, the non-forgetting…

Finite automata with translucent input letters are a recent model of discontinuous input processing. Basically, classical finite automata are equipped with a translucency function that defines, depending on the state, the set of translucent…

In this paper, we continue the research on the power of contextual grammars with selection languages from subfamilies of the family of regular languages. We investigate infix-, prefix-, and suffix-free languages (referred to as idefix-free…

We introduce and study a family of two-head finite automata called two head returning finite automata (2-HRFA) operating on rectangular arrays of picture languages, in which both heads move in opposite directions. We show that the class of…

Regular expressions with counting operations (c-regexes) offer a compact representation of repeating patterns by allowing numerical bounds to be added to subexpressions. Recent work introduced the counting-set data structure, which allows…

Backtracking regular expression matchers are widely used due to their expressive power but may exhibit exponential worst-case matching time. Memoization provides a principled method for eliminating redundant computation and ensuring linear…