Master Project Assignments
Title: mCRL2 with shared variables Description:
The process specification language mCRL2 does not have a notion of global variable; parallel components can only communicate by message passing. For many applications, especially when mCRL2 specifications are obtained through translation from another formalism that does have global variables, their absence in mCRL2 is inconvenient. It would therefore be interesting to investigate how a notion of global variable can be added to mCRL2, and what would be the theoretical and practical implications of such an addition.
The assignment would consist of addressing some of the following questions: What are the implications for the process-algebraic semantics of mCRL2 specifications? What are the appropriate notions of behavioural equivalence? How should global variables be used in modal logics for specifying properties of mCRL2 specifications? How would adding a notion of global variable to mCRL2 affect the tools in the mCRL2 toolset.
Title: Process Algebra with Signals Description:
There are various proposals in the process-algebraic literature for extending process algebra with a notion of signal [1,2]. In those proposals processes can emit information about their state to other processes without resorting to the message passing paradigm. There are several theoretical open questions pertaining these proposals. For instance, to what extent do the addition of signals increase the expressiveness of the process algebra, and is the equational theory presented in  sound and ground-complete for rooted branching bisimilarity. Furthermore, it would be interesting to develop the theory of a process algebra with data and signals. This could serve as a stepping stone towards and extension of mCRL2 with a notion of shared variable.
 Jan A. Bergstra and Jos C. M. Baeten. Process Algebra with Propositional Signals. Theoretical Computer Science 177(2):381-405, 1997.  Victor Dyseryn, Rob van Glabbeek and Peter Höfner. Analysing Mutual Exclusion using Process Algebra with Signals. In K. Peters and S. Tini (editors): Proceedings of EXPRESS/SOS 2017, pp. 18-34, 2017. Title: An ω-complete axiomatisation of interleaving and successful termination Description:
In , a finite ω-complete axiomatisation of the equational theory of the process algebra PA was presented. One of the axioms needed in this axiomatisation is not sound if the constant 1 (denoting immediate successful termination) is added to the theory. The assignment is to investigate whether a finite ω-complete axiomatisation exists for the extension of PA with the constant 1.
 Wan Fokkink and Bas Luttik. An ω-complete equational specification of interleaving (extended abstract). In: Ugo Montanari, José D.P. Rolim and Emo Welzl, editors, Proceedings of ICALP 2000, LNCS 1853, pp. 729-743, July 2000, Copyright © 2000 Springer-Verlag. Title: Analysis of non-atomic (group) mutual exclusion algorithms with the mCRL2 toolset Description: Many mutual exclusion algorithms rely on the assumption that reading and writing of shared variables is atomic; in particular, this is the case for Peterson's algorithm, which has already been analysed thoroughly with the mCRL2 toolset. The goal of this assignment is to analyse mutual exclusion algorithms not relying on such atomicity assumptions and investigate how their correctness can be convincingly established using the mCRL2 toolset that this is so. Also group mutual exclusion algorithms, and possibly other distributed can be investigated.