分布式状态机的代数模型及其模型检验算法

• 作者: 刘键
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 分布式状态机 模型检验 最大不动点 DSM收敛定理 异步收敛定理
• 年，卷（期）: 2002,（4）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 381-391
• 页数: 11页
• 分类号: TP391
• 字数: 14271字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2002.04.007

摘要

分布式状态机(DSM)是一个分布式计算模型,特别适用于反应系统,有广泛的用途.但一般其正确性证明与模型检验的复杂性却很高,不易实用.作者曾提出了一个DSM的代数模型及其模型检验算法,复杂性较低,但模型推导过程有点问题.该文加强了对DSM模型检验问题的提法,研究了解的结构特征,证明了可将DSM模型检验问题归结为不动点计算问题,并将Cleaveland和Steffen求不动点的方法用于同步模型不动点计算过程,然后将Bertsekas关于欧氏空间上的异步收敛定理推广到完备格上,从而将求解异步DSM方程不动点问题转化为求解同步方程不动点问题,证明了在适当的条件下,有υgEA=υgES,υgES与υgEA分别是DSM同步方程与异步方程的最大不动点.该同步算法的复杂性为O(|S|log|TRAN|),S为状态集,TRAN为转移关系式集.利用本文结果,可以有效地克服DSM进程之间的并发干扰所带来的各种困难,对分布式反应系统的可靠设计有很大的帮助.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘键	华中科技大学计算机学院	1	0	0.0	0.0