形式语言与自动机理论

We study transformations of automata and games using Muller conditions into equivalent ones using parity or Rabin conditions. We present two transformations, one that turns a deterministic Muller automaton into an equivalent deterministic…

We present a polynomial time algorithm that constructs a deterministic parity automaton (DPA) from a given set of positive and negative ultimately periodic example words. We show that this algorithm is complete for the class of…

Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for…

We study the expressiveness and succinctness of history-deterministic pushdown automata (HD-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of…

We develop a theory of vector spaces spanned by orbit-finite sets. Using this theory, we give a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata…

This work proposes a hierarchical clustering algorithm for high-dimensional datasets using the cyclic space of reversible finite cellular automata. In cellular automaton (CA) based clustering, if two objects belong to the same cycle, they…

Hyperproperties enable simultaneous reasoning about multiple execution traces of a system and are useful to reason about non-interference, opacity, robustness, fairness, observational determinism, etc. We introduce hyper parametric timed…

Parikh's Theorem is a fundamental result in automata theory with numerous applications in computer science: software verification (e.g. infinite-state verification, string constraints, and theory of arrays), verification of cryptographic…

Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are write-only variables, that is, they do not affect the control flow of the automaton; thus…

Given a log and a specification, timed pattern matching aims at exhibiting for which start and end dates a specification holds on that log. For example, "a given action is always followed by another action before a given deadline". This…

Regular transition systems (RTS) are a popular formalism for modeling infinite-state systems in general, and parameterised systems in particular. In a CONCUR 22 paper, Esparza et al. introduce a novel approach to the verification of RTS,…

In the development of operational semantics of concurrent systems, a key decision concerns the adoption of a suitable notion of execution model, which basically amounts to choosing a class of partial orders according to which events are…

Interval-order partially ordered multisets with interfaces (ipomsets) have shown to be a versatile model for executions of concurrent systems in which both precedence and concurrency need to be taken into account. In this paper, we develop…

We report some further developments regarding the language theory of higher-dimensional automata (HDAs). Regular languages of HDAs are sets of finite interval partially ordered multisets (pomsets) with interfaces. We show a pumping lemma…

We introduce Merlin-Arthur (MA) automata where Merlin provides a certificate at the beginning of computation and it is scanned by Arthur before reading the input. We define Merlin-Arthur deterministic, probabilistic, and quantum finite…

This paper investigates the state complexities of subword-closed and superword-closed languages, comparing them to regular languages. We focus on the square root operator and the substitution operator. We establish an exponential lower…

Active learning of finite automata has been vigorously pursued for the purposes of analysis and explanation of black-box systems. In this paper, we study an L*-style learning algorithm for weighted automata over the max-plus semiring. The…

For any synchronizing $n$-state deterministic automaton, \v{C}ern\'{y} conjectures the existence of a synchronizing word of length at most $(n-1)^2$. We prove that there exists a synchronizing word of length at most $2n^2 - 7n + 7$ for…

Most Formal Languages and Automata Theory courses explore the duality between computation models to recognize words in a language and computation models to generate words in a language. For students unaccustomed to formal statements, these…

Data trees serve as an abstraction of structured data, such as XML documents. A number of specification formalisms for languages of data trees have been developed, many of them adhering to the paradigm of register automata, which is based…