在 SPIN ltl 公式中使用 (U)ntil 运算符

Question

我正在尝试了解如何在 ltl 公式中正确使用 till 运算符。我发现这个定义(如下(很清楚：

Until

AUB：如果存在，我就是这样：

• B 在 [s_i， s i_{+1， s i+2}， ...]

• 对于所有 j 使得 0 ≤ j <i，公式>j， s j₊₁， s_j+2， ... ]

意义：

• B 在时间 i 为真

• 对于介于 0 和 I-1 之间的时间，公式 A 为真

仍然使用"在时间 i 时为真"的形式化

带有示例 ltl 公式的示例代码：

mtype = {Regular, Reverse, Quit}
mtype state = Regular;
init {
do ::
if
::state == Regular -> state = Reverse
::state == Reverse -> state = Quit
::state == Quit -> break
fi
od
}
ltl p0 { [] ((state == Reverse) U (state != Reverse))}

根据我给出的 till 运算符的定义，我不明白上面的 ltl 公式如何不会产生任何错误。难道state == Reverse不需要一直如此，直到state != Reverse？最初state == Regular.

下面是运行测试后的 SPIN 输出：

(Spin Version 6.4.6 -- 2 December 2016)
+ Partial Order Reduction
Full statespace search for:
never claim             + (p0)
assertion violations    + (if within scope of claim)
acceptance   cycles     + (fairness disabled)
invalid end states  - (disabled by never claim)
State-vector 28 byte, depth reached 13, errors: 0
9 states, stored (11 visited)
2 states, matched
13 transitions (= visited+matched)
0 atomic steps
hash conflicts:         0 (resolved)
Stats on memory usage (in Megabytes):
0.000   equivalent memory usage for states (stored*(State-vector + overhead))
0.288   actual memory usage for states
128.000   memory used for hash table (-w24)
0.534   memory used for DFS stack (-m10000)
128.730   total actual memory usage

unreached in init
(0 of 12 states)
unreached in claim p0
_spin_nvr.tmp:14, state 20, "-end-"
(1 of 20 states)
pan: elapsed time 0 seconds

Answer 1

强至

其正式定义是：

M， s_k⊨ φ U ψ

<->

∃ j ∈ N .

1. (J ≥ k( ∧

2. ∀ 我∈ N .((k ≤ i <j(>i， s_i+1> ∈ R_t(( ∧

3. (M， s_j⊨ ψ( ∧

4. ∀ 我∈ N .((k ≤ i <j(>i ⊨ φ((

哪里

• M 是克里普克结构

• R_t是转移关系

解释：

• 条件(1(-(2( 强制将状态序列 (s_{k， s k+1}， ...， s_j， ...( 作为可以计算ltl公式的转换系统的有效执行路径。

• 条件(3(迫使ψ保持s_j。

• 条件(4( 迫使ϕ保持从s_k(包含(到 s_j(排除(的路径沿线的任何状态 s_i。

由于具有false前提的蕴涵总是true的，条件(4(内的逻辑蕴涵对于位于范围[k, j)之外的任何i都是微不足道的。每当选择j等于k时，就像您的问题一样，[k, j) = [k, k)的范围为空，任何i选择都在所述间隔之外。在这种情况下，无论M, s ⊨ ϕ对某些s成立(或不成立(的事实如何，条件(4(对于任何i选择都是微不足道的，并且它不再对执行路径施加任何约束(s_k，sk+1，...，s_j，...(。换句话说，当条件(4(不再对ϕ U ψ状态的财产验证提供任何有意义的贡献j = k时。

---

弱直到

弱直到(在此用ϕ W ψ表示(和强直到之间的区别是弱直到也由任何执行路径 s.t 满足。G (ϕ ∧ ¬ψ)，而强，直到迫使F ψ。

---

示例分析

属性p0

[] ((state == Reverse) U (state != Reverse))

需要P1

((state == Reverse) U (state != Reverse))

保持系统的每种状态。为了清楚起见，我将p1分解为两个组件，并将φ定义为相等state == Reverse，ψ定义为相等state != Reverse(注意：ϕ <-> !ψ(。

为了简化起见，让我们假设您的系统由以下三种状态组成：

• s_0：常规状态，也恰好是初始状态
• s_1：反向状态
• s_2：最终状态

为了使p0保持，p1必须针对这些状态中的每一个都成立。

• 在状态s_0中，ψ持有的属性，因此P1也成立j等于0。
• 在州s_1属性ψ是false。然而，我们有φ在s_1中成立，ψ在s_2中成立，这是它的直接和唯一的继任者。因此，属性p1在s_1中成立。
• 在状态s_2性质ψ是true，所以P1再次得到微不足道的满足。

---