logic - 线性时序逻辑约束

Question

我想用线性时间逻辑表达以下约束。

如果 A 发生，那么 B 必须直接发生在它之前。

我尝试了“BR！A”（！A 在 B 变为真之前一直为真；B 可能永远不会变为真），但它是不正确的，因为 A 可能会在 B 发生后发生，也可能不会发生。

任何逻辑专家可以帮助我解决这个问题吗？非常感谢！

Answer 1

好吧，如果 X 被读取为下一个，即 Xp 表示在下一个时间步，p 就是这种情况，那么 Xp → q 就是你要找的。

或者在你的信中：XA → B

（X 有时被替换为 N 或圆圈，但始终存在于 LTL 中。）

Answer 2

您可以为此使用 PT-LTL。它过去的时间零担。公式是 A -> XB，这里 X 表示之前的意思。

您可以使用 JavaMOP 来实现 PTLTL 监视器。