基于 Lyapunov 方法的 CTMC 与 CTMDP 时间有界可达性分析

时间有界可达性是连续时间马尔可夫链（CTMC）与马尔可夫决策过程（CTMDP）在连续随机逻辑规约下模型检验的一个基本问题。它可通过数值求解特征线性动力系统来计算，但该过程计算代价高昂。我们采用控制理论方法，提出一种降维技术，即寻找另一个维度（变量数）更低的动力系统，使得数值求解该降阶动力系统能以有保证的误差界逼近原系统的解。我们的技术将可集总性（或概率互模拟）推广到定量设定。我们的主要结果是对两种动力学轨迹差的 Lyapunov 函数刻画，其依赖于初始失配并随时间呈指数衰减。特别地，该 Lyapunov 函数使我们能计算两动力学间的误差界及收敛速率。最后，我们证明降阶动力学的搜索可通过转移矩阵的 Schur 分解在多项式时间内完成。这使我们能通过计算刻画降阶动力学的上三角矩阵的指数来高效求解降阶动力系统。对于 CTMDP，我们使用分段二次 Lyapunov 函数针对切换仿射动力系统推广了我们的方法。我们通过其降阶切换系统为 CTMDP 综合出一种策略，保证时间有界可达概率高于某一阈值。我们给出了依赖于策略最小驻留时间的误差界。我们在排队网络实例上演示了该技术，对此可集总性不产生任何状态空间约简，而我们的技术使用模型的降阶版本综合出策略。