直觉主义计算树逻辑中的安全性和活性  

Safety and Liveness in Intuitionistic Computing Tree Logic

作　　者：鲍秋霜 张晋津[2] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016 [2]南京审计学院计算机科学与技术系,南京211815

出　　处：《计算机科学与探索》2016年第2期163-172,共10页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金Nos.11426136;60973045;江苏省高校自然科学基金No.13KJB520012~~

摘　　要：将Patrick Maier关于直觉主义线性时序逻辑的研究扩展到计算树逻辑中,基于完全树和非完全树构成的集合提出了一种直觉主义解释的计算树逻辑,并在此逻辑框架中研究了安全性和活性及其相关性质。比较了经典计算树逻辑与直觉主义计算树逻辑的表达能力,探究了直觉主义计算树逻辑中安全性和活性在并、交等操作下的封闭性以及与经典计算树逻辑中安全性和活性的关系,并为直觉主义计算树逻辑公式建立了分解定理。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.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]