| 行为时序逻辑中四级公平性下的活性推理规则 |
| |
| 引用本文： | 唐郑熠,薛醒思,王金水,王晓峰.行为时序逻辑中四级公平性下的活性推理规则[J].计算机应用研究,2016,33(10). |
| |
| 作者姓名： | 唐郑熠 薛醒思 王金水 王晓峰 |
| |
| 作者单位： | 福建工程学院 信息科学与工程学院,福建工程学院 信息科学与工程学院,福建工程学院 信息科学与工程学院,北方民族大学 计算机科学与工程学院 |
| |
| 基金项目： | 福建省自然科学基金计划资助项目(2016J05146);国家自然科学基金资助项目(61503082);福州市科技基金资助项目(2012-G-126);福建工程学院科研启动基金资助项目(GY-Z13112) |
| |
| 摘 要： | 公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,通过对公平性内涵的分析,给出了四级公平性体系下的活性推理规则,并分别进行了证明。作为示例,运用新的活性推理规则,对一个程序实例进行了推理验证。在建立起相应的活性推理规则后,四级公平性才能够被有效运用到实际的系统描述与验证中。
|
| 关 键 词： | 行为时序逻辑 公平性 活性 推理规则 系统验证 |
| 收稿时间： | 8/2/2015 12:00:00 AM |
| 修稿时间： | 2016/8/21 0:00:00 |
The reasoning rules of four grades fairness in temporal logic of action |
| |
| TANG Zheng-yi,XUE Xing-si,WANG Jin-shui and WANG Xiao-feng.The reasoning rules of four grades fairness in temporal logic of action[J].Application Research of Computers,2016,33(10). |
| |
| Authors: | TANG Zheng-yi XUE Xing-si WANG Jin-shui and WANG Xiao-feng |
| |
| Affiliation: | School of Information Science and Engineering,Fujian University of Technology,School of Information Science and Engineering,Fujian University of Technology,School of Information Science and Engineering,Fujian University of Technology,School of Computer Science and Engineering, North University of Nationalities |
| |
| Abstract: | |
| |
| Keywords: | temporal logic of action fairness liveness reasoning rules system verification |
|
| 点击此处可从《计算机应用研究》浏览原始摘要信息 |
|
点击此处可从《计算机应用研究》下载全文 |
|
