形式语言与自动机理论

The state complexity, respectively, nondeterministic state complexity of a regular language $L$ is the number of states of the minimal deterministic, respectively, of a minimal nondeterministic finite automaton for $L$. Some of the most…

A model of an information system describes its processes and how resources are involved in these processes to manipulate data objects. This paper presents an extension to the Petri nets formalism suitable for describing information systems…

In time Petri nets (TPNs), time and control are tightly connected: time measurement for a transition starts only when all resources needed to fire it are available. Further, upper bounds on duration of enabledness can force transitions to…

We study minimization problems for deterministic $\omega$-automata in the presence of don't care words. We prove that the number of priorities in deterministic parity automata can be efficiently minimized under an arbitrary set of don't…

We establish a Myhill-Nerode type theorem for higher-dimensional automata (HDAs), stating that a language is regular if and only if it has finite prefix quotient. HDAs extend standard automata with additional structure, making it possible…

An absent factor of a string $w$ is a string $u$ which does not occur as a contiguous substring (a.k.a. factor) inside $w$. We extend this well-studied notion and define absent subsequences: a string $u$ is an absent subsequence of a string…

We present a formal and constructive framework for simulating Alternating Finite Automata (AFAs) using Logic-Gated Time-Shared Feedforward Networks (LG-TS-FFNs). Unlike prior neural automata models limited to Nondeterministic Finite…

We construct automata with input(s) in base $k$ recognizing some basic relations and study their number of states. We also consider some basic operations on $k$-automatic sequences $(h(i))_{i \geq 0}$ and discuss their state complexity. We…

This paper lays out the formal foundations upon which the SCAN statistical model checker is built.

History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some…

Timed automata are a widely used formalism for specifying the discrete-state/continuous-time behavior of time-critical reactive systems. For the fundamental verification problem of comparing two timed automata, it has been shown that timed…

We propose novel algorithms for sequence prediction based on ideas from stringology. These algorithms are time and space efficient and satisfy mistake bounds related to particular stringological complexity measures of the sequence. In this…

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. In their original definition, patterns only allow for…

A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA A obtains a mean payoff, and every word w is assigned the maximal mean payoff obtained by…

We present an algorithm for regular expression parsing and submatch extraction based on tagged deterministic finite automata. The algorithm works with different disambiguation policies. We give detailed pseudocode for the algorithm,…

Existing literature on timed opacity uses specific definitions for restricted subclasses of timed automata or limited observation models. This lack of a unified definition makes it difficult to establish formal relationships and compare the…

Many Cyber Physical System (CPS) work in a safety-critical environment, where correct execution, reliability and trustworthiness are essential. Signal Temporal Logic (STL) provides a formal framework for checking safety-critical CPS.…

This paper investigates the conditions under which a given circular (synchronizing) DFA is \emph{simple} (sometimes referred to as \emph{primitive}) and when it is \emph{irreducible}. Our notion of irreducibility slightly differs from the…

Automata over infinite alphabets have emerged as a convenient computational model for processing structures involving data, such as nonces in cryptographic protocols or data values in XML documents. We introduce active learning methods for…

Data words with binders formalize concurrently allocated memory. Most name-binding mechanisms in formal languages, such as the $\lambda$-calculus, adhere to properly nested scoping. In contrast, stateful programming languages with explicit…