Tesis:
A Uniform Approach to Language Containment Problems
- Autor: DOVERI KARRA, Kyveli
- Título: A Uniform Approach to Language Containment Problems
- Fecha: 2024
- Materia:
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: SIN DEPARTAMENTO DEFINIDO
- Acceso electrónico: https://oa.upm.es/81007/
- Director/a 1º: GANTY, Pierre
- Resumen: We introduce an algorithmic framework to decide the language inclusion for languages of infinite words. We define algorithms for different decidable cases like the inclusion between (nondeterministic) Büchi automata, a PSpace-complete problem, and the inclusion between Büchi Visibly Pushdown Automata, an EXPTime-complete problem. All our algorithms rely on a least fixpoint characterization of the languages, leveraging ultimately periodic words, i.e., infinite words of the form uvvvv... with u as a finite prefix and v as a finite period of an infinite word. They are parameterized by quasiorders, indicating which ultimately periodic words need not be tested as counterexamples to inclusion without compromising completeness.
Our first algorithm for the inclusion between Büchi automata is called BAIT and uses two quasiorders on finite words. BAIT is quite simple: it consists of two least fixpoint computations, one for prefixes and the other for periods, manipulating finite sets of states.
Our second algorithm for the inclusion between Büchi automata is called FORKLIFT. Its novelty is that it uses a family of quasiorders. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of a family of right congruences put forward by Maler and Staiger in 1993. FORKLIFT consists of two fixpoints for the prefixes and an unbounded number of fixpoints for the periods. Even though it computes more fixpoints, it scales up better than BAIT and the state-of-the-art on a variety of benchmarks, including benchmarks from program verification and theorem proving for word combinatorics.
Our third algorithm, called omegaVPLInc, decides the inclusion between Büchi Visibly Pushdown Automata. It uses a pair of quasiorders to prune the search for counterexamples to inclusion. We also implemented our algorithm and conducted an empirical evaluation on benchmarks from software verification.
Additionally, in this thesis we establish a Myhill-Nerode like theorem for specific subclasses of timed languages accepted by one-clock timed automata. The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to a canonical form, which in turn, is the basis of automata learning algorithms. Such an equivalence has been studied for various subclasses of timed languages, for instance, deterministic timed languages, and real-time languages (which are described by a one-clock timed automaton that is reset in every transition). In this work, we consider the subclass of timed automata with integer resets. This class is known to have good automata- theoretic properties and is also useful for practical modeling. We present a Nerode-style equivalence for this class that depends on a constant K and leads to the construction of a canonical one-clock integer-reset timed automaton with maximum constant K.
RESUMEN
Introducimos un marco algorítmico para decidir la inclusión de lenguajes de palabras infinitas. Definimos algoritmos para diferentes casos decidibles como la inclusión entre autómatas (no deterministas) Büchi, un problema PSpace-completo, y la inclusión entre autómatas Büchi Visibly Pushdown, un problema EXPTime-completo. Todos nuestros algoritmos se basan en una caracterización de punto fijo mínimo de los lenguajes, aprovechando palabras periódicas en última instancia, es decir, palabras infinitas de la forma uvvvv..., con u como prefijo finito y v como período finito de una palabra infinita. Están parametrizados por cuasi-órdenes, indicando qué palabras periódicas en última instancia no necesitan ser probadas como contraejemplos a la inclusión sin comprometer la completitud.
Nuestro primer algoritmo para la inclusión entre autómatas Büchi se denomina BAIT y utiliza dos cuasiórdenes sobre palabras finitas. BAIT es bastante sencillo: consiste en dos cálculos de punto fijo mínimo, uno para prefijos y otro para períodos, manipulando conjuntos finitos de estados.
Nuestro segundo algoritmo para la inclusión entre autómatas Büchi se llama FORKLIFT. Su novedad es que utiliza una familia de cuasiórdenes. Introducimos FORQs (family of right quasiorders) que obtenemos adaptando la noción de familia de congruencias derechas propuesta por Maler y Staiger en 1993. FORKLIFT consta de dos puntos fijos para los prefijos y un número ilimitado de puntos fijos para los períodos. A pesar de que calcula más puntos fijos, se adapta mejor que BAIT y el estado de la técnica en una variedad de puntos de referencia, incluyendo puntos de referencia de verificación de programas y demostración de teoremas para la combinatoria de palabras.
Nuestro tercer algoritmo, llamado omegaVPLInc, decide la inclusión entre autómatas Büchi Visibly Pushdown. Utiliza un par de cuasi-órdenes para podar la búsqueda de contraejemplos a la inclusión. También implementamos nuestro algoritmo y realizamos una evaluación empírica en puntos de referencia de verificación de software.
Además, en esta tesis establecemos un teorema similar al de Myhill-Nerode para subclases específicas de lenguajes temporizados aceptados por autómatas temporizados de un reloj. La conocida equivalencia de Nerode para palabras finitas desempeña un papel fundamental en nuestra comprensión de la clase de lenguajes regulares. La equivalencia conduce a una forma canónica que, a su vez, es la base de los algoritmos de aprendizaje de autómatas. Dicha equivalencia se ha estudiado para varias subclases de lenguajes temporizados, por ejemplo, los lenguajes temporizados deterministas y los lenguajes en tiempo real (que se describen mediante un autómata temporizado de un reloj que se reinicia en cada transición). En este trabajo, consideramos la subclase de autómatas temporizados con reinicios enteros. Se sabe que esta clase tiene buenas propiedades autómatas-teóricas y también es útil para el modelado práctico. Presentamos una equivalencia al estilo de Nerode para esta clase que depende de una constante K y conduce a la construcción de un autómata temporizado canónico de un reloj con restablecimiento entero y constante máxima K.