面向一类基于轮数的分布式算法的状态空间分析与模型检测
| 摘要 | 第1-10页 |
| ABSTRACT | 第10-12页 |
| 第一章 介绍 | 第12-16页 |
| ·研究背景 | 第12页 |
| ·问题描述 | 第12-13页 |
| ·本文工作 | 第13-14页 |
| ·论文结构 | 第14-16页 |
| 第二章 相关工作 | 第16-26页 |
| ·分布式算法 | 第16-20页 |
| ·网络模型 | 第16-17页 |
| ·领袖选举 | 第17-18页 |
| ·分布式一致性 | 第18-20页 |
| ·模型检测 | 第20-24页 |
| ·Spin模型检测器 | 第20-21页 |
| ·Promel语言 | 第21-23页 |
| ·线性时序逻辑 | 第23页 |
| ·验证选项 | 第23-24页 |
| ·状态空间爆炸 | 第24页 |
| ·领袖选举算法的形式化验证 | 第24页 |
| ·分布式一致性算法的形式化验证 | 第24-26页 |
| 第三章 基于轮数相对距离的无限状态空间转换方法 | 第26-29页 |
| ·基于轮数相对距离的无限状态空间转换方法 | 第26页 |
| ·有效性与合理性证明 | 第26-29页 |
| 第四章 领袖选举算法的模型检测 | 第29-47页 |
| ·Itai-Rodeh领袖选举算法的模型检测 | 第29-39页 |
| ·Itai-Rodeh算法 | 第29-31页 |
| ·轮数之间相互关系的分析 | 第31-32页 |
| ·算法的模型检测 | 第32-39页 |
| ·改进的Itai-Rodeh算法的模型检测 | 第39-47页 |
| ·不带脏位的算法 | 第39页 |
| ·轮数之间相互关系的分析 | 第39-41页 |
| ·算法的模型检测 | 第41-44页 |
| ·算法正确性证明 | 第44-47页 |
| 第五章 分布式一致性算法的模型检测 | 第47-65页 |
| ·BT概率一致性算法的模型检测 | 第47-55页 |
| ·BT概率一致性算法 | 第47-49页 |
| ·对空间爆炸问题的分析和处理 | 第49-52页 |
| ·算法的模型检测 | 第52-55页 |
| ·一个旋转协调者算法的模型检测 | 第55-65页 |
| ·旋转协调者算法 | 第56页 |
| ·对空间爆炸问题的分析和处理 | 第56-60页 |
| ·算法的模型检测 | 第60-65页 |
| 第六章 总结与展望 | 第65-67页 |
| ·总结 | 第65-66页 |
| ·将来工作 | 第66-67页 |
| 参考文献 | 第67-71页 |
| 致谢 | 第71-72页 |
| 攻读学位期间发表的学术论文目录 | 第72-73页 |
| 学位论文评阅及答辩情况表 | 第73页 |
