Checking Refinement of Asynchronous Programs against Context-Free Specifications

TL;DR

This paper investigates the complexity of verifying asynchronous programs against Dyck language specifications, establishing EXPSPACE-completeness and proposing a novel reduction approach involving vector addition systems and regular language approximations.

Contribution

It introduces a new EXPSPACE-complete algorithm for refinement verification against Dyck languages, utilizing a downward closure construction and VASS reduction.

Findings

Verification problem is EXPSPACE-complete

Regular language approximation replaces context-free tasks

Reduction to vector addition systems enables decision procedures

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.