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

Reasoning rules of four grades fairness in temporal logic of action

作　　者：唐郑熠[1,2] 薛醒思[1] 王金水[1] 王晓峰[2,3] Tang Zhengyi;Xue Xingsi;Wang Jinshui;Wang Xiaofeng(School of Information Science & Engineering, Fujian University of Technology, Fuzhou 350118 , China;School of Computer Science & Technology, Guizhou University, Guiyang 550025 , China;School of Computer Science & Engineering, North University of Nationalities, Yinchuan 750021 , China)

机构地区：[1]福建工程学院信息科学与工程学院,福州350118 [2]贵州大学计算机科学与技术学院,贵阳550025 [3]北方民族大学计算机科学与工程学院,银川750021

出　　处：《计算机应用研究》2016年第10期3045-3048,共4页Application Research of Computers

基　　金：福建省自然科学基金计划资助项目(2016J05146);国家自然科学基金资助项目(61503082);福州市科技基金资助项目(2012-G-126);福建工程学院科研启动基金资助项目(GY-Z13112)

摘　　要：公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,通过对公平性内涵的分析,给出了四级公平性体系下的活性推理规则,并分别进行了证明。作为示例,运用新的活性推理规则对一个程序实例进行了推理验证,在建立起相应的活性推理规则后,四级公平性才能够被有效运用到实际的系统描述与验证中。Fairness is the representation of system liveness in the temporal logic of action( TLA),it affects the correctness and completeness of system description directly. The refinement of fairness can improve the description ability of TLA. But there is short of corresponding reasoning rules which can be used to property verification. For this problem,this paper gave the reasoning rules of four grades fairness by analysising the intension of fairness,and it also proved the correctness of rules. As a example,it used the new reasoning rules to verify a program by inferring. Now the four grades fairness can be used to describe and verify system by this work.

关 键 词：行为时序逻辑 公平性 活性 推理规则 系统验证 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]