AIB 2014-16: Verifying Probabilistic Systems: New Algorithms and Complexity Results

[Thomas Ströder]

The following technical report is available from
http://aib.informatik.rwth-aachen.de:

Verifying Probabilistic Systems: New Algorithms and Complexity Results
Hongfei Fu
AIB 2014-16

The content of the dissertation falls in the area of formal verification
of probabilistic systems.
It comprises four parts listed below:


1. the decision problem of (probabilistic) simulation preorder between
probabilistic pushdown automata (pPDAs) and finite probabilistic
automata (fPAs);

2. the decision problem of a bisimilarity metric on finite probabilistic
automata (fPAs);

3. the approximation problem of acceptance probability of
deterministic-timed-automata (DTA) objectives on continuous-time Markov
chains (CTMCs);

4. the approximation problem of cost-bounded reachability probability on
continuous-time Markov decision processes (CTMDPs).

The first two parts are concerned with equivalence checking on
probabilistic automata, where probabilistic automata (PAs) are an
analogue of discrete-time Markov decision processes that involves both
non-determinism and discrete-time stochastic transitions. The last two
parts are concerned with numerical algorithms on Markov jump processes.
In Part 1 and Part 2, we mainly focus on complexity issues; as for Part
3 and Part 4, we mainly focus on numerical approximation algorithms.