我得到了上述原子命题系统 {a,b,c}。
然后我的意思是说某些 LTL 公式是否成立(例如 ♢ðc)。
我理解 LTL 公式的含义(最终 c 永远成立)，但我不知道如何阅读图表并将其与 LTL 联系起来。
我认为它就像一个流程图，我们从左上角 /{a} 开始，可以经历不同的状态。但是每个除以 a 意味着什么？
最佳答案
看起来像 FSM/transduser 而不是 Kripke 结构。输入/输出或更一般的前置条件/后置条件是 FSM 及其同类的常见表示法。前置条件/后置条件(a and b and ...) / (x and y and...) 。所以a在该州q1 。在接下来的状态中要么仅 b在第四季度或 b and c或q3。当然可能是or而不是and前提条件，否则系统可能会死机..
关于logic - 你如何阅读一组原子命题？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/44214297/