Extended Full Computation-Tree Logic with Sequence Modal Operator: Representing Hierarchical Tree Structures
Extended Full Computation-Tree Logic with Sequence Modal Operator: Representing Hierarchical Tree Structures
复制标题
使用序列模态运算符扩展完整计算树逻辑：表示分层树结构
DOI：
10.1007/978-3-642-10439-8_49
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
K. Kaneiwa
中科院分区：
文献类型：
--
作者：
N. Kamide;K. Kaneiwa
扩展的完整计算树逻辑 CTLS* 是作为带有序列模态运算符的 Kripke 语义引入的。该逻辑可以适当地表示分层树结构，其中 CTLS* 中的序列模态运算符应用于树结构。证明了CTLS*到CTL*的嵌入定理。 CTLS* 的有效性、可满足性和模型检查问题被证明是可判定的。使用 CTLS* 公式给出了生物分类学的说明性示例。
An extended full computation-tree logic, CTLS*, is introduced as a Kripke semantics with a sequence modal operator. This logic can appropriately represent hierarchical tree structures where sequence modal operators in CTLS*are applied to tree structures. An embedding theorem of CTLS*into CTL*is proved. The validity, satisfiability and model-checking problems of CTLS*are shown to be decidable. An illustrative example of biological taxonomy is presented using CTLS*formulas.