Join us for coffee and tea at 15.30 p.m.
Professor Joost-Pieter Katoen
RWTH Aachen University
and University of Twente
Observing Stochastic Processes by Timed Automata
We consider the automated verification of a continuous-time Markov chain C. For timed reachability objectives---can C reach a certain set of states within a deadline with a given likelihood---we show that this amounts to solving Volterra integral equation systems of the first type. Then, we consider the more general question of verifying CTMC C against a timed automaton A. The central problem is to compute the probability mass of runs in C that are accepted by A. We show that this can be solved by determining reachability probabilities in Davis' piecewise deterministic Markov processes. In fact this amounts to solve Volterra integral equations of the second type. For the special case of single clock timed automata, reachability probabilities in (our) PDMPs can be characterized by the least solution of a linear equation system, whose coefficients are ODE solutions. We show that this can be done very efficiently by employing a graph decomposition of the PDMP. This approach is amenable to bisimulation minimization and parallelization. Experiments with various examples from computer science as well as biology confirm that these optimizations lead to significant speed-ups.
Colloquium coordinators are Prof.dr. A.C.D. van Enter (e-mail : A.C.D.van.Enter@rug.nl) and
Dr. A.V. Kiselev (e-mail:
The University of Groningen (UG) will be awarding honorary doctorates to Prof. Titia de Lange and Dr Philipp Blom during its anniversary week in June 2019. Historian Blom will be awarded an honorary doctorate at the suggestion of Prof. Ann-Sophie Lehmann...
Prof. dr. Stynke Castelein, hoogleraar aan de Rijksuniversiteit Groningen en hoofd onderzoek bij Lentis, ontvangt de Vrouw in de Media Award 2018 Groningen.
Marc Kramer of the Faculty of Economics and Business has been chosen as Lecturer of the Year 2018.