1

我开始使用 Promela，但在表达一些 LTL 公式时遇到了麻烦。

一个例子是sequence我想断言的以下值是单调递增的。直观地说，我想在下一个状态中写下， sequence >= its previous value，但是查看文档，我看不到表达这一点的方法。有没有表达这种公式的方法？

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 看起来真的很棒:)

4

2 回答 2

1

Promela 中没有这样的符号。然而，任何过去时间 LTL公式都可以转换为未来时间 LTL（可能更麻烦）。

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

还要检查过去的LTL 规范模式存储库。

请参阅 CS stackexhange 中的讨论

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

于 2017-09-15T21:32:15.693 回答
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 ...
}

否则，与相关的不变性质可能会导致在某些状态的相应自动机上被破坏。（注意：这实际上不会妨碍您感兴趣的特定 LTL 属性的验证，但它可能是其他公式的问题）prev_valuecur_values_i

通配符索引。

如果我理解正确，您想表达一个属性 st --在每个状态中 -- 只需要从0up toindex-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 预处理器的宏来简化属性的编码并避免一遍又一遍地编写相同的内容。

笔记：

让我们假设0-1 整数变量 st在下一个状态curr_int中等于 的值（也就是 的前一个值），而布尔变量 st是当且仅当等于 时。next_int next_intcurr_intcurr_intnext_intcurrcurrtruecurr_int1

然后，根据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)

Thich 是给定 state的最终LTL 可编码版本，当两者都是0-1 Integer variables时。curr_int <= next_ints_i

于 2017-09-15T18:01:49.210 回答