形式语言与自动机理论

We introduce a new technique for repairing syntax errors in arbitrary context-free languages. This technique models syntax repair as a language intersection problem by defining a finite language that provably generates every syntactically…

In runtime verification, pattern matching, which searches for occurrences of a specific pattern within a word, provides more information than a simple violation detection of the monitored property, by locating concrete evidence of the…

We prove that, paying a polynomial increase in size only, every unrestricted two-way nondeterministic finite automaton (2NFA) can be complemented by a 1-limited automaton (1-LA), a nondeterministic extension of 2NFAs still characterizing…

We give a decision procedure and proof of correctness for the equational theory of probabilistic Kleene algebra with angelic nondeterminism introduced in Ong, Ma, and Kozen (2025).

Complementation of finite automata is a basic operation used in numerous applications. The standard way to complement a nondeterministic finite automaton (NFA) is to transform it into an equivalent deterministic finite automaton (DFA) and…

This paper is a continuation of a previous study on the so-called measure once finite quantum automata model introduced by Moore and Crutchfield in 2000. We investigate conditions assuring that, given a language recognized by such a device…

We show that the big-O problem for max-plus automata is decidable and PSPACE-complete. The big-O (or affine domination) problem asks whether, given two max-plus automata computing functions f and g, there exists a constant c such that f <…

We prove that many dynamical properties of group cellular automata (i.e., cellular automata defined on any finite group and with global rule which is an endomorphism), including surjectivity, injectivity, sensitivity to initial conditions,…

Process mining leverages event data extracted from IT systems to generate insights into the business processes of organizations. Such insights benefit from explicitly considering the frequency of behavior in business processes, which is…

We study the notion of sparseness for regular languages over finite trees and infinite words. A language of trees is called sparse if the relative number of $n$-node trees in the language tends to zero, and a language of infinite words is…

The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the…

The problem of LTLf reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolution of the inputs and outputs has a prefix that satisfies a…

Regular expression matching is of practical importance due to its widespread use in real-world applications. In practical use, regular expressions are often used with real-world extensions. Accordingly, the matching problem of regular…

We develop and explore the idea of recognition of languages (in the general sense of subsets of topological algebras) as preimages of clopen sets under continuous homomorphisms into Stone topological algebras. We obtain an Eilenberg…

In a \emph{separability problem}, we are given two sets $K$ and $L$ from a class $\mathcal{C}$, and we want to decide whether there exists a set $S$ from a class $\mathcal{S}$ such that $K\subseteq S$ and $S\cap L=\emptyset$. In this case,…

In a two-player zero-sum graph game, the players move a token throughout a graph to produce an infinite play, which determines the winner of the game. Bidding games are graph games in which in each turn, an auction (bidding) determines…

RNA co-transcriptionality, where RNA is spliced or folded during transcription from DNA templates, offers promising potential for molecular programming. It enables programmable folding of nano-scale RNA structures and has recently been…

This paper establishes formal mathematical foundations linking Chaos Game Representations (CGR) of DNA sequences to their underlying $k$-mer frequencies. We prove that the Frequency CGR (FCGR) of order $k$ is mathematically equivalent to a…

It is shown that shape preservation is decidable for top-down tree transducers, bottom-up tree transducers, and for compositions of total deterministic macro tree transducers. Moreover, if a transducer is shape preserving, then it can be…

System behaviors are traditionally evaluated through binary classifications of correctness, which do not suffice for properties involving quantitative aspects of systems and executions. Quantitative automata offer a more nuanced approach,…