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.