Formal Languages and Automata Theory
The rules in a shape grammar apply in terms of embedding to take advantage of the parts that emerge visually in the appearance of shapes. While the shapes are kept unanalyzed as a computation moves forward, part-structures for shapes can be…
We provide a reformulation and a formalization of the classical result by Juhani Karhum\"aki characterizing intersections of two languages of the form $\{x,y\}^*\cap \{u,v\}^*$. We use the terminology of morphisms which allows to formulate…
We study the complexity of the reachability problem for Vector Addition Systems with States (VASSes) in fixed dimensions. We provide four lower bounds improving the currently known state-of-the-art: 1) \np-hardness for unary flat $4$-VASSes…
Implicit Computational Complexity (ICC) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers. Among the methods developed, the mwp-flow analysis…
We consider the positions of occurrences of a factor $x$ and its binary complement $\overline{x}$ in the Thue-Morse word ${\bf t} = {\tt 01101001} \cdots$, and show that these occurrences are "intertwined" in essentially two different ways.…
This paper studies the reduction (abstraction) of finite-state transition systems for control synthesis problems. We revisit the notion of alternating simulation equivalence (ASE), a more relaxed condition than alternating bisimulations, to…
We present an exponential-time algorithm approximating the minimal lookahead necessary to win an $\omega$-regular delay game.
In this paper, we study the extension of 1-clock Alternating Timed Automata (1-ATA) with the ability to read in both forward and backward direction, the 2-Way 1-clock Alternating Timed Automata (2-Way 1-ATA). We show that subclass of 2-Way…
We use results from communication complexity, both new and old ones, to prove lower bounds for unambiguous finite automata (UFAs). We show three results. $\textit{Complement:}$ There is a language $L$ recognised by an $n$-state UFA such…
The class of regular transformations has several equivalent characterizations such as functional MSO transductions, deterministic two-way transducers, streaming string transducers, as well as regular transducer expressions (RTE). For…
We investigate computational resources used by Turing machines (TMs) and alternating Turing machines (ATMs) to accept languages generated by coordinated table selective substitution systems with two components. We prove that the class of…
In this paper we study the number $r_{bwt}$ of equal-letter runs produced by the Burrows-Wheeler transform ($BWT$) when it is applied to purely morphic finite words, which are words generated by iterating prolongable morphisms. Such a…
In this paper we consider a number of natural decision problems involving k-regular sequences. Specifically, they arise from - lower and upper bounds on growth rate; in particular boundedness, - images, - regularity (recognizability by a…
We present $L^{\#}$, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the $L^{\ast}$ algorithm and its descendants, $L^{\#}$ takes a different perspective: it tries to establish…
Different classes of automata on infinite words have different expressive power. Deciding whether a given language $L \subseteq \Sigma^\omega$ can be expressed by an automaton of a desired class can be reduced to deciding a game between…
We explore in this paper a novel approach that builds an overapproximation of the state space of preemptive real time systems. Our graph construction extends the expression of a class to the time distance system that encodes the…
In this paper, we for the first time obtain characterization of four fundamental notions of detectability for general labeled weighted automata over monoids (denoted by $\mathcal{A}^{\mathfrak{M}}$ for short), where the four notions are…
Gauge-invariance is a fundamental concept in Physics -- known to provide mathematical justification for the fundamental forces. In this paper, we provide discrete counterparts to the main gauge theoretical concepts directly in terms of…
The verification of cyber-physical systems operating in a safety-critical environment requires formal system models. The validity of the verification hinges on the precision of the model: possible behavior not captured in the model can…
The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular winning conditions in order to generate certificates for the number of states that a…