在SPIN LTL公式中使用(U)ntil运算符 [英] Using (U)ntil operator in SPIN ltl formula

问题描述

我试图了解如何在ltl公式中正确使用直到"运算符.我发现此定义(如下)很清楚:

I am trying to understand how to correctly use the Until operator in an ltl formula. I found this definition (below) to be clear:

U ntil

A U B:如果存在以下条件，则为true:

AUB: true if there exists i such that:

• B在[s _i ，s _{i + 1} ，s _{i + 2} ，...中是正确的 ]

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

对于所有j，使得0≤j< i，公式A在[s _j ，s _{j + 1} ，s _{j + 2} ， …]

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

含义:

• B在时间i正确

• B is true at time i

对于0到i-1之间的时间，公式A为真

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

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

still using the formalization of "true at time i"

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

Sample code with example ltl formula:

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))}

基于我给出的直到运算符的定义，我不明白上面的ltl公式如何不会产生任何错误.在state != Reverse之前，state == Reverse是否需要一直为真?最初是state == Regular.

Based on the definition of the until operator that I gave, I don't understand how the above ltl formula is not producing any errors. Wouldn't state == Reverse need to be true for all time up until state != Reverse? Initially state == Regular.

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

Below is the SPIN output after running the test:

(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

推荐答案

强大直到

其正式定义是:

M，s _k ϕ Uψ

<->

∃j∈N.

1. (j≥k)∧

1. (j ≥ k) ∧

∀i∈N. ((k≤i< j)⇒(< s _i ，s _{i + 1} >∈R _t ))∧

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

(M，s _j ⊨ψ)∧

∀i∈N. ((k≤i< j)⇒(M，s _i ⊨ϕ))

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

其中

• M是克里普克结构

• M is the Kripke Structure

R _t 是过渡关系

说明:

• 条件(1)-(2)强制执行状态序列(s _k ，s _{k + 1} 、. ..，s _j ，...)作为过渡系统的有效执行路径，可以在该路径上评估 ltl 公式.

• 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.

条件(3)强制ψ保持在s _j 中.

Condition (3) forces ψ to hold in s_j.

条件(4)强制ϕ沿从s _k (包括)，直到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).

由于带有false前提的蕴涵始终为true，因此条件(4)内的逻辑蕴涵一般满足对于任何超出范围[k, j)的i.每当被拾取为等于，如在你的问题，该范围是空的和谎言任何选择所述外部间隔.在这种情况下，无论M, s ⊨ ϕ对于某些s持有(或不持有)的事实，对于i的任何选择，均满足条件(4)并且不再对执行路径(s _k ，s _{k + 1} ，...，s _j ，.. ).换句话说，当j = k条件(4)不再对状态s _k 的属性ϕ U ψ的验证提供任何有意义的贡献.

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.

弱直到

WEAK UNTIL

弱直到(在此用ϕ W ψ表示)和强直到之间的区别在于，弱直到也可以通过执行来满足路径G (ϕ ∧ ¬ψ)，而强直到强制F ψ.

The difference among weak until, hereby denoted with ϕ W ψ, and strong until is that weak until is also satisfied by any execution path s.t. G (ϕ ∧ ¬ψ), whereas strong until compels F ψ.

示例分析

属性 p0

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

需要 p1

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

保持系统的每个状态.为了清楚起见，我将 p1 分解为两个部分，并定义 ϕ 等于state == Reverse和ψ等于state != Reverse(注意:ϕ <-> !ψ).

to hold in each and every state of your system. I will break down p1 in two components for clarity, and define ϕ to be equal state == Reverse and ψ to be equal state != Reverse (note: ϕ <-> !ψ).

为简单起见，我们假设您的系统由以下三种状态组成:

Let's assume, to simplify things, that your system is comprised by the following three states:

• s_0 :常规状态，也恰好是初始状态
• s_1 :相反的状态
• s_2 :最终状态

• s_0: a regular state, which also happens to be the initial state
• s_1: a reverse state
• s_2: the final state

要保持 p0 ，必须为每个状态保持 p1 .

In order for p0 to hold, p1 must hold for each of these states.

• 在状态 s_0 中保持属性ψ，因此对于j等于 0 来说， p1 也成立.
• 状态为 s_1 ，属性ψ为false.但是， ϕ 保留在 s_1 中，而ψ保留在 s_2 中，这是其直接且唯一的，接班人.因此，属性 p1 保存在 s_1 中.
• 状态为 s_2 的属性ψ为true，因此再次满足了 p1 .

• in state s_0 the property ψ holds, therefore p1 holds too for j equal 0.
• in state s_1 the property ψ is false. However, we have that ϕ holds in s_1 and ψ holds in s_2 which is its immediate, and only, successor. So property p1 holds in s_1.
• in state s_2 the property ψ is true, so p1 is again trivially satisfied.

这篇关于在SPIN LTL公式中使用(U)ntil运算符的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！