在SPIN公式中使用（U）ntil运算符公式

Question

我想了解如何在ltl公式中正确使用Until运算符。我发现this定义（见下文）是明确的：

ù NTIL

甲û B：如果存在真实我使得：

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

• 对于所有的j，使得0≤Ĵ< I，式A是真[秒_Ĵ，S _{J + 1}，S _{J + 2}， ...]

含义：

• B是在时间真我

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

Answer 1

STRONG UNTIL

其正式定义是：

M，S _ķ⊨φ Uψ

< - >

∃j∈N。

1. （j≥K）∧

2. ∀我∈N。（（K≤我< j）的⇒（<小号_我，S _{i + 1的}>∈R_吨））∧

3. （M，S _Ĵ⊨ψ）∧

4. ∀i∈N。 （（K≤我< j）的⇒（M，S _我⊨φ））

其中

• M是Kripke结构

• ř_吨是过渡关系

说明：

• 条件（1） - （2）执行状态（S _ķ，S _{K + 1}，...，S _Ĵ，的序列。 ..）作为转换系统的有效执行路径，通过该路径可以评估公式。

• 条件（3）力量ψ举行以s _Ĵ。

• 条件（4）力ϕ在持有任何状态s _我其从s _ķ（附带）沿着路径位于到s _Ĵ（除外） 。

由于与false前提的含义是总是true，内部条件的逻辑蕴涵（4）是平凡满意为位于范围[k, j)之外的任何i。每当j被挑选为等于k，如在你的问题中，范围[k, j) = [k, k)是空的，任何选择i位于所述区间之外。在这种情况下，不管事实M, s ⊨ ϕ保持（或不）一些s，条件（4）是用于i任何选择平凡满足，并且它不再施加任何约束在执行路径（S _ķ ，s _{k + 1}，...，s _j，...）。换句话说，当j = k条件（4）不再提供任何有意义的贡献来验证状态ϕ U ψ状态s _k。

---

弱UNTIL

之间弱直到，与ϕ W ψ特此表示的差，和强直到是弱直到也由任何执行路径S.T.满足G (ϕ ∧ ¬ψ)，而强至强制F ψ。

---

实例分析

酒店P0

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

需要P1

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

在EA持有ch和你系统的每个状态。我会分解P1两个组件的清晰度，并定义φ等于state == Reverse和ψ等于state != Reverse（注：ϕ <-> !ψ）。

假设，把事情简单化，你的系统是由以下三种状态包括：

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

为了P0持有，P1必须持有每个状态。

• 在状态S_0属性ψ成立，因此P1保持过多为j等于。
• 状态S_1财产ψ是false。但是，我们有φ持有S_1和ψ持有S_2这是它的直接的，也是唯一的继承人。所以财产p1保留在s_1。
• 状态S_2财产ψ是true，所以P1又是平凡满意。

---