CTMCs和CTMDPs时间有界可达性的李雅普诺夫方法
A Lyapunov Approach for Time Bounded Reachability of CTMCs and CTMDPs
摘要：
时间有界可达性是连续随机逻辑规范的连续时间马尔可夫链（CTMC）和马尔可夫决策过程（CTMDP）模型检查中的一个基本问题。它可以通过数值求解特征线性动力系统来计算，但是该过程在计算上是昂贵的。我们采取控制理论的方法，并提出了一种减少技术，找到另一个动力系统的低维（变量数），这样，数值求解减少的动力系统提供了一个近似的解决方案，保证误差界的原始系统。我们的技术概括成块性（或概率互模拟）的定量设置。我们的主要结果是一个李雅普诺夫函数表征的两个动力学的轨迹，取决于初始失配和随时间呈指数下降的差异。特别是，李雅普诺夫函数使我们能够计算两个动态之间的误差界以及收敛速度。最后，我们表明，搜索的减少动力学可以计算在多项式时间使用舒尔分解的过渡矩阵。这使我们能够有效地解决减少动力系统通过计算上三角矩阵的指数表征减少的动态。对于CTMDPs，我们推广我们的方法使用分段二次李雅普诺夫函数切换仿射动力系统。我们合成的CTMDP通过其降阶切换系统，保证时间有界的可达性概率高于阈值的政策。我们提供的误差范围取决于最小停留时间的政策。我们展示了技术的例子，从集群网络，其中块不产生任何状态空间减少，但我们的技术合成的政策，使用减少版本的模型。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
