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.
Bachelor Research Project Assignments
Title: Modelling and verifying a non-atomic dual bakery algorithm with bounded tokens in mCRL2. Description:
Mutual exclusion algorithms typically rely on atomic access to shared variables. For instance, Peterson’s algorithm is correct under the assumption that both processes can atomically read from and write to the turn variable. A notable exception is Lamport's Bakery Algorithm , which does not rely on an atomicity assumption. The drawback to Lamport's algorithm is, however, that it relies on shared variables storing (unbounded) integers. This is inconvenient for an implementation of the algorithm. It also hampers an analysis using the mCRL2 toolset, because the associated statespace is infinite. Aravind and Hesse link propose a non-atomic dual bakery algorithm with bounded tokens [2,3]. The goal of this bachelor research project is to model the latter algorithm in mCRL2 and investigate to what extent the correctness of the algorithm can be analysed with the mCRL2 toolset.
 Lamport, L. A new solution of Dijkstra's concurrent programming problem. Commun. ACM 17: 453-455, 1974.  Aravind, A.A. and Hesselink, W. H. Nonatomic dual bakery algorithm with bounded tokens. Acta Informatica 48: 67-96, 2011.  Raynal, M. Concurrent Programming: Algorithms, Principles, and Foundations. Springer Press, 2013.