我目前正在撰写硕士论文，面临着在时间逻辑中指定和验证我的方法。
在我的情况下，哪种时序逻辑最适合使用？我真的很想得到一些关于我的方法以及如何继续的反馈
我的模型由参与者组成，这些参与者将同时执行。对于每个参与者，都可以注册规则。它们看起来像这样:
conditions -> action
例如
received(a, c) ^ received(b,c) -> allowed(c,d)
这意味着 c 必须已收到来自 b 的消息和来自 c 的消息才能被允许向 d 发送消息。
在参与者之一发送或接收消息之前，我的原型(prototype)会检查是否允许参与者执行该操作。到目前为止，我想验证该算法是否执行以下操作:
如果不存在条件成立的规则:禁止该操作
如果存在条件成立且禁止该操作的规则:禁止该操作
如果存在条件成立的规则，则允许该操作，并且不存在条件成立且禁止该操作的其他规则:允许该操作
最佳答案
您似乎想了解规范的某些属性是否是不变的。也就是说，如果在程序执行期间属性始终为 true。
不变量的概念可以用所有时序逻辑形式来表达。但是，我会使用 TLA+因为有一个模型检查器、一个可用的证明系统、一个活跃的社区以及一些用于编写规范的优秀书籍。
但是……请注意，时态逻辑并不是小菜一碟，您需要花一些时间仔细阅读和思考。
关于logic - LTL、CTL 或 TLA 用于我的模型建模(内部有详细说明)？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/22147090/