A process algebra with global variables

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

Onderzoeksoutput: Bijdrage aan tijdschriftCongresartikelAcademicpeer review


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.

Originele taal-2Engels
Pagina's (van-tot)33-50
Aantal pagina's18
TijdschriftElectronic Proceedings in Theoretical Computer Science, EPTCS
StatusGepubliceerd - 27 aug 2020
EvenementCombined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020 - Virtual, Online, Oostenrijk
Duur: 31 aug 2020 → …

Vingerafdruk Duik in de onderzoeksthema's van 'A process algebra with global variables'. Samen vormen ze een unieke vingerafdruk.

Citeer dit