<>P -> (!P U R)的解释是什么？
提问于 2019-04-19 05:43:27
<>P -> (!P U R)的解释是什么？这似乎是矛盾的，因为在未来，P是预期的，在R.模型检查工具通过BDD和BMC技术之前检查P的缺失。
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-04-24 11:51:45
我看不出有什么矛盾。
该属性由任何Buchi自动机s.t实现。
- P总是假的，因为蕴涵的前提是假的，或者
- 在将来的某个时刻，P变为真，但在一段时间内，P可能是假的，直到R变为真为止。
即
在自然语言中，人们可以这样表达这个属性：“如果迟早P变成真的，那么'event‘R必须首先被触发”。
例如，您可以想象P是“发送应答消息”，R是“接收到的输入消息”，而整个属性是“从未发送过未经请求的应答消息”。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/55762828
复制相关文章
腾讯云开发者
