Decidable Models of Recursive Asynchronous Concurrency

TL;DR

This paper introduces Nets with Nested Coloured Tokens (NNCTs), an extension of Petri nets, to model recursive asynchronous concurrency with shaped stacks, establishing their coverability problem as Tower-complete.

Contribution

It defines NNCTs, proves their coverability is Tower-complete, and links them to ACPS with shaped stacks, expanding the class of decidable recursive concurrent models.

Findings

NNCT's coverability problem is Tower-complete.

NNCT extends Petri nets with infinite token types.

Decidability results for ACPS with shaped stacks.

Abstract

Asynchronously communicating pushdown systems (ACPS) that satisfy the empty-stack constraint (a pushdown process may receive only when its stack is empty) are a popular decidable model for recursive programs with asynchronous atomic procedure calls. We study a relaxation of the empty-stack constraint for ACPS that permits concurrency and communication actions at any stack height, called the shaped stack constraint, thus enabling a larger class of concurrent programs to be modelled. We establish a close connection between ACPS with shaped stacks and a novel extension of Petri nets: Nets with Nested Coloured Tokens (NNCTs). Tokens in NNCTs are of two types: simple and complex. Complex tokens carry an arbitrary number of coloured tokens. The rules of NNCT can synchronise complex and simple tokens, inject coloured tokens into a complex token, and eject all tokens of a specified set of colours to predefined places. We show that the coverability problem for NNCTs is Tower-complete. To our knowledge, NNCT is the first extension of Petri nets, in the class of nets with an infinite set of token types, that has primitive recursive coverability. This result implies Tower-completeness of coverability for ACPS with shaped stacks.