Verifying probabilistic systems : new algorithms and complexity results

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 anddiscrete-time stochastic transitions. The last two parts are concerned withnumerical 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