Parity games are two-player, infinite duration games that can be used answer whether a property holds true of a system with a yes or no. In several application domains, one is not only interested in …continue reading

Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. We generalise learning from automata to a large class of state-based systems, using the theory of coalgebras. The approach relies …continue reading

In the last years an increasing number of companies have shown interest in applying verification techniques in model based software engineering and Océ is one of them. To apply such techniques it is necessary to …continue reading

Refinement checking plays an important role in system verification. This means that the correctness of the system is established by showing a refinement relation between two models; one for the implementation and one for the …continue reading

Analytical Software Design (ASD) enables model-based development of component software systems. Until now, functional verification of ASD systems is only possible on a per-component basis. There is no functional verification engine for ASD itself, so …continue reading

The xMAS language introduced a convenient way of high-level modeling and verification of communication fabrics. For micro-architectural models expressed in xMAS, it was shown that the problem of proving liveness could be transformed into a …continue reading

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 …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 …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 …continue reading

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 …continue reading