Statistical Unbounded Verification (SUV)
SUV is a DFG project 383882557.
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.
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:
- declaratively as satisfaction of a property such as a temporal-logic formula or a reward constraint, or
- behaviourally as conformance to another system.
In such cases, statistical approaches and simulation form a powerful alternative.
- when the system is too large due to state space explosion, or
- when the exact transitions are unknown (so-called black-box systems).
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.