形式语言与自动机理论

For almost a century, the decidability of the Skolem Problem - that is, the problem of finding whether a given linear recurrence sequence (LRS) has a zero term - has remained open. A breakthrough in the 1980s established that the Skolem…

Interaction models describe distributed systems as algebraic terms, with gates marking interaction points between local views. Composing local models into a coherent global one requires aligning these gates while respecting the algebraic…

State reduction of finite automata plays a significant role in improving efficiency in formal verification, pattern recognition, and machine learning, where automata-based models are widely used. While deterministic automata have…

GF(2)-grammars are a recently introduced grammar family with some unusual algebraic properties. They are closely connected to unambiguous grammars. By using the method of formal power series, we establish strong conditions that are…

Multiparty Session Types (MPST) provide a type-theoretic foundation for specifying and verifying communication protocols in distributed systems. MPST rely on the notion of global type which specifies the global behaviour and local types,…

The reachability problem in multi-pushdown automata (MPDA) has many applications in static analysis of recursive programs. An example is safety verification of multi-threaded recursive programs with shared memory. Since these problems are…

Extensions of {\omega}-automata to infinite alphabets typically rely on symbolic guards to keep the transition relation finite, and on registers or memory cells to preserve information from past symbols. Symbolic transitions alone are…

In this article, we present Tahr, a framework that allows taking attribute grammar specifications and generating a set of software artefacts that can be used programmatically to operate on text compliant with the grammars. Tahr can be used…

In this work, we study the problems of counting and sampling Mazurkiewicz traces that a regular language touches. Fix an alphabet $\Sigma$ and an independence relation $\mathbb{I} \subseteq \Sigma \times \Sigma$. The input consists of a…

Branching Rauzy induction is a two-sided form of Rauzy induction that acts on regular interval exchange transformations (IETs). We introduce an extended form of branching Rauzy induction that applies to arbitrary standard IETs, including…

The target discounted-sum problem is the following: Given a rational discount factor $0<\lambda<1$ and three rational values $a,b$, and $t$, does there exist a finite or an infinite sequence $w \in \{a,b\}^*$ or $w \in \{a,b\}^\omega$, such…

Simple process models are key for effectively communicating the outcomes of process mining. An important question in this context is whether the complexity of event logs used as inputs to process discovery algorithms can serve as a reliable…

Counters that hold natural numbers are ubiquitous in modeling and verifying software systems; for example, they model dynamic creation and use of resources in concurrent programs. Unfortunately, such discrete counters often lead to…

We describe witness languages meeting the upper bound on the state complexity of the multiple concatenation of $k$ regular languages over an alphabet of size $k+1$ with a significantly simpler proof than that in the literature. We also…

Hard attention Chain-of-Thought (CoT) transformers are known to be Turing-complete. However, it is an open problem whether softmax attention Chain-of-Thought (CoT) transformers are Turing-complete. In this paper, we prove a stronger result…

In probabilistic programming, the inference problem asks to determine a program's posterior distribution conditioned on its "observe" instructions. Inference is challenging, especially when exact rather than approximate results are…

We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs…

Multi-stack machines and Turing machines can simulate to each other. In this note, we give a succinct definition of multi-stack machines, and from this definition it is clearly seen that pushdown automata and deterministic finite automata…

John Conway proved that every audioactive sequence (a.k.a. look-and-say) decays into a compound of 94~elements, a statement he termed the cosmological theorem. The underlying audioactive process can be modeled by a finite-state machine,…

Cellular automata (CA) are well-studied models of decentralized parallel computation, known for their ability to exhibit complex global behavior from simple local rules. While their dynamics have been widely explored through simulations, a…