Rick Erkens: A Set Automaton to Locate All Pattern Matches in a Term
Term pattern matching is the problem of finding all pattern matches in a subject term, given a set of patterns. It is a fundamental algorithmic problem in for instance automated theorem proving and term rewriting. We present a set automaton solution for the term pattern matching problem that is based on match set derivatives where …continue reading
Bas Luttik: Equationally axiomatising parallel composition
I will overview some results pertaining to the (equational) axiomatisation of interleaving parallel composition.
Jan Friso Groote: Partition refinement algorithms for strong bisimulation are Omega(n log n)
A question haunting me for a while is whether the O(m log n) algorithm for strong bisimulation is optimal. We found a family of graphs that shows that any reasonable partition refinement algorithm is necessarily Omega(n log n), n being the number of states, steps to calculate strong bisimulation. This appeared to answer the question. …continue reading
Hans Zantema: Complexity of Simon’s problem in classical sense
Simon’s problem is a standard example of a problem that is exponential in classical sense, while it admits a linear solution in quantum computing. It is about a function f for which it is given that a unique non-zero vector s exists for which f(x) = f(x xor s) for all x. The goal is to find s. The …continue reading
Jan Martens: Solving bisimilarity and the relational coarsest partition problem in sub-linear parallel time seems hard
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
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 a system refines its specification. There are many refinement relations described in the literature. Fair testing is the coarsest liveness-preserving …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 design flaws to be uncovered, before they emerge in the time and resource intensive testing phase. Some of the modelling …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 environment during their working process. Reconfiguration provides many advantages to various existing systems. However, by adopting such aspect, some issues …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 Peterson’s algorithm to n processes. In this talk, I will look at such generalisations. I will also describe how these …continue reading