关键词: 直觉主义, 计算树逻辑, 安全性, 活性, 分解定理

Abstract: This paper makes an extension from the intuitionistic linear time logic of Patrick Maier to computation tree logic, proposes an intuitionistic computation tree logic based on the set constructed by total and non-total tree, and considers safety and livenss in this intuitionistic computation tree logic. This paper also compares the expressive power between classical computation tree logic and intuitionistic computation tree logic, explores some properties of safety and liveness in intuitionistic computation tree logic under disjunction and conjunction, and discusses the relationship between intuitionistic computation tree logic and classical computation tree logic. Besides, this paper builds the decomposition theorem for formulas of intuitionistic computation tree logic.

Key words: intuitionistic, computation tree logic, safety, liveness, decomposition theorem