Formal Languages and Automata Theory
Simulink is a widely used model-based development environment for embedded systems. Stateflow is a component of Simulink for modeling event-driven control via hierarchical state machines and flow charts. However, Stateflow lacks an official…
Anomaly-based intrusion detection systems are essential defenses against cybersecurity threats because they can identify anomalies in current activities. However, these systems have difficulties providing entity processing independence…
While finite automata have minimal DFAs as a simple and natural normal form, deterministic omega-automata do not currently have anything similar. One reason for this is that a normal form for omega-regular languages has to speak about more…
We present Assume-Guarantee-Repair (AGR) - a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs - these are simple…
A typewriter automaton is a special variant of a two-dimensional automaton that receives two-dimensional words as input and is only capable of moving its input head through its input word in three directions: downward, leftward, and…
We study runtime monitoring of $\omega$-regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain $\mathcal M$ is monitored against a fixed but arbitrary $\omega$-regular specification…
A synchronizing word of a deterministic finite complete automaton is a word whose action maps every state to a single one. Finding a shortest or a short synchronizing word is a central computational problem in the theory of synchronizing…
This work introduces a new problem, named as, affinity classification problem which is a generalization of the density classification problem. To solve this problem, we introduce temporally stochastic cellular automata where two rules are…
The Global Cellular Automata (GCA) Model is a generalization of the Cellular Automata (CA) Model. The GCA model consists of a collection of cells which change their states depending on the states of their neighbors, like in the classical CA…
The subject of this paper is to study conformance checking for timed models, that is, process models that consider both the sequence of events in a process as well as the timestamps at which each event is recorded. Time-aware process mining…
State machines are popular models to model and visualize discrete systems such as software systems, and to represent regular grammars. Most algorithms that passively learn state machines from data assume all the data to be available from…
Natural language is an intuitive way for humans to communicate tasks to a robot. While natural language (NL) is ambiguous, real world tasks and their safety requirements need to be communicated unambiguously. Signal Temporal Logic (STL) is…
We introduce regular languages of morphisms in free monoidal categories, with their associated grammars and automata. These subsume the classical theory of regular languages of words and trees, but also open up a much wider class of…
Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic…
The introduction of pattern languages in the seminal work [Angluin, ``Finding Patterns Common to a Set of Strings'', JCSS 1980] has revived the classical model of inductive inference (learning in the limit, gold-style learning). In…
The determinization of a nondeterministic B\"uchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as…
Reachability problems in infinite-state systems are often subject to extremely high complexity. This motivates the investigation of efficient overapproximations, where we add transitions to obtain a system in which reachability can be…
In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of $\omega$-context-free…
We revisit the problem of reducing incompletely specified Mealy machines with reactive synthesis in mind. We propose two techniques: the former is inspired by the tool MeMin and solves the minimization problem, the latter is a novel…
Let $A_N$ denote nondeterministic automatic complexity and \[ L_{k,c}=\{x\in [k]^* : A_N(x)> |x|/c\}. \] In particular, $L_{k,2}$ is the language of all $k$-ary words for which $A_N$ is maximal, while $L_{k,3}$ gives a rough dividing line…