参考Promela LTL声明中的以前状态

Question

我开始使用Promela，并且在表达一些LTL公式时遇到问题。

一个示例是以下sequence值，我想断言是单调增加。直觉上我想在下一个状态中写，顺序是> =其前值，但是通过查看文档，我没有看到一种方式来表达这一点。有没有一种方法来表达这种类型的公式？

byte sequence = 0; 
ltl p0 { [] sequence >= prev(sequence) } 
... processes that manipulate sequence ... 

假设它可能表达上述的sequence单调增加的财产，我想知道如果有一个通配符数组索引语法。类似于上面的例子，我直观地想引用所有以前的索引条目。

byte values[N]; 
byte index = 0; 
ltl p1 { values[0..index-1] are monotonically increasing } 
... processes ... 

非常感谢您的帮助。 PROMELA似乎真的很棒:)

Answer 1

据我所知，

单调非减序列。

线性时序逻辑具有X操作者，允许一个表达是指保持在下一状态一个布尔条件，而不是在先前状态的性质。

然而，可以不直接与一个LTL式中的下一个状态的比较当前状态的整数值，因为X评估为布尔值。

从理论上讲，有什么可以做的是位爆破它，例如编码的<=运营商在整数布尔属性通过一些巧妙地利用了模运算的手段或位运算（它不应该是无符号的变量太用力）和相应的布尔值的位对位比较（见最后注）。

然而，从建模的角度来看，最简单的方法是使用prev_value变量丰富您的模型，并简单地检查在每个状态下属性prev_value <= cur_value是否成立。请注意，在这种情况下，您应该使用命令d_step将两个值分配组合在一起，以便它们在单个状态下合并，不存在中间转换，例如。

... 
byte prev_value; 
byte cur_value; 
... 
d_step { 
    prev_value = cur_value; 
    cur_value = ... non-blocking function ... 
} 

否则，关于prev_value到cur_value的不变性可能导致在相应的自动机被打破一些状态s_i。（注：这实际上不会妨碍特定LTL财产你有兴趣的验证，但它可以与其他公式的问题）

通配符索引编制。

如果我理解正确，你想表达一个属性s.t. - 在每种状态下，只有从0到index-1的存储单元需要为单调不递减，其中index是一个可以更改值（任意？）的变量。

这种属性的结构应该是：

ltl p1 { 
    [] (
     ((1 <= index) -> "... values[0] is monotonically non-decreasing ...") && 
     ((2 <= index) -> "... values[1] is monotonically non-decreasing ...") && 
     ((3 <= index) -> "... values[2] is monotonically non-decreasing ...") && 
     ... 
     ((N <= index) -> "... values[N-1] is monotonically non-decreasing ...") 
    ) 
} 

我相信回答你的问题是没有。不过，我建议您使用宏作为C预处理器以简化属性的编码并避免一遍又一遍地写同样的东西。

---

注：

让我们curr_int和next_int0-1整数变量S.T. next_int等于在下一个状态（又名curr_int是next_int的前一个值）和curr布尔变量s.t.中的值curr_int。 curr是true当且仅当curr_int等于1。

然后，由LTL语义，X curr是true当且仅当curr_int（next_int）是在下一（电流）状态等于1。

考虑以下真值表国有s_i：

curr_int | next_int | curr_int <= next_int 

    0 |  0 |   1 
    0 |  1 |   1 
    1 |  0 |   0 
    1 |  1 |   1 

从上面的定义，我们可以把它改写为：

curr | X curr |   EXPR 

    false | false |   true 
    false | true |   true 
    true | false |   false 
    true | true |   true 

从真值表这是可以可见EXPR对应于

!curr v (X curr) 

可以更优雅改写为

curr -> (X curr) 

释是我们最后的LTL-encodeable版本的curr_int <= next_int对于给定的状态s_i，当两者都0-1整数变量。

Answer 2

Promela中没有这样的符号。然而，任何Past Time LTL公式都可以翻译成未来时间LTL（可能更加麻烦）。

不确定是否有一种简单的方法来比较不同状态下的变量值。

还检查LTL specification pattern repository过去。在CS stackexhange

见discusssion

https://cstheory.stackexchange.com/questions/29444/do-past-time-ltl-and-future-time-ltl-have-the-same-expressiveness