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

• 作者: 肖美华 薛锦云
• 来源期刊: 海军工程大学学报
• 学科: 工学
• 关键词: 形式化方法 并发系统 时态逻辑 模型检测
• 年，卷（期）: 2004,（5）
• 页码范围: 10-13
• 页数: 4页
• 分类号: TP302.2
• 字数: 3243字
• 语种: 中文
• DOI: 10.3969/j.issn.1009-3486.2004.05.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖美华	江西师范大学计算机信息工程学院	27	313	8.0	17.0
7	薛锦云	江西师范大学计算机信息工程学院	77	745	15.0	23.0