Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic (Extended Version)

技术摘要：通过概率时序逻辑进行马尔可夫跳变线性系统的稳定性检查

问题陈述
马尔可夫跳变线性系统（MJLSs）用于模拟受离散时间马尔可夫链控制的、在多个线性模式之间进行随机切换的动力学现象。MJLSs 的经典稳定性分析依赖于全局概念，如均值稳定性（MS）和均方稳定性（MSS），这些概念表征了系统状态的一阶矩和二阶矩的渐近行为。这些经典方法通常要求对所有初始条件提供稳定性保证。作者认为，这种全局视角在实践中可能过于保守或具有误导性。具体而言，不稳定性可能仅由极小部分的初始状态引起（例如，物理上不可达的配置），而系统对于所有实际相关的状态都是稳定的。相反，一个系统可能对所有初始状态都收敛，但收敛到不同的极限值，尽管表现出理想的收敛行为，却未能满足严格的稳定性定义（稳定性要求收敛到一个共同的值，通常是原点）。

本文解决了文献中关于针对特定初始状态集合验证稳定性属性的空白。这被框架化为一个模型检测问题，其目标是确定对于给定的状态空间子集，特定的时序性质关于矩收敛是否成立。

方法论
作者通过将稳定性分析嵌入到概率计算树逻辑（PCTL）的框架中来解决这一问题。

1. MJLSs 上的 PCTL 形式化：
   论文首先将标准的 PCTL 在 MJLSs 上形式化。状态空间定义为 $S_J = \mathbb{R}^n \times \{1, \dots, m\}$，结合了连续状态变量和离散马尔可夫模式。原子命题定义在连续状态的凸多胞形和离散状态的特定模式之上。满足关系定义在无限路径上，其概率基于由底层马尔可夫链导出的柱集（cylinder sets）进行计算。

2. 通用 PCTL 模型检测的局限性：
   作者分析了在 MJLSs 上全量 PCTL 逻辑（包括无界的“直到”算子）的可判定性。他们建立了 MJLSs 可以嵌入到一般马尔可夫过程（GMPs）中的结论。利用线性动力系统（LDSs）是 MJLSs 的确定性特例这一事实，他们证明了 MJLSs 上 PCTL 的可达性问题继承了与 Skolem 问题相关的不可判定性结果。具体而言，在 LDSs 中确定维度为四或更高的集合的可达性是一个开放问题，这意味着 MJLSs 上 PCTL 的通用模型检测问题（超出步长限制片段 $PCTL^-$）也是开放的，且很可能是不可判定的。

3. 带有稳定性算子的扩展：
   为了克服全局稳定性定义的局限性和通用可达性的不可判定性，作者使用新的原子命题扩展了 PCTL，这些命题捕捉了相对于特定初始状态的基于矩的稳定性属性。

   • 算子： 他们引入了步长限制型（$E^k_\Pi, V^k_\Xi$）和步长无限制型（$E_\Pi, V_\Xi$）算子。
     • $E_\Pi$ 和 $V_\Xi$ 用于检查一阶矩（期望值）和二阶矩（非中心方差）的 Cesàro 极限（时间平均极限）是否落在指定的凸多胞形（$\Pi$ 或 $\Xi$）内。
     • 这些算子利用 Cesàro 极限而非逐点极限，以处理可能不具备逐点收敛性但具有确定的平均值的振荡行为。
   • 代数方法： 这些新算子的验证依赖于线性代数技术，而非通用的可达性分析。
     • 条件矩的演化由线性算子控制：一阶矩使用 $B_J$，二阶矩使用 $T_J$。
     • 无限制型算子的满足集通过分析这些算子的谱性质（特征值、特征向量/若尔当块）来计算。
     • 对于可对角化算子，极限由初始状态在对应于单位圆上特征值的特征空间上的投影决定。
     • 对于不可对角化算子，作者采用若尔当标准型进行符号化的极限计算，处理项发散或抵消的情况。

主要贡献与结果

• 逻辑框架： 论文为 MJLSs 提供了一套形式语义，并扩展了 PCTL 以包含用于指定相对于特定初始状态集的稳定性属性的算子。
• 算法验证：
  • 提供了一个针对步长限制片段（$PCTL^-$）和新稳定性算子（$E_\Pi, V_\Xi$ 等）的判定程序。
  • 这些算法将稳定性算子的验证问题归约为求解线性方程组并检查在凸多胞形中的成员资格。这确保了所得的满足集是可表示的（作为凸集或其并集），并且在可以计算特征值的前提下是计算上可行的。
  • 作者证明了虽然由于与 Skolem 问题的联系，通用的 PCTL 模型检测问题是开放的，但处理矩稳定性的特定片段可以通过线性代数进行判定。
• 处理振荡： 通过使用 Cesàro 极限，所提出的算子能够捕捉一种即使在矩序列发生振荡时依然保持良定义的收敛概念，这与可能因此失效的经典定义形成对比。
• 案例研究： 论文包含了计算示例（例如一个具有 2 个状态变量的 3 模式 MJLS），可视化了满足诸如 $P_{\ge 0.3}(\Lambda \mathcal{U}_{\le 5} E_\Pi)$ 等复杂稳定性与可达性要求的公式的满足集。

意义与主张
作者声称，其工作实现了一种此前无法表达或判定的“精细化”视角下的 MJLS 稳定性。通过脱离全局保证，该框架允许分析人员：

1. 识别针对特定、实际相关初始条件的稳定性属性，从而避免全局分析的保守性。
2. 在单个逻辑公式内，将稳定性属性与经典的到达或分支时间目标相结合。
3. 利用概率模型检测作为状态相关稳定性分析的自然框架。

论文对于其可判定性范围的描述保持了适度的审慎。它明确承认，由于与数学中长期存在的开放问题（Skolem 问题）密切相关，MJLSs 上通用的步长无限制 PCTL 属性的模型检测问题仍然是开放的。此外，它还指出了实现中的实际限制：由于 Abel-Ruffini 定理的存在，对于维度大于 4 的矩阵，通常无法进行精确的特征值计算，这意味着对于更大的系统，分析依赖于数值近似而非精确的符号解。论文总结道，虽然富含稳定性算子的特定逻辑（排除通用的无限制直到算子）可以通过线性代数技术实现可判定，但反向嵌套（将 PCTL 公式嵌入到稳定性算子内部）在当前框架中并不受支持，且其模型检测问题也将是开放的。