引用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

AFAIK，

单调非递减序列.

线性时态逻辑有一个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属性的验证，但它可能是其他公式的问题)

通配符索引.

如果我理解正确的话，你想表达一个属性。--在每一种状态中--从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 ...")
    )
}

我相信你的问题的答案是no。但是，我建议您为C预处理器使用宏，以简化属性的编码，避免重复编写相同的内容。

注：

让我们以curr_int和next_int 0-1整数变量s.t为例。next_int等于下一个状态下的curr_int值(即curr_int是next_int__的前一个值)，以及curr布尔变量s.t。curr是true当且仅当curr_int等于1。

然后，根据LTL语义，X curr是true当且仅当curr_int true在下一个(当前)状态下等于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)

这是我们为给定状态的curr_int <= next_int的最后的LTL可编码版本，当两者都是0-1整数变量时.

Answer 2

在普罗美拉没有这样的符号。然而，任何过去时间LTL公式都可以转换为未来时间LTL (可能更麻烦)。

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

也可以检查LTL规范模式库的过去。

见CS堆栈中的讨论

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