时态逻辑描述能力比较研究  

The Comparisons of Expressive Power of Temporal Logics

作　　者：黎升洪[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机工程与科学学院

出　　处：《计算机工程与应用》2006年第22期75-77,共3页Computer Engineering and Applications

基　　金：国家自然科学基金资助项目(编号:60373072);江西省教育厅科技项目(赣教科技便函字[2002]01号)

摘　　要：时态逻辑在软件确认和模型检查中有广泛的应用。时态逻辑的不同变体有不同描述能力。正确理解时态逻辑的描述能力有助于书写系统特性的正确时态逻辑公式特性。论文从语法、语义域定义和语法到语义域映射三个方面对不同时态逻辑加以描述,对时态逻辑描述能力进行了比较。Temporal logics are widely used in software verification and model checking.Understanding temporal logics expressive powers is very helpful for writing corrective temporal formula that are based on systems properties,The variance of temporal logics are depicted in syntax,semantic domain and the mapping between syntax and semantic domain and their expressive powers are compared.

关 键 词：时态逻辑 模型检查 CTL^＊ LTL 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]