We provide new insights on the determinization and minimization of tree automata using congruences on trees. From this perspective, we study a Brzozowski's style minimization algorithm for tree automata. First, we prove correct this method relying on the following fact: when the automata-based and the language-based congruences coincide, determinizing the automaton yields the minimal one. Such automata-based congruences, in the case of word automata, are defined using pre and post operators. Now we extend these operators to tree automata, a task that is particularly challenging due to the reduced expressive power of deterministic top-down (or equivalently co-deterministic bottom-up) automata. We leverage further our framework to offer an extension of the original result by Brzozowski for word automata. Comment: 47 pages, 2 figures

We study the language inclusion problem L 1 ⊆ L 2 , where L 1 is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L 1 , obtained by approximating the Kleene iterates of its least fixpoint characterization, is included in L 2 . We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e., its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e., it guarantees termination of least fixpoint computations). This overapproximating abstraction of languages can be defined using quasiorder relations on words, where the abstraction gives the language of all the words “greater than or equal to” a given input word for that quasiorder. We put forward a range of such quasiorders that allow us to systematically design decision procedures for different language inclusion problems, such as regular languages into regular languages or into trace sets of one-counter nets, and context-free languages into regular languages. In the case of inclusion between regular languages, some of the induced inclusion checking procedures correspond to well-known state-of-the-art algorithms, like the so-called antichain algorithms. Finally, we provide an equivalent language inclusion checking algorithm based on a greatest fixpoint computation that relies on quotients of languages and, to the best of our knowledge, was not previously known.

In this work, we define a framework of automata constructions based on quasiorders over words to provide new insights on the class of residual automata. We present a new residualization operation and a generalized double-reversal method for building the canonical residual automaton for a given language. Finally, we use our framework to offer a quasiorder-based perspective on NL*, an online learning algorithm for residual automata. We conclude that quasiorders are fundamental to residual automata as congruences are to deterministic automata.

We present an algorithm for searching regular expression matches in compressed text. The algorithm reports the number of matching lines in the uncompressed text in time linear in the size of its compressed version. We define efficient data structures that yield nearly optimal complexity bounds and provide a sequential implementation -zearch- that requires up to 25% less time than the state of the art.

In this work we use a framework of finite-state automata constructions based on equivalences over words to provide new insights on the relation between well-known methods for computing the minimal deterministic automaton of a language.