LTL,CTL或TLA用于我的模型建模(内部详细说明)？

Question

我目前正在撰写我的硕士论文,并面临着在时间逻辑中指定和验证我的方法.

在我的情况下哪种时态逻辑最好用？我真的希望对我的方法以及如何继续进行一些反馈

我的模型由参与者组成,这些参与者将同时执行.对于每个参与者,可以注册规则.他们看起来像这样:

conditions -> action

例如

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

这意味着c必须接收来自b的消息和来自c的消息才能被允许向d发送消息.

在其中一个参与者发送或接收消息之前,我的原型检查是否允许参与者执行该操作.到目前为止,我想验证该算法是否执行以下操作:

Answer 1

看起来您想要了解规范的某些属性是否为不变量.也就是说,如果在执行程序期间属性始终为真.

不变量的概念可以用所有时态逻辑形式表达.但是,我会使用TLA +,因为有一个模型检查器,一个可用的证明系统,一个活跃的社区,以及一些用于编写规范的优秀书籍.

但是......请注意,Temporal Logic不是小菜一碟,你需要花一些时间阅读和仔细思考.

Answer 2

比较这三种逻辑存在误解。TLA+ 和 LTL 中的时间逻辑都是线性的。TLA+包含集合论，TLA+的公理基于Zermelo-Fraenkel集合论。TLA+ 在语法上强制执行口吃不变性（以确保细化实用）。LTL 是一种命题逻辑。

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

CTL 中提供路径量化，而 LTL 中不提供路径量化。LTL 和 CTL 有一个共同的子集，但它们没有可比性（= 某些属性只能用 LTL 表达，其他属性只能用 CTL 表达）。CTL* 是它们的共同超集。

对于您所描绘的应用程序，线性时间语义似乎更合适。我建议使用 TLA+，因为它为描述系统提供了良好的规则，并且在时间上具有足够的表达能力，您可能不需要 LTL（反过来说：如果您无法使用以下中的口吃不变公式指定系统） TLA+，那么更有可能的是系统需要修改，而不是需要 LTL 的完整表达能力）。

TLA + 书是一本非常易读的介绍性书籍。