形式语言与自动机理论

A subsequence of a word $w$ is a word $u$ such that $u = w[i_1] w[i_2] \cdots w[i_k]$, for some set of indices $1 \leq i_1 < i_2 < \dots < i_k \leq \vert w \vert$. A word $w$ is \emph{$k$-subsequence universal} over an alphabet $\Sigma$ if…

In inductive inference, we investigate the learnability of classes of formal languages. We are interested in what classes of languages are learnable in certain learning settings. A class of languages is learnable, if there is a learner that…

We study algorithmic complexity and expressive power of fusion grammars, a novel formalism introduced in [Kreowski, Kuske, and Lye 2017], which extends hyperedge replacement grammars. In the first part of the work, we prove that the…

Conformance testing of automata is about checking the equivalence of a known specification and a black-box implementation. An important notion in conformance testing is that of a complete test suite, which guarantees that if an…

We introduce a novel paradigm for reducing the size of finite automata by compressing repeating sub-graphs. These repeating sub-graphs can be viewed as invocations of a single procedure. Instead of representing each invocation explicitly,…

Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, over which the properties are checked. However, creating…

In this paper, we introduce rerailing automata for $\omega$-regular languages. They generalize both deterministic parity (DPW) and minimized history-deterministic co-B\"uchi automata (with transition based acceptance, HdTbcBW) while…

We study the space complexity of the following problem: For a fixed regular language $L$, we receive a stream of symbols and want to test membership of a sliding window of size $n$ in $L$. For deterministic streaming algorithms we prove a…

In this paper, we introduce a novel method for active learning of deterministic real-time one-counter automata (DROCA). The existing techniques for learning DROCA rely on observing the behaviour of the DROCA up to exponentially large…

Hybrid Rebeca is a modeling framework for asynchronous event-based cyber-physical systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. Besides the syntactical extension, we…

Takai proposed a method for constructing a maximally permissive supervisor for the similarity control problem (IEEE Transactions on Automatic Control, 66(7):3197-3204, 2021). This paper points out that this construction does…

Markov decision process over vector addition system with states (VASS MDP) is a finite state model combining non-deterministic and probabilistic behavior, augmented with non-negative integer counters that can be incremented or decremented…

A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult to detect, yet a high level of confidence in the outcome is…

We give an active learning algorithm for deterministic one-counter automata (DOCAs) where the learner can ask the teacher membership and minimal equivalence queries. The algorithm called OL* learns a DOCA in time polynomial in the size of…

Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability…

In this paper, we introduce a restriction of Timed Automata (TA), called non-resetting test Timed Automata (nrtTA). An nrtTA does not allow to test and reset the same clock on the same transition. The model has the same expressive power of…

Regular transductions over finite words have linear input-to-output growth. This class of transductions enjoys many characterizations. Recently, regular transductions have been extended by Boja\'nczyk to polyregular transductions, which…

We characterize the words that can be mapped to arbitrarily high powers by injective morphisms. For all other words, we prove a linear upper bound for the highest power that they can be mapped to, and this bound is optimal up to a constant…

Patterns are words with terminals and variables. The language of a pattern is the set of words obtained by uniformly substituting all variables with words that contain only terminals. Length constraints restrict valid substitutions of…

Inspired by Martin Fr\"anzle's persistent and influential work on capturing and handling delay inherent to cyber-physical systems in the formal verification of such systems, we study timed games where controllable actions do not take effect…