Erik de Vink: On Quantum Process Algebra
After a quick intro to quantum computing addressing Deutsch’s problem, we turn to quantum teleportation and look into what may be needed to handle such with a tool like (probabilistic) mCRL2.
Maurice Laveaux: Antichain Based Algorithm for Fair Testing
The notion of refinement plays an important role in software engineering. It is the basis of a stepwise development methodology in which the correctness of a system can be established by proving, or computing, that …continue reading
Ferry Timmers: State-space exploration of generated system controllers
Model-driven system engineering is a practice also employed in the design of controllers for cyber-physical systems. The method allows controllers to be modelled and verified before they are implemented in software, allowing potential glitches and …continue reading
Yousra Hafidi: Modeling and Improved Verification of Reconfigurable Discrete Event Systems using R-TNCESs Formalism
Reconfigurability is a concept that appeared recently in several areas including manufacturing, aerospace, medical, robotic, and telecommunication systems. This concept provides systems with an aspect of flexibility allowing them to easily adapt with their external …continue reading
Jeroen Keiren: Peterson’s mutual exclusion algorithm for n processes
When talking about mutual exclusion, many textbooks start by introducing Peterson’s algorithm for two processes. The algorithm looks very simple, but upon closer inspection its behaviour is deceptively subtle. Less commonly known are extensions of …continue reading
Mark Bouwman: Direct formalization of EULYNX SysML in mCRL2
FormaSig aims to strengthen railway signalling standardization processes with the use of formal methods. The concrete approach investigated in FormaSig is to derive formal mCRL2 models from existing SysML specifications. These formal models are then …continue reading
Wieger Wesselink: Symbolic Reachability using LDDs
The mCRL2 toolset contains several applications in which computing the set of reachable states of a transition relation plays a role. For example in state space generation and in solving a PBES. List decision diagrams …continue reading
Herman Geuvers: Relating Apartness and Bisimulation
We have studied the dual of bisimulation: the notion of “apartness”. Intuitively, two elements are apart if there is a positive way to distinguish them. Apartness is the dual of bisimilarity in a precise categorical sense: apartness is …continue reading
Flip van Spaendonck: “Automatic Sequences: The effect of local changes on complexity”
We take a look at k-DFAOs, which are Deterministic Finite Automata with Output with a special property: each k-DFAO represents a k-automatic sequence a, an infinite sequence in which the i-th element is the output …continue reading
Olav Bunte: Evidence for behavioural inequivalence
Whenever two Labelled Transition Systems (LTSs) are behaviourally inequivalent to each other, one may be interested why this is the case. Using a modal logic that characterises such a behavioural equivalence one can create formulae …continue reading