时态逻辑形式化描述并发系统性质

作者：肖美华; 薛锦云

来源：海军工程大学学报, 2004, (05): 10-13.

• 形式化方法
• 并发系统
• 时态逻辑
• 模型检测

时态逻辑是一种描述反应式(并发)系统中状态迁移序列的形式化方法,用于刻画并发系统所需验证的性质,是模型检测的基础.阐述了时态逻辑CTL 及其子逻辑CTL、LTL的语法及语义,然后分析运用时态逻辑描述并发系统性质,最后给出一个应用实例.

• 单位
  江西师范大学; 中国科学院软件研究所; 计算机科学国家重点实验室; 南昌大学