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

我试图了解如何在 ltl 公式中正确使用 Until 运算符。我发现this定义（如下）要清楚：

Until

AUB：如果存在 i 则为真：

• B is true in [s_i, s_i+1, s_i+2, … ]

• for all j such that 0 ≤ j < i, formula A is true in [s_j, s_j+1, s_j+2, … ]

meaning:

• B 在时间 i 为真

• 对于 0 到 i-1 之间的时间，公式 A 成立

仍然使用“true at time 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))}

根据我给出的until运算符的定义，我不明白上面的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

强直到

Its 正式定义 is:

M, s_k ⊨ ϕ U ψ

∃ j ∈ N 。

1. (j≥k)∧

2. ∀ i ∈ N . ((k ≤ i < j) ⇒ (<s_i, s_i+1> ∈ R_t)) ∧

3. (M, s_j ⊨ ψ) ∧

4. ∀ i ∈ N . ((k ≤ i < j) ⇒ (M, s_i ⊨ ϕ))

where

• M 是克里普克结构

• R_t is the transition relation

解释：

• Conditions (1)-(2) enforce the sequence of states (s_k, s_k+1, ..., s_j, ...) to be a valid execution path of the transition system over which the ltl formula can be evaluated.

• Condition (3) forces ψ to hold in s_j.

• Condition (4) forces ϕ to hold in any state s_i that lies along the path from s_k (included) up to s_j (excluded).

Since an implication with a false premise is always true, the logical implication inside condition (4) is trivially satisfied for any i that lies outside of the range [k, j). Whenever j is picked to be equal to k, as in your question, the range [k, j) = [k, k) is empty and any choice of i lies outside said interval. In this case, regardless of the fact M, s ⊨ ϕ holds (or not) for some s, condition (4) is trivially satisfied for any choice of i and it no longer imposes any constraint over the execution path (s_k, s_k+1, ..., s_j, ...). In other words, when j = k condition (4) no longer provides any meaningful contribution to the verification of property ϕ U ψ over the state s_k.

弱直到

之间的区别弱直到，特此表示为ϕ W ψ, and 强直到就是它弱直到也满足任何执行路径 s.t.G (ϕ ∧ ¬ψ)， 然而强直到强迫F ψ.

实例分析

该物业p0

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

需要p1

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

保持系统的每一个状态。我会崩溃p1为了清楚起见，分为两个部分，并定义ϕ平等state == Reverse and ψ平等state != Reverse (note: ϕ <-> !ψ).

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

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

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

• 处于状态s_0该财产ψ成立，因此p1也适用于j equal 0.
• 处于状态s_1该财产ψ is false。然而，我们有这样的ϕ坚持s_1 and ψ坚持s_2这是它的直接且唯一的继承者。所以财产p1坚持s_1.
• 处于状态s_2该财产ψ is true, so p1又是微不足道的满足了。