Formal Languages and Automata Theory
Register automata extend classical finite automata with a finite set of registers that can store data from an infinite data domain for later equality comparisons with data from an input data word. While the registers in the original model…
We present several new results and connections between various extensions of finite automata through the study of vector automata and homing vector automata. We show that homing vector automata outperform extended finite automata when both…
In (DLT 2016) we studied timed context sensitive languages characterized by multiple stack push down automata (MPA), with an explicit bound on number of stages where in each stage at most one stack is used (k-round MPA). In this paper, we…
We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while…
A word $u$ is a scattered factor of $w$ if $u$ can be obtained from $w$ by deleting some of its letters. That is, there exist the (potentially empty) words $u_1,u_2,..., u_n$, and $v_0,v_1,..,v_n$ such that $u = u_1u_2...u_n$ and $w =…
Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite…
In this paper, we associate the idea of derivation languages with flat splicing systems and compare the families of derivation languages (Szilard and control languages) of these systems with the family of languages in Chomsky hierarchy. We…
We investigate the state complexity of the shuffle operation on regular languages initiated by Campeanu et al. and studied subsequently by Brzozowski et al. We shift the problem into the combinatorics domain by turning the problem of state…
Patterns provide a concise, syntactic way of describing a set of strings, but their expressive power comes at a price: a number of fundamental decision problems concerning (erasing) pattern languages, such as the membership problem and…
We give two different proofs of the fact that non-oblivious selection via regular group sets preserves normality. Non-oblivious here means that whether or not a symbol is selected can depend on the symbol itself. One proof relies on the…
The classical subset construction for non-deterministic automata can be generalized to other side-effects captured by a monad. The key insight is that both the state space of the determinized automaton and its semantics---languages over an…
A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left…
The transducer synthesis problem on finite words asks, given a specification $S \subseteq I \times O$, where $I$ and $O$ are sets of finite words, whether there exists an implementation $f: I \rightarrow O$ which (1) fulfils the…
Monadic decomposibility --- the ability to determine whether a formula in a given logical theory can be decomposed into a boolean combination of monadic formulas --- is a powerful tool for devising a decision procedure for a given logical…
We establish an Eilenberg-type correspondence for data languages, i.e. languages over an infinite alphabet. More precisely, we prove that there is a bijective correspondence between varieties of languages recognized by orbit-finite nominal…
In this paper we provide a positive answer to a question left open by Alur and and Deshmukh in 2011 by showing that equivalence of finite-valued copyless streaming string transducers is decidable.
Calude, Jain, Khoussainov, Li, and Stephan (2017) proposed a quasi-polynomial-time algorithm solving parity games. After this breakthrough result, a few other quasi-polynomial-time algorithms were introduced; none of them is easy to…
In this first paper, we look at the following question: are the properties of the Fibonacci tree still true if we consider a finitely generated tree by the same rules but rooted at a black node? The direct answer is no, but new properties…
Value iteration is a fundamental algorithm for solving Markov Decision Processes (MDPs). It computes the maximal $n$-step payoff by iterating $n$ times a recurrence equation which is naturally associated to the MDP. At the same time, value…
We investigate the star-free closure, which associates to a class of languages its closure under Boolean operations and marked concatenation. We prove that the star-free closure of any finite class and of any class of groups languages with…