Formal Languages and Automata Theory
Compartmental models are used in epidemiology to capture the evolution of infectious diseases such as COVID-19 in a population by assigning members of it to compartments with labels such as susceptible, infected, and recovered. In a…
Existing models for the analysis of concurrent processes tend to focus on fail-stop failures, where processes are either working or permanently stopped, and their state (working/stopped) is known. In fact, systems are often affected by grey…
We study power-set operations on classes of trees and tree algebras. Our main result consists of a distributive law between the tree monad and the upwards-closed power-set monad, in the case where all trees are assumed to be linear. For…
We study a standard operator on classes of languages: unambiguous polynomial closure. We prove that for every class C of regular languages satisfying mild properties, the membership problem for its unambiguous polynomial closure UPol(C)…
We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is an FO-definable language that is monotone in monadic predicates but not definable in FO+. This…
Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties are useful for specifying the chronological order of events…
A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in…
We study the emptiness and $\lambda$-reachability problems for unary and binary Probabilistic Finite Automata (PFA) and characterise the complexity of these problems in terms of the degree of ambiguity of the automaton and the size of its…
Letter-to-letter transducers are a standard formalism for modeling reactive systems. Often, two transducers that model similar systems differ locally from one another, by behaving similarly, up to permutations of the input and output…
Regular synchronization languages can be used to define rational relations of finite words, and to characterize subclasses of rational relations, like automatic or recognizable relations. We provide a systematic study of the decidability of…
We study the variety ZG of monoids where the elements that belong to a group are central, i.e., commute with all other elements. We show that ZG is local, that is, the semidirect product ZG * D of ZG by definite semigroups is equal to LZG,…
A function on an algebra is congruence preserving if, for any congruence, it maps pairs of congruent elements onto pairs of congruent elements. We show that on the algebra of binary trees whose leaves are labeled by letters of an alphabet…
We say that a language $L$ is \emph{constantly growing} if there is a constant $c$ such that for every word $u\in L$ there is a word $v\in L$ with $\vert u\vert<\vert v\vert\leq c+\vert u\vert$. We say that a language $L$ is…
A classic result in formal language theory is the equivalence among non-counting, or aperiodic, regular languages, and languages defined through star-free regular expressions, or first-order logic. Past attempts to extend this result beyond…
In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite…
Regular path queries (RPQs) are an essential component of graph query languages. Such queries consider a regular expression r and a directed edge-labeled graph G and search for paths in G for which the sequence of labels is in the language…
We have introduced a q-deformation, i.e., a polynomial in q with natural coefficients, of the binomial coefficient of two finite words u and v counting the number of occurrences of v as a subword of u. In this paper, we examine the…
The synthesis problem asks to automatically generate, if it exists, an algorithm from a specification of correct input-output pairs. In this paper, we consider the synthesis of computable functions of infinite words, for a classical Turing…
Regular expressions with backreferences (regex, for short), as supported by most modern libraries for regular expression matching, have an NP-complete matching problem. We define a complexity parameter of regex, called active variable…
In this paper, we consider fair assignment of complex requests for Mobility-On-Demand systems. We model the transportation requests as temporal logic formulas that must be satisfied by a fleet of vehicles. We require that the assignment of…