Formal Languages and Automata Theory
We show that an automaton group or semigroup is infinite if and only if it admits an $\omega$-word (i. e. a right-infinite word) with an infinite orbit, which solves an open problem communicated to us by Ievgen V. Bondarenko. In fact, we…
In this thesis we use quasiorders on words to offer a new perspective on two well-studied problems from Formal Language Theory: deciding language inclusion and manipulating the finite automata representations of regular languages. First, we…
A theorem of Nekrashevych and Sidki shows the Mealy Automata structures one can place on Z^m are parametrized by a family of matrices (called "1/2-integral") and a choice of residuation vector e in Z^m. While the impact of the chosen matrix…
The locality of words is a relatively young structural complexity measure, introduced by Day et al. in 2017 in order to define classes of patterns with variables which can be matched in polynomial time. The main tool used to compute the…
Learning-based testing (LBT) is an emerging methodology to automate iterative black-box requirements testing of software systems. The methodology involves combining model inference with model checking techniques. However, a variety of…
In this work we construct an automaton for the commutative closure of a given regular group language. The number of states of the resulting automaton is bounded by the number of states of the original automaton, raised to the power of the…
Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades. It consists in the synthesis of a controller that reacts to environment's inputs satisfying a…
In this paper we investigate the number of objects actually used in the terminating computations of a certain variant of polarizationless P systems with active membranes. The P systems we consider here have no in-communication rules and…
We study the computational complexity of universality and inclusion problems for unambiguous finite automata and context-free grammars. We observe that several such problems can be reduced to the universality problem for unambiguous…
Reaction systems are a computational model inspired by the bio-chemical reactions that happen inside biological cells. They have been and currently are studied for their many nice theoretical properties. They are also a useful modeling tool…
Reaction systems are discrete dynamical systems inspired by bio-chemical processes, whose dynamical behaviour is expressed by set-theoretic operations on finite sets. Reaction systems thus provide a description of bio-chemical phenomena…
We consider the computability and complexity of decision questions for Probabilistic Finite Automata (PFA) with sub-exponential ambiguity. We show that the emptiness problem for strict and non-strict cut-points of polynomially ambiguous…
In this work, we define a framework of automata constructions based on quasiorders over words to provide new insights on the class of residual automata. We present a new residualization operation and a generalized double-reversal method for…
We study the abelian period sets of Sturmian words, which are codings of irrational rotations on a one-dimensional torus. The main result states that the minimum abelian period of a factor of a Sturmian word of angle $\alpha$ with continued…
We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to…
In [11] and [13] the authors showed that elementary cellular automata rules 0, 3, 8, 12, 15, 28, 32, 34, 44, 51, 60, 128, 136, 140, 160, 162, 170, 200 and 204 (and their conjugation, reflection, reflected-conjugation) are not maximum…
We study languages of unambiguous VASS, that is, Vector Addition Systems with States, whose transitions read letters from a finite alphabet, and whose acceptance condition is defined by a set of final states (i.e., the coverability…
Deep neural networks are increasingly being used as controllers for safety-critical systems. Because neural networks are opaque, certifying their correctness is a significant challenge. To address this issue, several neural network…
We study liveness and model checking problems for broadcast networks, a system model of identical clients communicating via message passing. The first problem that we consider is Liveness Verification. It asks whether there is a computation…
We investigate the orbits of automaton semigroups and groups to obtain algorithmic and structural results, both for general automata but also for some special subclasses. First, we show that a more general version of the finiteness problem…