We consider a process language featuring both nondeterministic and probabilistic choice with an operational semantics taking distributions of processes as basic building blocks. For this langauge we propose a sound and complete axiomatization of rooted branching probabilistic bisimulation. Exploiting the notion of a concrete process and building on the completeness of strong probabilistic bisimulation, a …continue reading

For a smooth integration of classical automata theory and concurrency theory, one would like to consider process algebras including a constant denoting successful termination and binary operations for alternative and sequential composition. Using alternative composition and successful termination it is possible to express a notion of intermediate acceptance as it occurs, e.g., in (classical) finite …continue reading

Inductive theorem proving combines equational reasoning and induction to prove properties on ground terms. We present some basics, and show how it also applies in data structures not having a unique representation and in infinite data structures.

Discrete-time stochastic systems are an essential modelling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class of models, methods for the formal verification and synthesis of control strategies are computationally hard and generally rely on the use of approximate abstractions. Building on approximate abstractions, we …continue reading

The notion of conformance provides a rigorous basis for testing systems. In particular, a notion of hybrid conformance is useful in establishing a formal model-based technique for cyber-physical systems. A logical characterisation of conformance precisely specifies the set of formulae that are preserved and reflected by conformance. We present what is to our knowledge, the …continue reading

In this talk, first I give an overview of activities in our session type group in Imperial and how mCRL2 is used in our researches. Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication …continue reading

In this talk, I will discuss how the Boolean Satisfiability (SAT) problem can be solved using a parallel implementation of the Ant Colony Optimization (ACO) algorithm for execution on the Graphics Processing Unit (GPU). We propose a new efficient parallel strategy for the ACO algorithm executed entirely on the CUDA architecture, and perform experiments to …continue reading

After the PhD. defense of Maciej Gazda, I walked back with one of the committee members who explained me a game that he knew he could win, but he would not be able to tell how.

In this talk, we will give an overview of the additions and improvements to mCRL2 from the last couple of years. First, the mCRL2 language has been expanded with the possibility to specify probabilistic behaviour. Second, there are several new and improved implementations of behavioural relations: the GJKW algorithm for branching bisimulation with complexity O(m …continue reading

Rheumatoid Arthritis (RA) is an autoimmune disease that affects about one percent of the world population. A medicine for RA has not yet been found, current treatment options only decelerating the progress of the disease. In this work a Boolean network model for RA is analysed. Two kinds of models, synchronous and asynchronous are compared. …continue reading