<>P -> (!P U R) 的解释是什么
What is the interpretation of <>P -> (!P U R)
<>P -> (!P U R) 的解释是什么？这似乎是矛盾的，因为在未来 P 是预期的并且检查 P 的缺席直到 R。
模型检查工具通过 BDD 和 BMC 技术传递它。
我看不出有什么矛盾。
属性 由任何 Buchi 自动机 s.t 变为真。
- P永远为假【因为蕴涵的前提为假】，或者
- 在未来的某个时刻 P 变为真，但在一段时间内 P 可能为假，直到 R 变为真。
即
在自然语言中，属性 可以表示为："If, by any chance, sooner or later P becomes true, then it must be the case that the 'event' R fired first".
例如，你可以想象 P 是 "sending answer message"，R 是 "received input message"，整个 属性 为 "no unsolicited answer message is ever sent".
<>P -> (!P U R) 的解释是什么？这似乎是矛盾的，因为在未来 P 是预期的并且检查 P 的缺席直到 R。 模型检查工具通过 BDD 和 BMC 技术传递它。
我看不出有什么矛盾。
属性 由任何 Buchi 自动机 s.t 变为真。
- P永远为假【因为蕴涵的前提为假】，或者
- 在未来的某个时刻 P 变为真，但在一段时间内 P 可能为假，直到 R 变为真。
即
在自然语言中，属性 可以表示为："If, by any chance, sooner or later P becomes true, then it must be the case that the 'event' R fired first".
例如，你可以想象 P 是 "sending answer message"，R 是 "received input message"，整个 属性 为 "no unsolicited answer message is ever sent".