Conceptual modeling in full computation-tree logic with sequence modal operator

In this paper, we propose a method for modeling concepts in full computation-tree logic with sequence modal operators. 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 in cases where sequence modal operators in CTLS∗ are applied to tree structures. We prove a theorem for embedding CTLS∗ into CTL∗ . 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.

• Type: Journal
• Year: 2011
• Where: IJIS
• Authors: Ken Kaneiwa, Norihiro Kamide
• Keywords: Biological Taxonomy, Computation Tree Logic, IJIS 2011, Kripke Semantics