2

我试图了解如何在 ltl 公式中正确使用直到运算符。我发现这个定义（如下）很清楚：

直到_

A U B：如果存在 i 则为真：

  • B 在 [s i , s i+1 , s i+2 , ... ]中为真

  • 对于所有满足 0 ≤ j < i 的 j，公式 A 在 [s j , s j+1 , 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))}

根据我给出的 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
4

1 回答 1

1

强大直到

它的正式定义是：

M, s k ⊨ φ U ψ

<->

∃ j ∈ N 。

  1. (j ≥ k) ∧

  2. ∀ i ∈ N 。((k ≤ i < j) ⇒ (<s i , s i+1 > ∈ R t )) ∧</p>

  3. (M, s j ⊨ ψ) ∧</p>

  4. ∀ i ∈ N 。((k ≤ i < j) ⇒ (M, s 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)内的逻辑蕴涵对于任何位于范围之外的事物都可以轻松满足。Whenever is picked to be equal to , as in your question, the range is empty and any choice of lies outside said interval. 在这种情况下，无论对于 some事实是否成立，条件(4)对 的任何选择都会得到满足，并且不再对执行路径施加任何约束 (s k , s k+1 , ... , s ji[k, j)jk[k, j) = [k, k)iM, s ⊨ ϕsi, ...)。换句话说，当j = k条件(4)不再ϕ U ψ对状态sk的属性验证提供任何有意义的贡献时。

弱到

弱直到（在此用 表示ϕ W ψ）和强直到之间的区别在于，弱直到也满足任何执行路径 st 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再次满足。
于 2017-08-17T10:20:55.853 回答