Formal Languages and Automata Theory
Reactive synthesis algorithms allow automatic construction of policies to control an environment modeled as a Markov Decision Process (MDP) that are optimal with respect to high-level temporal logic specifications. However, they assume that…
For all natural numbers a,b and d > 0, we consider the function f_{a,b,d} which associates n/d to any integer n when it is a multiple of d, and an + b otherwise; in particular f_{3,1,2} is the Collatz function. Coding in base a > 1 with b <…
We consider linear cost-register automata (equivalent to weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems of boundedness and zero isolation ask whether there is a…
The identification of a deterministic finite automaton (DFA) from labeled examples is a well-studied problem in the literature; however, prior work focuses on the identification of monolithic DFAs. Although monolithic DFAs provide accurate…
Stream-based runtime monitors are used in safety-critical applications such as Unmanned Aerial Systems (UAS) to compute comprehensive statistics and logical assessments of system health that provide the human operator with critical…
We study synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling such systems is register automata and transducers. They extend finite-state automata by…
An F-system is a computational model that performs a folding operation on words of a given language, following directions coded on words of another given language. This paper considers the case in which both given languages are regular, and…
The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem that lies at the core of many questions in this setting is the…
Probabilistic automata are an extension of nondeterministic finite automata in which transitions are annotated with probabilities. Despite its simplicity, this model is very expressive and many of the associated algorithmic questions are…
Tree-adjoining grammar (TAG) and combinatory categorial grammar (CCG) are two well-established mildly context-sensitive grammar formalisms that are known to have the same expressive power on strings (i.e., generate the same class of string…
A locally testable semigroup S is a semigroup with the property that for some nonnegative integer k, called the order or level of local testability, two words u and v in some set of generators for semigroup S are equal in the semigroup if…
Given a finite alphabet $\Sigma$ and a right-infinite word $w$ over the alphabet $\Sigma$, we construct a topological space ${\rm Rec}(w)$ consisting of all right-infinite recurrent words whose factors are all factors of $w$, where we work…
Geometric folding processes are ubiquitous in natural systems ranging from protein biochemistry to patterns of insect wings and leaves. In a previous study, a folding operation between strings of formal languages was introduced as a model…
We consider the model of pushdown vector addition systems with resets. These consist of vector addition systems that have access to a pushdown stack and have instructions to reset counters. For this model, we study the coverability problem.…
While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound…
Opacity is an information flow property that captures the notion of plausible deniability in dynamic systems, that is whether an intruder can deduce that "secret" behavior has occurred. In this paper we provide a general framework of…
When omega-regular objectives were first proposed in model-free reinforcement learning (RL) for controlling MDPs, deterministic Rabin automata were used in an attempt to provide a direct translation from their transitions to scalar values.…
Simulations and bisimulations between two fuzzy automata over a complete residuated lattice were defined by \'Ciri\'c et al. (2012) as fuzzy relations between the sets of states of the automata. However, they act as a crisp relationship…
Transition systems (TS) and Petri nets (PN) are important models of computation ubiquitous in formal methods for modeling systems. An important problem is how to extract from a given TS a PN whose reachability graph is equivalent (with a…
We investigate the properties of formal languages expressible in terms of formulas over quantifier-free theories of word equations, arithmetic over length constraints, and language membership predicates for the classes of regular, visibly…