Modeling and Analysis of Probabilistic Timed Systems
Prof. Joost-Pieter Katoen, RWTH Aachen University, Alemania y University of Twente, Holanda.
These lectures will cover the verification of continuous-time Markov chains as well as the compositional modeling of such models. The analysis will focus on efficient algorithms for timed reachability objectives on CTMCs, and expected time and long-run objectives for Markov automata, a model that extends CTMCs with nondeterminacy. We will also discuss the application of such models in the field of stochastic Petri nets (performance) and fault trees (reliability).