计算机应用研究2016，Vol.33Issue(10)：3045-3048,4.DOI:10.3969/j.issn.1001-3695.2016.10.039
行为时序逻辑中四级公平性下的活性推理规则
Reasoning rules of four grades fairness in temporal logic of action
摘要
Abstract
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 reaso-ning rules of four grades fairness by analysising the intension of fairness,and it also proved the correctness of rules.As a exa-mple,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.关键词
行为时序逻辑/公平性/活性/推理规则/系统验证Key words
temporal logic of action/fairness/liveness/reasoning rules/system verification分类
信息技术与安全科学引用本文复制引用
唐郑熠,薛醒思,王金水,王晓峰..行为时序逻辑中四级公平性下的活性推理规则[J].计算机应用研究,2016,33(10):3045-3048,4.基金项目
福建省自然科学基金计划资助项目（2016J05146）；国家自然科学基金资助项目（61503082）；福州市科技基金资助项目（2012-G-126）；福建工程学院科研启动基金资助项目 （）
