Analysis of Quantitative Properties: Attacking the State Explosion Problem

I will give an overview of research on quantitative analysis techniques I was involved in. The application domains range from timing analysis for real-time systems (WCET analysis) to Markov decision processes and continuous-time Markov chains. The common theme is that I will present different ways to tackle the state-explosion problem: symbolic, approximative and abstraction.

I will then focus on abstraction for concurrent probabilistic programs, which can be used to model and analyze network protocols.