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

Research output: Contribution to journalArticlepeer-review

3 Downloads (Pure)


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 databased coordination languages. Furthermore, we introduce a notion of refinement to introduce the guarded list construct in a correctness-preserving manner.

Original languageEnglish
Pages (from-to)55-72
Number of pages18
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Publication statusPublished - 21 Aug 2023
Event16th Interaction and Concurrency Experience, ICE 2023 - Lisbon, Portugal
Duration: 19 Jun 2023 → …


Dive into the research topics of 'On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues'. Together they form a unique fingerprint.

Cite this