Formal Languages and Automata Theory
The Thue-Morse set T is the set of those non-negative integers whose binary expansions have an even number of 1. The name of this set comes from the fact that its characteristic sequence is given by the famous Thue-Morse word…
We investigate the state complexity of the star of symmetrical differences using modifiers and monsters. A monster is an automaton in which every function from states to states is represented by at least one letter. A modifier is a set of…
We propose a query learning algorithm for residual symbolic finite automata (RSFAs). Symbolic finite automata (SFAs) are finite automata whose transitions are labeled by predicates over a Boolean algebra, in which a big collection of…
The abelian critical exponent of an infinite word $w$ is defined as the maximum ratio between the exponent and the period of an abelian power occurring in $w$. It was shown by Fici et al. that the set of finite abelian critical exponents of…
The second author introduced with I. T\"orm\"a a two-player word-building game [Playing with Subshifts, Fund. Inform. 132 (2014), 131--152]. The game has a predetermined (possibly finite) choice sequence $\alpha_1$, $\alpha_2$, $\ldots$ of…
Cyber-physical systems come with increasingly complex architectures and failure modes, which complicates the task of obtaining accurate system reliability models. At the same time, with the emergence of the (industrial) Internet-of-Things,…
We investigate a learning algorithm in the context of nominal automata, an extension of classical automata to alphabets featuring names. This class of automata captures nominal regular languages; analogously to the classical language…
Choreographic approaches to message-passing applications can be regarded as an instance of the model-driven development principles. Choreographies specify interactions among distributed participants coordinating among themselves with…
The firing squad synchronization problem (FSSP, for short) is a problem in automata theory introduced in 1957 by John Myhill. Its goal is to design a finite automaton A such that, if copies of A are placed in a line and connected and are…
We consider the firing squad synchronization problems for paths in the two and the three-dimensional grid spaces. Minimal-time solutions of these problems are not known and are unlikely to exist. However, at present we have no proofs of…
We show how to calculate the operator algebra and the operator Lie algebra of a stochastic labelled-graph grammar. More specifically, we carry out a generic calculation of the product (and therefore the commutator) of time-evolution…
In this note we consider a new variant of network of splicing processors which simplifies the general model such that filters remain associated with nodes but the input and output filters of every node coincide. This variant is called {\it…
Splicing systems are generative mechanisms introduced by Tom Head in 1987 to model the biological process of DNA recombination. The computational engine of a splicing system is the "splicing operation", a cut-and-paste binary string…
Graph transformation systems (GTS) have been successfully proposed as a general, theoretically sound model for concurrency. Petri nets (PN), on the other side, are a central and intuitive formalism for concurrent or distributed systems,…
This work introduces a concept of explanations with respect to the violation of safe behaviours within software defined networks (SDNs) expressible in NetKAT. The latter is a network programming language that is based on a well-studied…
We propose a new robustness score for continuous-time Signal Temporal Logic (STL) specifications. Instead of considering only the most severe point along the evolution of the signal, we use average scores to extract more information from…
The process of decomposing a complex system into simpler subsystems has been of interest to computer scientists over many decades, for instance, for the field of distributed computing. In this paper, motivated by the desire to distribute…
This paper provides a geometric characterization of subclasses of the regular languages. We use finite model theory to characterize objects like strings and trees as relational structures. Logical statements meeting certain criteria over…
The verification of systems combining hard timing constraints with concurrency is challenging. This challenge becomes even harder when some timing constants are missing or unknown. Parametric timed formalisms, such as parametric timed…
In this paper we consider the reachability problem for bounded branching VASS. Bounded VASS are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the…