一句话：提出基于自动机的 CTL 成员判定准则，为判断 LTL 公式是否可由 CTL 定义提供条件。
CTL 在形式验证中广泛应用，但与 LTL 不同，其与字自动机和树自动机的联系尚未被充分理解。LTL 与 CTL 之间的长期联系也仍缺失：两者共同片段是否可判定未知，且判断一个 LTL 公式能否用 CTL 定义时，现有必要条件和充分条件都非常有限。本文以自动机为工具研究 CTL 成员性问题，提出基于自动机的判定准则，用于刻画公式何时属于 CTL 或可由 CTL 定义，从而为理解 CTL、LTL 及其共同片段提供新的理论视角。摘要未报告具体实验结果，论文贡献属于时序逻辑与自动机理论方向的理论准则与刻画。
Computation Tree Logic (CTL) is widely used in formal verification, however, unlike linear temporal logic (LTL), its connection to automata over words and trees is not yet fully understood. Moreover, the long sought connection between LTL and CTL is still missing; It is not known whether their common fragment is decidable, and there are very limited necessary conditions and sufficient conditions for checking whether an LTL formula is definable in CTL.
DOI 原文 ·
@inproceedings{paperbot4386,
title = {Automaton-Based Criteria for Membership in CTL},
author = {Udi Boker and Yariv Shaulian},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209143}
}