以下の制約を線形時相論理で表現したいと思います。
A が発生した場合、B はその直前に発生する必要があります。
「BR !A」(!A は B が真になるまで真のままであり、B は真にならない可能性がある) を試しましたが、B が発生した後に A が発生する場合と発生しない場合があるため、正しくありません。
ロジックの専門家がこの問題について私を助けてくれますか? どうもありがとうございました！
2 に答える
2
X が次のように読み取られる場合、つまり Xp は次の時間ステップを意味し、p が該当する場合、Xp → q が探しているものになります。
またはあなたの手紙で: XA → B
(X は N または円に置き換えられることがありますが、LTL には常に存在します。)
于 2012-08-03T10:01:25.767 に答える
0
これには PT-LTL を使用できます。その過去の時間LTL。式は A -> XB になります。ここで、X は以前を意味します。
PTLTL モニターの実装に JavaMOP を使用できます。
于 2014-05-03T02:28:08.823 に答える