Lois Nijland: Adding sequential composition and termination to the linear time – branching time spectrum
Van Glabbeek presented the linear time – branching time spectrum of behavioural semantics and gave sound, ground-complete axiomatisations for the process theory BCCSP. Groote and Chen et al. proved for the semantics in the spectrum …continue reading
Astrid Belder: Decidability of bisimilarity and axiomatisation for sequential processes in the presence of intermediate termination
An alternative semantics for sequential composition in a setting with intermediate termination was proposed in a recent article by Baeten, Luttik and Yang. We consider two open questions regarding sequential processes with intermediate termination that …continue reading
Maurice Laveaux: Abstracting real-valued parameters in parameterised Boolean equation systems
The mCRL2 tool-set utilizes parameterised boolean equation systems to verify formulas from modal mu-calculus on models written in the minimal common representation language (mCRL2). For models of real-timed systems this introduces real-valued parameters in these …continue reading
Roxana Paval: Modeling and Verifying Concurrent Data Structures
Concurrent data structures can be used to communicate between parallel processes in a system. The challenge in manipulating these objects arises from the many possible ways in which the processes can interleave. To ensure correct …continue reading
Perry van Wesel: Formal analysis of ring networks
Systems-on-Chips rely on the correct functioning of the communication between their components. As these systems grow more complex, so do the underlying communication networks. Simulating a network does not guarantee the entire state-space is explored, …continue reading