Event Category: Colloquium

It is known that deciding bisimilarity is a P-complete problem. This means it is thought of as a problem that is inherently sequential and hard to solve in parallel. Despite this fact efforts have been made to construct increasingly efficient parallel algorithms. In a previous colloquium I presented a parallel algorithm that decides bisimilarity in …continue reading

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 a system refines its specification. There are many refinement relations described in the literature. Fair testing is the coarsest liveness-preserving …continue reading

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 design flaws to be uncovered, before they emerge in the time and resource intensive testing phase. Some of the modelling …continue reading

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 environment during their working process. Reconfiguration provides many advantages to various existing systems. However, by adopting such aspect, some issues …continue reading

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 Peterson’s algorithm to n processes. In this talk, I will look at such generalisations. I will also describe how these …continue reading

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 used for two distinct purposes: (i) checking whether the original standard satisfies the requirements that are imposed upon them, and …continue reading

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 (LDDs) can be used to store sets of states and transitions in a compact manner. This has been demonstrated by …continue reading

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 an initial algebra and gives rise to an induction principle. In the talk we will focus on the inductive nature of …continue reading