參考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