On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues

TL;DR

This paper introduces guarded lists in data-based coordination languages to enhance expressiveness and performance, while ensuring correctness through a refinement approach, addressing model checking performance issues.

Contribution

It proposes guarded lists as a novel construct that improves efficiency and expressiveness, with a correctness-preserving refinement method.

Findings

Guarded lists increase performance in model checking.

They strictly enrich the expressiveness of coordination languages.

A correctness-preserving refinement approach is established.

Abstract

Concurrency theory has received considerable attention, but mostly in the scope of synchronous process algebras such as CCS, CSP, and ACP. As another way of handling concurrency, data-based coordination languages aim to provide a clear separation between interaction and computation by synchronizing processes asynchronously by means of information being available or not on a shared space. Although these languages enjoy interesting properties, verifying program correctness remains challenging. Some works, such as Anemone, have introduced facilities, including animations and model checking of temporal logic formulae, to better grasp system modelling. However, model checking is known to raise performance issues due to the state space explosion problem. In this paper, we propose a guarded list construct as a solution to address this problem. We establish that the guarded list construct increases performance while strictly enriching the expressiveness of data-based coordination languages. Furthermore, we introduce a notion of refinement to introduce the guarded list construct in a correctness-preserving manner.