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

Question

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

Until

AUB: true if there exists i such that:

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 is true at time i

for times between 0 and i-1, formula A is true

still using the formalization of "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

Answer 1

强到

它的正式定义是：

M, s_k ⊨ ϕ U ψ

<->

∃ j ∈ N .

(j ≥ k) ∧

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

(M, s_j ⊨ ψ) ∧

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

where

M is the Kripke Structure

R_t is the transition relation

解释：

条件(1)-(2)强制执行状态序列（s_k，s_k+1, ..., s_j, ...) 是过渡系统的有效执行路径，ltl公式可以求值
条件(3)强制ψ保持在s_j.
条件(4)强制ϕ保持任何状态s_i 位于从 s_k （包括） 到 s_{j[=144 的路径上=] (排除).}

由于false前提的蕴涵总是true，逻辑蕴涵内部条件(4) 对于任何位于 [k, j) 范围之外的 i 来说， 都满足 。每当 j 被选为等于 k 时，如您的问题，范围 [k, j) = [k, k) 为空，并且 i 的任何选择都在所述区间之外。在这种情况下，不管 M, s ⊨ ϕ 对于某些 s 是否成立 （或不成立），条件 (4)对于 i 的任何选择都可以满足，并且它不再对执行路径施加任何约束（s_k，s_k+1, ..., s_j, ...)。换句话说，当 j = k 条件 (4) 不再对状态 s[= 上的属性 ϕ U ψ 的验证提供任何有意义的贡献117=]k.

弱到

weak until，特此用ϕ W ψ表示，与strong until的区别在于 weak until 也满足任意执行路径s.t。 G (ϕ ∧ ¬ψ)，而 strong until 迫使 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 中成立，ψ 在 [=87 中成立=]s_2 这是它的直接且唯一的后继者。所以属性 p1 在 s_1.
在状态s_2中属性ψ是true，所以p1 再次满足。

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

Using (U)ntil operator in SPIN ltl formula

model-checking

spin

promela