Timed Automata as Observers of Stochastic Processes
- Day - Time: 27 September 2011, h.11:00
- Place: Area della Ricerca CNR di Pisa - Room: C-40
Speakers
- Prof. Dr. Ir. Joost-Pieter Katoen (RWTH Aachen University, (Aquisgrana, Germania))
Referent
Abstract
In this talk, we will argue that (deterministic) timed automata are a natural specification formalism for practically relevant measures on stochastic processes. It will be discussed how DTA specifications can be checked on continuous-time Markov chains, an important class of stochastic processes used in the performance and dependability community, by using a product construction. We'll provide encouraging empirical results for checking single-clock DTA specifications and indicate how parallelization as well as bisimulation minimization can be naturally exploited in this setting. Finally, we shortly discuss the model checking of DTA specifications on a richer class of stochastic processes: continuous-time Markov decision processes (CTMDPs).