Premium
Conceptual modeling in full computation‐tree logic with sequence modal operator
Author(s) -
Kaneiwa Ken,
Kamide Norihiro
Publication year - 2011
Publication title -
international journal of intelligent systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 1.291
H-Index - 87
eISSN - 1098-111X
pISSN - 0884-8173
DOI - 10.1002/int.20486
Subject(s) - computation tree logic , decidability , modal logic , modal operator , kripke structure , computer science , sequence (biology) , operator (biology) , algorithm , theoretical computer science , satisfiability , modal μ calculus , modal , tree (set theory) , computation , kripke semantics , multimodal logic , model checking , mathematics , normal modal logic , description logic , combinatorics , biochemistry , chemistry , repressor , biology , transcription factor , polymer chemistry , gene , genetics
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. © 2011 Wiley Periodicals, Inc.