Language inclusion algorithms as complete abstract interpretations

Ganty, Pierre and Ranzato, Francesco and Valero Mejía, Pedro (2019). Language inclusion algorithms as complete abstract interpretations. In: "26th International Symposium (SAS 2019)", 8-11 Oct 2019, Oporto, Portugal. ISBN 978-3-030-32304-2. pp. 140-161. https://doi.org/10.1007/978-3-030-32304-2.

Description

Title: Language inclusion algorithms as complete abstract interpretations
Author/s:
  • Ganty, Pierre
  • Ranzato, Francesco
  • Valero Mejía, Pedro
Item Type: Presentation at Congress or Conference (Article)
Event Title: 26th International Symposium (SAS 2019)
Event Dates: 8-11 Oct 2019
Event Location: Oporto, Portugal
Title of Book: Static analysis : 26th International Symposium (SAS 2019)
Date: 2019
ISBN: 978-3-030-32304-2
Volume: 11822
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Otro
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (493kB) | Preview

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 _xpoint characterization, is included in L2. We show that a language inclusion problem is decidable whenever this overapproximating abstraction satis_es a completeness condition (i.e. its loss of precision causes no false alarm) and prevents in_nite ascending chains (i.e. it guarantees termination of least _xpoint computations). Such overapproximating abstraction function on languages can be de_ned 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 di_erent 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 _xpoint language inclusion check which relies on quotients of languages and, to the best of our knowledge, was not previously known.

Funding Projects

TypeCodeAcronymLeaderTitle
Government of SpainPGC2018-102210-B-I00UnspecifiedFundación IMDEA SoftwareFundamentos para el desarrollo, análisis y comprensión de los blockchains y los contratos inteligentes
Madrid Regional GovernmentS2018/TCS-4339BLOQUES-CMUnspecifiedContratos inteligentes y blockchains escalables y seguros mediante verificación y análisis
Government of SpainRYC-2016-20281UnspecifiedFundación IMDEA SoftwareUnspecified

More information

Item ID: 57610
DC Identifier: http://oa.upm.es/57610/
OAI Identifier: oai:oa.upm.es:57610
DOI: 10.1007/978-3-030-32304-2
Official URL: https://link.springer.com/content/pdf/10.1007%2F978-3-030-32304-2.pdf
Deposited by: Memoria Investigacion
Deposited on: 13 Apr 2020 10:14
Last Modified: 13 Apr 2020 10:14
  • 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