Amparore Elvio Gilberto, Donatelli Susanna, Gallà Francesco
Dipartimento di Informatica, Università degli Studi di Torino, Torino, Italy.
PeerJ Comput Sci. 2022 Feb 24;8:e823. doi: 10.7717/peerj-cs.823. eCollection 2022.
Model-checking of temporal logic formulae is a widely used technique for the verification of systems. CTL is a temporal logic that allows to consider an intermix of both branching behaviours (like in CTL) and linear behaviours (LTL), overcoming the limitations of LTL (that cannot express "possibility") and CTL (cannot fully express fairness). Nevertheless CTL model-checkers are uncommon. This paper presents (1) the algorithms for a approach for CTL , and (2) their implementation in the open-source tool starMC, a CTL model checker for systems specified as Petri nets. Testing has been conducted on thousands of formulas over almost a hundred models. The experiments show that the fully symbolic automata-based approach of starMC can compute the set of states that satisfy a CTL formula for very large models (non trivial formulas for state spaces larger than 10 states are evaluated in less than a minute).
时态逻辑公式的模型检查是一种广泛用于系统验证的技术。CTL 是一种时态逻辑，它允许同时考虑分支行为（如在 CTL 中）和线性行为（LTL）的混合，克服了 LTL（无法表达“可能性”）和 CTL（无法完全表达公平性）的局限性。然而，CTL 模型检查器并不常见。本文介绍了（1）一种用于 CTL 的方法的算法，以及（2）它们在开源工具 starMC 中的实现，starMC 是一个用于将系统指定为 Petri 网的 CTL 模型检查器。已经对近一百个模型上的数千个公式进行了测试。实验表明，starMC 基于完全符号自动机的方法可以为非常大的模型计算满足 CTL 公式的状态集（对于状态空间大于 10 个状态的非平凡公式，评估时间不到一分钟）。
