logic - 線形時相論理制約

Question

以下の制約を線形時相論理で表現したいと思います。

A が発生した場合、B はその直前に発生する必要があります。

「BR !A」(!A は B が真になるまで真のままであり、B は真にならない可能性がある) を試しましたが、B が発生した後に A が発生する場合と発生しない場合があるため、正しくありません。

ロジックの専門家がこの問題について私を助けてくれますか? どうもありがとうございました！

Answer 1

X が次のように読み取られる場合、つまり Xp は次の時間ステップを意味し、p が該当する場合、Xp → q が探しているものになります。

またはあなたの手紙で: XA → B

(X は N または円に置き換えられることがありますが、LTL には常に存在します。)

Answer 2

これには PT-LTL を使用できます。その過去の時間LTL。式は A -> XB になります。ここで、X は以前を意味します。

PTLTL モニターの実装に JavaMOP を使用できます。