Branching vs. Linear Time: Final Showdown
Branching vs. Linear Time: Final Showdown
复制标题
DOI：
10.1007/3-540-45319-9_1
复制
发表时间：
2001-04
期刊：
影响因子：
--
通讯作者：
Moshe Y. Vardi
中科院分区：
文献类型：
--
作者：
Moshe Y. Vardi
对线性框架与分支时间框架相对优点的讨论可以追溯到 20 世纪 80 年代初。主导这一讨论的信念之一是“虽然在 LTL（线性时间逻辑）中指定更容易，但在 CTL（分支时间逻辑）中验证更容易”。事实上，CTL 的语法限制限制了它的表达能力，许多重要的行为（例如强公平性）无法在 CTL 中指定。另一方面，虽然 CTL 的模型检查可以在与规范大小呈线性关系的时间内完成，但所需的时间与 LTL 规范的大小呈指数关系。由于这些论点，并且由于历史原因，工业使用中占主导地位的时间规范语言是 CTL。在本文中，我们认为，尽管基于 CTL 的模型检查取得了巨大的成功，但 CTL 作为规范语言仍面临一些基本限制，所有这些都源于 CTL 是分支时间形式主义的事实：该语言不直观且难以使用，它不适合组合推理，并且从根本上与半形式验证不兼容。这些固有的限制严重阻碍了基于 CTL 的模型检查器的功能。相比之下，线性时间框架具有表现力和直观性，支持组合推理和半形式验证，并且适合结合枚举和符号搜索方法。虽然我们支持线性时间框架，但我们也认为 LTL 的表达能力不够，并讨论什么是“最终”时间规范语言。
The discussion of the relative merits of linear-versus branching-time frameworks goes back to early 1980s. One of the beliefs dominating this discussion has been that “while specifying is easier in LTL (linear-temporal logic), verification is easier for CTL (branching-temporal logic)”. Indeed, the restricted syntax of CTL limits its expressive power and many important behaviors (e.g., strong fairness) can not be specified in CTL. On the other hand, while model checking for CTL can be done in time that is linear in the size of the specification, it takes time that is exponential in the specification for LTL. Because of these arguments, and for historical reasons, the dominant temporal specification language in industrial use is CTL.In this paper we argue that in spite of the phenomenal success of CTL-based model checking, CTL suffers from several fundamental limitations as a specification language, all stemming from the fact that CTL is a branching-time formalism: the language is unintuitive and hard to use, it does not lend itself to compositional reasoning, and it is fundamentally incompatible with semi-formal verification. These inherent limitations severely impede the functionality of CTL-based model checkers. In contrast, the linear-time framework is expressive and intuitive, supports compositional reasoning and semi-formal verification, and is amenable to combining enumerative and symbolic search methods. While we argue in favor of the linear-time framework, we also we argue that LTL is not expressive enough, and discusswhat would be the “ultimate” temporal specification language.