logic - 你如何阅读一组原子命题？

Question

我得到了上述原子命题 {a,b,c} 的系统。

然后我的意思是说某些 LTL 公式是否成立（例如♢☐c）。

我了解 LTL 公式的含义（最终 c 永远成立），但我不知道如何阅读图表并将其与 LTL 相关联。

我假设它就像一个流程图，我们从左上角开始，/{a}可以通过不同的状态。但是每一个除以 是什么意思a？

Answer 1

看起来像 FSM/transduser 而不是 Kripke 结构。输入/输出或更一般的前置条件/​​后置条件是 FSM 及其亲属的常见表示法。前置条件/​​后置条件(a and b and ...) / (x and y and...)。所以a处于状态q1。在下一个状态中，仅b在 q4b and c或 q3 中。当然可能or不是and前提条件，否则系统可能会停止..