Toggle Main Menu Toggle Search

Open Access padlockePrints

A Lyapunov Approach for Time Bounded Reachability of CTMCs and CTMDPs

Lookup NU author(s): Dr Sadegh Soudjani



This is the authors' accepted manuscript of an article that has been published in its final definitive form by ACM, 2020.

For re-use rights please refer to the publisher's terms and conditions.


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

Publication metadata

Author(s): Salamati A, Soudjani S, Majumdar R

Publication type: Article

Publication status: Published

Journal: ACM Transactions on Modeling and Performance Evaluation of Computing Systems (TOMPECS)

Year: 2020

Volume: 5

Issue: 1

Print publication date: 01/02/2020

Acceptance date: 08/11/2019

Date deposited: 11/12/2019

ISSN (print): 2376-3639

ISSN (electronic): 2376-3647

Publisher: ACM


DOI: 10.1145/3371923


Altmetrics provided by Altmetric


Find at Newcastle University icon    Link to this publication