Efficient simultaneous exploration of Synchronising Linear Processes Equations
------------------------------------------------------------------------------

The mCRL2 toolset [1] can be used to explore and analyse the behaviour of complex software. An important step in the analysis is the generation of the state space of an mCRL2 specification. The toolset typically achieves this by first linearising the specification, which results in a so-called Linear Process Equation (LPE), from which a state space can be generated efficiently. In most cases this procedure works well, but sometimes the resulting state space is too large to further analyse, or the linearisation grinds to a halt due to the complicated communication structure used in the specification. A possible way around this is to define a network of LPEs, inspired by the notion of a network of LTSs [2]. The idea is that these can be explored in parallel, leading to multiple state spaces that can be combined afterwards. Doing so naively would lead to infinite-sized state spaces because the required synchronisation between the various LPEs in the network is not considered. In this project the assignment is thus to come up with algorithms and theory to do this in a more clever fashion.
 
[1] Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, Tim A. C. Willemse: The mCRL2 Toolset for Analysing Concurrent Systems - Improvements in Expressivity and Usability. TACAS (2) 2019: 21-39
 
[2] Frederic Lang, Radu Mateescu: Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems. Log. Methods Comput. Sci. 9(4) (2013)