用LTL、CTL或TLA对我的模型进行建模（详细描述见内部）？

Question

我正在撰写我的硕士论文，需要在时间逻辑中说明和验证我的方法。

在我的情况下，哪种时间逻辑最好使用？我真的希望能得到关于我的方法和如何继续的反馈。

我的模型由参与者组成，将同时执行。对于每个参与者，可以注册规则。它们看起来像这样：

conditions -> action

例如。

received(a, c) ^ received(b,c) -> allowed(c,d) 

这意味着c必须收到来自b和c的消息，才能发送消息给d。

在参与者发送或接收消息之前，我的原型会检查参与者是否被允许执行该操作。到目前为止，我想验证算法是否执行以下操作：

1. 如果不存在符合条件的规则：禁止该操作 2. 如果存在符合条件的规则，但它禁止该操作：禁止该操作 3. 如果存在符合条件的规则，它允许该操作，并且不存在其他符合条件的规则禁止该操作：允许该操作

- nanoquack

Answer 1

看起来您想要找出规范的某些属性是否为不变量。也就是说，在程序执行期间，这些属性始终为真。

不变量的概念可以用所有时序逻辑形式表达。然而，我会使用 TLA+，因为它有一个模型检查器、一个证明系统、一个活跃的社区，以及一些编写规范的优秀书籍。

但是...请注意，时序逻辑不是易于掌握的技能，您需要花费一些时间仔细阅读和思考。

- marcmagransdeabril

Answer 2

这三种逻辑存在误解。TLA+和LTL中的时间逻辑是线性的。TLA+包括集合论，其公理基于Zermelo-Fraenkel集合论。TLA+在语法上强制实现抽搐不变性（以确保细化是实用的）。LTL是命题逻辑。

CTL与LTL截然不同，因为CTL是一种分支时间逻辑，而LTL是一种线性时间逻辑。单个序列是线性时间公式的模型。相反，树是分支时间公式的模型。序列代表单个执行，而树代表许多从某个状态开始的执行。

路径量词可以在CTL中使用，但在LTL中不存在。LTL和CTL有一个共同的子集，但它们是不可比较的（即某些属性仅可在LTL中表示，而其他属性仅可在CTL中表示）。CTL*是它们的公共超集。

对于您所勾画的应用程序，线性时间语义似乎更加合适。我建议使用TLA+，因为它提供了一种描述系统的良好规范，并且在时间上足够表达，您可能不需要LTL（反之亦然：如果您无法使用TLA+中的“口吃不变公式”指定系统，则更有可能需要修订系统，而不是需要完整的LTL表达能力）。 TLA+书籍是一个非常易懂的入门介绍。

- 0 _