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

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.