摘要
时态逻辑在软件确认和模型检查中有广泛的应用。时态逻辑的不同变体有不同描述能力。正确理解时态逻辑的描述能力有助于书写系统特性的正确时态逻辑公式特性。论文从语法、语义域定义和语法到语义域映射三个方面对不同时态逻辑加以描述,对时态逻辑描述能力进行了比较。
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.
出处
《计算机工程与应用》
CSCD
北大核心
2006年第22期75-77,共3页
Computer Engineering and Applications
基金
国家自然科学基金资助项目(编号:60373072)
江西省教育厅科技项目(赣教科技便函字[2002]01号)
