你如何阅读一组原子命题？答案

【问题标题】：How do you read a set of atomic propositions?你如何阅读一组原子命题？
【发布时间】：2017-05-27 07:40:31
【问题描述】：

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

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

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

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

【问题讨论】：

我认为我最困惑的部分是斜线是什么意思？肯定不是除以

标签： logic model-checking ctl

【解决方案1】：

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

【讨论】：