  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.
