我目前正在写我的硕士论文，并面临着在时间逻辑中指定和验证我的方法。
在我的情况下，哪种时间逻辑最适合使用？我真的很想得到一些关于我的方法以及如何进行的反馈
我的模型由参与者组成，这些参与者将同时执行。对于每个参与者，可以注册规则。它们看起来像这样：
conditions -> action
例如
received(a, c) ^ received(b,c) -> allowed(c,d)
这意味着 c 必须收到来自 b 的消息和来自 c 的消息，才能被允许向 d 发送消息。
在其中一个参与者发送或接收消息之前，我的原型会检查参与者是否被允许执行该操作。到目前为止，我想验证该算法是否执行以下操作：
如果不存在其条件成立的规则：禁止该操作
如果存在条件成立且禁止该操作的规则：禁止该操作
如果存在条件成立的规则，则它允许该操作，并且不存在其条件成立且禁止该操作的其他规则：允许该操作
看起来您想查明您的规范的某些属性是否是不变量。也就是说，如果在程序执行期间属性始终为真。
不变量的概念可以用所有的时间逻辑形式来表达。但是，我会使用TLA+，因为有一个模型检查器、一个可用的证明系统、一个活跃的社区以及几本用于编写规范的优秀书籍。
但是......请注意，时间逻辑不是小菜一碟，您需要花一些时间仔细阅读和思考。
比较这三种逻辑存在误解。TLA+ 和 LTL 中的时间逻辑都是线性的。TLA+包括集合论，TLA+的公理是基于Zermelo-Fraenkel集合论。TLA+ 在语法上强制执行口吃不变性（以确保细化是实用的）。LTL 是一种命题逻辑。
CTL 与 LTL 截然不同，因为 CTL 是分支时间逻辑，而 LTL 是线性时间逻辑。单个序列是线性时间公式的模型。相反，树是分支时间公式的模型。一个序列代表一个单一的执行，而一棵树代表许多从某个状态开始的执行。
路径量化在 CTL 中可用，而在 LTL 中不存在。LTL 和 CTL 有一个共同的子集，但它们是无法比较的（= 某些属性只能在 LTL 中表达，而其他属性只能在 CTL 中表达）。CTL* 是它们的共同超集。
对于您绘制的应用程序，线性时间语义似乎更合适。我建议使用 TLA+，因为它为描述系统提供了一个很好的规则，并且在时间上足够表达你可能不需要 LTL（反过来：如果你不能用 stutter-invariant 公式指定系统TLA+，那么系统更可能需要修订，而不是需要 LTL 的全部表达能力）。
TLA+ 书是一本非常易读的介绍。