A process algebra with global variables

Mark Bouwman (Corresponding author), Bas Luttik, Wouter Schols, Tim A.C. Willemse

Research output: Contribution to journalConference articleAcademicpeer-review

Abstract

In standard process algebra, parallel components do not share a common state and communicate through synchronisation. The advantage of this type of communication is that it facilitates compositional reasoning. For modelling and analysing systems in which parallel components operate on shared memory, however, the communication-through-synchronisation paradigm is sometimes less convenient. In this paper we study a process algebra with a notion of global variable. We also propose an extension of Hennessy-Milner logic with predicates to test and set the values of the global variables, and prove correspondence results between validity of formulas in the extended logic and stateless bisimilarity and between validity of formulas in the extended logic without the set operator and state-based bisimilarity. We shall also present a translation from the process algebra with global variables to a fragment of mCRL2 that preserves the validity of formulas in the extended Hennessy-Milner logic.

Original languageEnglish
Pages (from-to)33-50
Number of pages18
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume322
DOIs
Publication statusPublished - 27 Aug 2020
EventCombined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020 - Virtual, Online, Austria
Duration: 31 Aug 2020 → …

Fingerprint Dive into the research topics of 'A process algebra with global variables'. Together they form a unique fingerprint.

Cite this