Statistical Unbounded Verification (SUV)

SUV is a DFG project 383882557.

Probabilistic systems

Probabilistic models of systems are abundant in many areas ranging from telecommunication (randomized protocols), transportation (automotive, aerospace), operations research (queuing networks), biology (signalling pathways), to daily-life appliances (embedded software controllers), to name just a few. There is a variety of modelling formalisms used, most notably Markov chains for purely probabilistic systems and Markov decision processes with additional controllable or unknown uncontrollable behaviour. Besides, richer formalisms extend them in order to cope with additional issues, such as timing.

Probabilistic verification

These models are analyzed in order to ensure proper behaviour of safety-critical systems, low consumption of resource-limited systems, high mean time to failure of dependable systems, or to gain understanding of complex behaviour of natural processes. The traditional information to be inferred about the systems is specified either The information about the model can be verified by probabilistic model checking in the former case and by equivalence checking (or computing distance) in the latter one. Verification of probabilistic systems traditionally relies on numerical approaches. However, numerical analysis of the whole system is often inapplicable in practice: In such cases, statistical approaches and simulation form a powerful alternative.

Goal of SUV

This project develops statistical methods for probabilistic model checking and distance estimation, improve their performance, and extend their applicability, in particular to handle non-determinism and unbounded linear-time properties efficiently.