On the use of quasiorders in formal language theory

Valero Mejía, Pedro (2020). On the use of quasiorders in formal language theory. Thesis (Doctoral), E.T.S. de Ingenieros Informáticos (UPM). https://doi.org/10.20868/UPM.thesis.64477.

Description

Title: On the use of quasiorders in formal language theory
Author/s:
  • Valero Mejía, Pedro
Contributor/s:
  • Ganty, Pierre
Item Type: Thesis (Doctoral)
Date: May 2020
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img] PDF - Users in campus UPM only until 7 April 2021 - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB)

Abstract

In this thesis we use quasiorders on words to offer a new perspective on two wellstudied problems from Formal Language Theory: deciding language inclusion and manipulating the finite automata representations of regular languages. First, we present a generic quasiorder-based framework that, when instantiated w i t h different quasiorders, yields different algorithms (some of them new) for deciding language inclusion. We then instantiate this framework to devise an efficient algorithm for searching with regular expressions on grammar-compressed text. Finally, define a framework of quasiorder-based automata constructions to offer a new perspective on residual automata. The Language I n c l u s i o n P r o b l em First, we study the language inclusion problem L1 c L2 where L1 is regular or context-free and L2 is regular. Our approach relies on checking whether an overapproximation of L1, obtained by successively over-approximating the Kleene iterates of its least fixpoint characterization, is included in L2. We show that a language inclusion problem is decidable whenever the over-approximating function 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). Such over-approximation of L1 can be defined using quasiorder relations on words where the over-approximation gives the language of all words “greater than or equal to” a given input word for that quasiorder. We put forward a range of quasiorders that allow us to systematically design decision procedures for difi ferent 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. Some of the obtained inclusion checking procedures correspond to wellknown algorithms like the so-called antichains algorithms. On the other hand, our quasiorder-based framework allows us to derive an equivalent greatest fixpoint language inclusion check which relies on quotients of languages and which, to the best of our knowledge, was not previously known. Searching o n Compressed Text Secondly, we instantiate our quasiorder-based framework for the scenario in which L1 consists on a single word generated by a context-free grammar and L2 is the regular language generated by an automaton. The resulting algorithm can be used for deciding whether a grammar-compressed text contains a match for a regular expression. We then extend this algorithm in order to count the number of lines in the uncompressed text that contain a match for the regular expression. We show that this extension runs in time linear in the size of the compressed data, which might be exponentially smaller than the uncompressed text. Furthermore, we propose efficient data structures that yield optimal complexity bounds and an implementation - z e a r c h - that outperforms the state of the art, offering up to 40% speedup w i t h respect to highly optimized implementations of the decompress and search approach. Residual F i n i t e - S t a t e A u t o m a ta Finally, we present a framework of finite-state automata constructions based on quasiorders over words to provide new insights on residual finite-state automata (RFA for short). We present a new residualization operation and show that the residual equivalent of the double-reversal method holds, i.e. our residualization operation applied to a co-residual automaton generating the language L yields the canonical RFA for L. We then present a generalization of the double-reversal method for RFAs along the lines of the one for deterministic automata. Moreover, we use our quasiorder-based framework to offer a new perspective on NL*, an on-line learning algorithm for RFAs. We conclude that quasiorders are fundamental to residual automata in the same way congruences are fundamental for deterministic automata. ----------RESUMEN---------- En esta tesis, usamos preórdenes para dar un nuevo enfoque a dos problemas fundamentales en Teoría de Lenguajes Formales: decidir la inclusión entre lenguajes y manipular la representación de lenguajes regulares como autómatas finitos. En primer lugar, presentamos un esquema que, dado un preorden que satisface ciertos requisitos, nos permite derivar de manera sistemática algoritmos de decisión para la inclusión entre diferentes tipos de lenguajes. Partiendo de este esquema desarrollamos un algoritmo de búsqueda con expresiones regulares en textos comprimidos mediante gramáticas. Por último, presentamos una serie de autómatas, cuya definición depende de un preorden, que nos permite ofrecer un nuevo enfoque sobre la clase de autómatas residuales. El Problema de la I n c l u s ión de Lenguajes En primer lugar, estudiamos el problema de decidir L\ c l 2 > donde L\ es un lenguaje independiente de contexto y L2 es un lenguaje regular. Para resolver este problema, sobre-aproximamos los sucesivos pasos de la iteración de punto fijo que define el lenguaje L\. Con ello, obtenemos una sobre-aproximación de L\ y comprobamos si está incluida en el lenguaje L2. Esta técnica funciona siempre y cuando la sobre-aproximación sea completa (es decir, la imprecisión de la aproximación no produzca falsas alarmas) y evite cadenas infinitas ascendentes (es decir, garantice que la iteración de punto fijo termina). Para definir una sobre-aproximación que cumple estas condiciones, usamos un preorden. De este modo, la aproximación del lenguaje L\ contiene todas las palabras “mayores o iguales que” alguna palabra de L\. En concreto, definimos una serie de preórdenes que nos permiten derivar, de manera sistemática, algoritmos de decisión para diferentes problemas de inclusión de lenguajes como la inclusión entre lenguajes regulares o la inclusión de lenguajes independientes de contexto en lenguajes regulares. Algunos de los algoritmos obtenidos mediante esta técnica coinciden con algoritmos bien conocidos como los llamados antichains algorithms. Por otro lado, nuestra técnica también nos permite derivar algoritmos de punto fijo que, hasta donde sabemos, no han sido descritos anteriormente. Búsqueda en textos comprimidos En segundo lugar, aplicamos nuestro algoritmo de decisión de inclusión entre lenguajes al problema Li c L2, donde L\ es un lenguaje descrito por una gramática que genera una única palabra y L2 es un lenguaje regular definido por un autómata o expresión regular. De esta manera, obtenemos un algoritmo que nos permite decidir si un texto comprimido mediante una gramática contiene, o no, una coincidencia de una expresión regular dada. Posteriormente, modificamos este algoritmo para contar las líneas del texto comprimido que contienen coincidencias de la expresión regular. De este modo, obtenemos un algoritmo que opera en tiempo linear respecto del tamaño del texto comprimido el cual, por definición, puede ser exponencialmente más pequeño que el texto original. Además, describimos las estructuras de datos necesarias para que nuestro algoritmo opere en tiempo óptimo y presentamos una implementación -zearclique resulta hasta un 40% más rápida que las las mejores implementaciones del método estándar de descompresión y búsqueda. Autómatas Residuales Finalmente presentamos una serie de autómatas parametrizados por preórdenes que nos permiten mejorar nuestra compresión de la clase de autómatas residuales (abreviados como RFA). Estos autómatas parametrizados nos permiten definir una nueva operación de residualization y demostrar que el método de double-reversal funciona para RFAs, es decir, residualizar un autómata cuyo reverso es residual da lugar al canonical RFA (un RFA de tamaño mínimo). Tras esto, generalizamos este método de forma similar a su generalización para el caso de autómatas deterministas. Por último, damos un nuevo enfoque a NL*, un algoritmo de aprendizaje de RFAs. Como conclusión, encontramos que los preórdenes juegan el mismo papel para los autómatas residuales que las congruencias para los deterministas.

Funding Projects

TypeCodeAcronymLeaderTitle
Government of SpainPGC2018-102210-B-I00UnspecifiedUnspecifiedFundamentos para el desarrollo, análisis y comprensión de los blockchains y los contratos inteligentes
Government of SpainTIN2015-71819-PUnspecifiedUnspecifiedTecnologías rigurosas para el análisis y verificación de software concurrente y distribuido sofisticado
Madrid Regional GovernmentS2018/TCS-4339BLOQUES-CMUnspecifiedUnspecified
Madrid Regional GovernmentS2013/ICE-2731N-GREENS SOFTWA REUnspecifiedNext-GeneRation Energy-EfficieNt Secure Software
Government of SpainRYC-2016-20281UnspecifiedUnspecifiedUnspecified

More information

Item ID: 64477
DC Identifier: http://oa.upm.es/64477/
OAI Identifier: oai:oa.upm.es:64477
DOI: 10.20868/UPM.thesis.64477
Deposited by: Archivo Digital UPM 2
Deposited on: 08 Oct 2020 06:31
Last Modified: 08 Oct 2020 06:31
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM