摘要
时态逻辑是一种描述反应式(并发)系统中状态迁移序列的形式化方法,用于刻画并发系统所需验证的性质,是模型检测的基础.阐述了时态逻辑CTL 及其子逻辑CTL、LTL的语法及语义,然后分析运用时态逻辑描述并发系统性质,最后给出一个应用实例.
The temporal logic is a formal method for describing sequences of transition between states in a reactive (concurrent) system. It is common to use the temporal logic to specify the properties that the design must satisfy. The temporal logic is the basic of model checking. This paper states the syntax and semantics of CTL~* and its sub-logics: CTL and LTL, and analyzes how to state the properties of concurrent system, and finally the application example is given.
出处
《海军工程大学学报》
CAS
2004年第5期10-13,共4页
Journal of Naval University of Engineering
基金
国家自然科学基金资助项目(60273092)
江西省自然科学基金资助项目(0411041)
南昌大学2003年度科研基金资助项目
关键词
形式化方法
并发系统
时态逻辑
模型检测
formal method
concurrent system
temporal logic
model checking
