概率系统的LTL模型检查与定性默认推理研究

### 概率系统的LTL模型检查与定性默认推理研究 概率系统的验证与推理在计算机科学和人工智能领域中具有重要意义。本文将深入探讨概率系统的线性时态逻辑（LTL）模型检查以及定性默认推理与概率之间的关系。 #### 概率系统的LTL模型检查 在概率系统的验证中，我们将概率验证问题简化为概率满足问题。该问题的核心在于检查给定概率系统中的所有路径是否以正概率满足给定的（线性时间）规范。 ##### 同步积 经典的基于自动机的验证方法首先构建系统和（取反的）规范ω - 自动机的同步积。同步积本质上是两个图的笛卡尔积，仅保留具有相同标签的转移对。 设概率系统 $M = ⟨S, T_M, α_M, β_M, λ_M, P_0, P⟩$ 和 ω - 自动机 $A = ⟨Q, T_A, α_A, β_A, λ_A, Q_0, Acc⟩$。同步积 $M ⊗ A = ⟨S × Q, T_⊗, α_⊗, β_⊗, λ_⊗, S_0 × Q_0, Acc_⊗⟩$ 的定义如下： - $T_⊗ = \{(t_M, t_A) ∈ T_M × T_A | λ_M(t_M) = λ_A(t_A)\}$ - $α_⊗$ 和 $β_⊗$ 定义为 $•(t_M, t_A) = (•t_M, •t_A)$ 和 $(t_M, t_A)• = (t_M •, t_A•)$ - $λ_⊗$ 是 $π_M$ 在 $T_⊗$ 上的限制 - $Acc_⊗ = \{U ⊆ T_⊗ | π_A(U) ∈ Acc\}$ 我们有等式 $L(M ⊗ A) = Path_ω(M) ∩ λ_M^{-1}(L(A))$。为了确定 $M$ 是否以正概率满足 $A$，即 $µ_M(L(M ⊗ A)) > 0$，我们将概率满足问题简化为检查是否存在 $(s, q) ∈ S_0 × Q_0$ 使得 $µ_M(L(M ⊗ A[s, q])) > 0$。 为了方便，我们记 $L(s, q) = L(M ⊗ A[s, q])$，并定义映射 $V : S × Q → [0, +∞[$ 为 $V (s, q) = µ_M[s](L(s, q))$。 根据 $L(s, q) = \bigcup_{(t_M,t_A)∈(s,q)•} t_M · L(t_M •, t_A •)$，我们可以得出 $V (s, q) > 0$ 当且仅当存在从 $(s, q)$ 可达的 $(s′, q′)$ 使得 $V (s′, q′) > 0$。 由此，我们引入以下关于强连通分量（SCC）的定义： - **空SCC**：若 $C ⊆ V^{-1}(\{0\})$，则称 SCC $C$ 为空。 - **持久SCC**：若 $C$ 是所有非空SCC中最大的，则称其为持久SCC。 - **瞬态SCC**：其他情况的SCC称为瞬态SCC。 概率验证问题最终归结为检查是否存在可达的非空SCC，即可达的持久SCC。 ##### 概率满足 局部正SCC在概率验证中起着关键作用。我们通过完整性和接受性这两个性质来刻画局部正SCC。 当 $A$ 在每个SCC上是无歧义的，或者具有向上封闭的接受条件时，对于 $M ⊗ A$ 中的任何SCC $C$，$C$ 是局部正的当且仅当 $C$ 是完整的且被接受。 - **完整性**：SCC $C$ 是完整的，当且仅当对于所有 $s ∈ π_M(C)$，有 $Path^*(M, s) = \bigcup_{q∈Q | (s,q)∈C} Trace^*((M ⊗ A)|_C, (s, q))$。 - **接受性**：SCC $C$ 被接受，当且仅当 $(•C ∩ C•) ∈ Acc_⊗$。 以下是一些相关的引理和定理： - **引理4.13**：若 $M ⊗ A$ 在 $C$ 上是确定性的，则 $C$ 是完整的当且仅当对于所有 $(s, q) ∈ C$ 和 $t_M ∈ s•$，有 $| π_M^{-1}(t_M) ∩ (s, q)• ∩ •C | = 1$。 - **引理4.14**：若 $M ⊗ A$ 在 $C$ 上是无歧义的且分离的，则 $C$ 是完整的当且仅当对于所有 $(s, q) ∈ C$，$SCC(s)