A process algebra with global variables

TL;DR

This paper introduces a process algebra with global variables and an extended logic for reasoning about shared memory systems, providing formal correspondence results and translation to mCRL2.

Contribution

It presents a novel process algebra with global variables, extends Hennessy-Milner logic with predicates, and establishes formal relationships and translation methods.

Findings

Formal correspondence between logic validity and bisimilarity types.

Extension of process algebra to include global variables.

Translation from the algebra to mCRL2 preserves logical validity.

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.