We study the language inclusion problem L1 ⊆ L2 where L1 is regular. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L1, obtained by successively overapproximating the Kleene iterates of its least fixpoint characterization, is included in L2. 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). Such overapproximating abstraction function on languages can be defined using quasiorder relations on words where the abstraction 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 different language inclusion problems such as regular languages into regular languages or into trace sets of one-counter nets. 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 greatest fixpoint language inclusion check which relies on quotients of languages and, to the best of our knowledge, was not previously known.

Language Inclusion Algorithms as Complete Abstract Interpretations

GANTY, PIERRE ANDRE';Ranzato, Francesco
;
2019

Abstract

We study the language inclusion problem L1 ⊆ L2 where L1 is regular. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L1, obtained by successively overapproximating the Kleene iterates of its least fixpoint characterization, is included in L2. 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). Such overapproximating abstraction function on languages can be defined using quasiorder relations on words where the abstraction 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 different language inclusion problems such as regular languages into regular languages or into trace sets of one-counter nets. 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 greatest fixpoint language inclusion check which relies on quotients of languages and, to the best of our knowledge, was not previously known.
2019
Proceedings of 26th International Static Analysis Symposium, SAS 2019
978-3-030-32303-5
978-3-030-32304-2
File in questo prodotto:
File Dimensione Formato  
published-paper.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Published (publisher's version)
Licenza: Accesso privato - non pubblico
Dimensione 509.38 kB
Formato Adobe PDF
509.38 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
sas.pdf

accesso aperto

Descrizione: Articolo principale in preprint
Tipologia: Preprint (submitted version)
Licenza: Accesso gratuito
Dimensione 481.89 kB
Formato Adobe PDF
481.89 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/3312173
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 1
social impact