形式语言与自动机理论

We present the first algorithm for query learning Mealy machines with timers in a black-box context. Our algorithm is an extension of the L# algorithm of Vaandrager et al. to a timed setting. We rely on symbolic queries which empower us to…

We consider a variant of reachability in Vector Addition Systems (VAS) dubbed \emph{box reachability}, whereby a vector $v\in \mathbb{N}^d$ is box-reachable from $0$ in a VAS $V$ if $V$ admits a path from $0$ to $v$ that not only stays in…

In this paper, we present structural abstraction refinement, a novel framework for verifying the threshold problem of probabilistic programs. Our approach represents the structure of a Probabilistic Control-Flow Automaton (PCFA) as a Markov…

This paper studies the recursion-theoretic aspects of large-scale geometries of infinite strings, a subject initiated by Khoussainov and Takisaka (2017). We investigate several notions of quasi-isometric reductions between recursive…

We introduce presheaf automata as a generalisation of different variants of higher-dimensional automata and other automata-like formalisms, including Petri nets and vector addition systems. We develop the foundations of a language theory…

We present an extended automata learning framework that combines active automata learning with deductive inference. The learning algorithm asks membership and equivalence queries as in the original framework, but it is also given advice,…

We investigate binary sequences generated by non-Markovian rules with memory length $\mu$, similar to those adopted in Elementary Cellular Automata. This generation procedure is equivalente to a shift register and certain rules produce…

Since the seminal work by Angluin and the introduction of the L*-algorithm, active learning of automata by membership and equivalence queries has been extensively studied to learn various extensions of automata. For weighted automata,…

Two new classes of finite automata, called General hexagonal Boustrophedon finite automata and General hexagonal returning finite automata operating on hexagonal grids, are introduced and analyzed. The work establishes the theoretical…

Multiparty session types (MPST) are a type-based approach for specifying message-passing distributed systems. They rely on the notion of global type specifying the global behaviour and local types, which are the projections of the global…

We show that the regular separability problem of VASS reachability languages is decidable and $\mathbf{F}_{\omega}$-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that…

We study density of rational languages under shift invariant probability measures on spaces of two-sided infinite words, which generalizes the classical notion of density studied in formal languages and automata theory. The density for a…

This note corrects a technical error in the ACM Computing Surveys paper mentioned in the title. The flaw involved constructions for showing that timed automata with urgent locations have the same expressiveness as timed automata that allow…

Compositional automata learning is attracting attention as an analysis technique for complex black-box systems. It exploits a target system's internal compositional structure to reduce complexity. In this paper, we identify system…

Determining whether an unknown distribution matches a known reference is a cornerstone problem in distributional analysis. While classical results establish a rigorous framework in the case of distributions over finite domains, real-world…

In Formal Languages and Automata Theory courses, students find understanding nondeterministic finite-state and pushdown automata difficult. In many cases, this means that it is challenging for them to comprehend the operational semantics of…

This article presents a novel framework to provide Formal Languages and Automata Theory students design support for the development of regular expressions. This framework includes a design recipe for regular expressions and a customized…

Many Formal Languages and Automata Theory courses introduce students to Turing machine extensions. One of the most widely-used extensions endows Turing machines with multiple tapes. Although multitape Turing machines are an abstraction to…

This paper presents a state-merging algorithm for learning timed languages definable by Event-Recording Automata (ERA) using positive and negative samples in the form of symbolic timed words. Our algorithm, LEAP (Learning Event-recording…

In this paper we introduce the notion of a runtime consultant. A runtime consultant is defined with respect to some value function on infinite words. Similar to a runtime monitor, it runs in parallel to an execution of the system and…