行为时序逻辑中四级公平性下的活性推理规则

• 作者: 唐郑熠 王晓峰 王金水 薛醒思
• 来源期刊: 计算机应用研究
• 关键词: 行为时序逻辑 公平性 活性 推理规则 系统验证
• 年，卷（期）: 2016,（10）
• 所属期刊栏目: 软件技术研究
• 页码范围: 3045-3048
• 页数: 4页
• 分类号: TP301.2
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2016.10.039

摘要

公平性是行为时序逻辑用于表达系统活性的形式，直接影响到系统描述的正确性与完整性，对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时，却缺乏相应的、运用于性质验证的推理规则。针对这一问题，通过对公平性内涵的分析，给出了四级公平性体系下的活性推理规则，并分别进行了证明。作为示例，运用新的活性推理规则对一个程序实例进行了推理验证，在建立起相应的活性推理规则后，四级公平性才能够被有效运用到实际的系统描述与验证中。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	薛醒思	福建工程学院信息科学与工程学院	26	18	2.0	3.0
2	王晓峰	贵州大学计算机科学与技术学院	26	122	6.0	9.0
4	唐郑熠	福建工程学院信息科学与工程学院	17	19	3.0	3.0
8	王金水	福建工程学院信息科学与工程学院	13	20	3.0	3.0