1: \begin{abstract}
2: Time bounded reachability is a fundamental
3: problem in model checking continuous-time Markov chains (CTMCs)
4: and Markov decision processes (CTMDPs) for specifications in continuous stochastic logics.
5: It can be computed by numerically solving a characteristic linear dynamical system but the procedure
6: is computationally expensive.
7: We take a control-theoretic approach and
8: propose a reduction technique that finds another dynamical system of lower dimension (number of variables),
9: such that numerically solving the reduced dynamical system provides an approximation to the
10: solution of the original system with guaranteed error bounds.
11: Our technique generalises lumpability (or probabilistic bisimulation) to a quantitative setting.
12: Our main result is a Lyapunov function characterisation of the difference in the trajectories of the two dynamics
13: that depends on the initial mismatch and exponentially decreases over time.
14: In particular, the Lyapunov function enables us to compute an error bound between the two dynamics as well as
15: a convergence rate.
16: Finally, we show that the search for the reduced dynamics can be computed
17: in polynomial time using a Schur decomposition of the transition matrix.
18: This enables us to efficiently solve the reduced dynamical system by computing the exponential of an
19: upper-triangular matrix characterising the reduced dynamics.
20: For CTMDPs, we generalise our approach using piecewise quadratic Lyapunov functions for switched affine dynamical
21: systems. We synthesise a policy for the CTMDP via its reduced-order switched system
22: that guarantees the time bounded reachability probability lies above a threshold.
23: We provide error bounds that depend on the minimum dwell time of the policy.
24: We demonstrate the technique on examples from queueing networks, for which lumpability does not
25: produce any state space reduction but our technique synthesises policies using reduced version of the model.
26: \end{abstract}
27: