License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2023.110
URN: urn:nbn:de:0030-drops-181622
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18162/
Baumann, Pascal ;
Ganardi, Moses ;
Majumdar, Rupak ;
Thinniyam, Ramanathan S. ;
Zetzsche, Georg
Checking Refinement of Asynchronous Programs Against Context-Free Specifications
Abstract
In the language-theoretic approach to refinement verification, we check that the language of traces of an implementation all belong to the language of a specification. We consider the refinement verification problem for asynchronous programs against specifications given by a Dyck language. We show that this problem is EXPSPACE-complete - the same complexity as that of language emptiness and for refinement verification against a regular specification. Our algorithm uses several technical ingredients. First, we show that checking if the coverability language of a succinctly described vector addition system with states (VASS) is contained in a Dyck language is EXPSPACE-complete. Second, in the more technical part of the proof, we define an ordering on words and show a downward closure construction that allows replacing the (context-free) language of each task in an asynchronous program by a regular language. Unlike downward closure operations usually considered in infinite-state verification, our ordering is not a well-quasi-ordering, and we have to construct the regular language ab initio. Once the tasks can be replaced, we show a reduction to an appropriate VASS and use our first ingredient. In addition to the inherent theoretical interest, refinement verification with Dyck specifications captures common practical resource usage patterns based on reference counting, for which few algorithmic techniques were known.
BibTeX - Entry
@InProceedings{baumann_et_al:LIPIcs.ICALP.2023.110,
author = {Baumann, Pascal and Ganardi, Moses and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
title = {{Checking Refinement of Asynchronous Programs Against Context-Free Specifications}},
booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
pages = {110:1--110:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-278-5},
ISSN = {1868-8969},
year = {2023},
volume = {261},
editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18162},
URN = {urn:nbn:de:0030-drops-181622},
doi = {10.4230/LIPIcs.ICALP.2023.110},
annote = {Keywords: Asynchronous programs, VASS, Dyck languages, Language inclusion, Refinement verification}
}
|
Keywords: |
|
Asynchronous programs, VASS, Dyck languages, Language inclusion, Refinement verification |
|
Collection: |
|
50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
05.07.2023 |
