《计算机学报》文章摘要   全文下载
  文章题目分布式状态机的代数模型及其模型检验算法
  作者刘 键
  作者单位(华中科技大学计算机学院 武汉 430074)
  发表年份2002
  发表月份4期　（页码：381—391)
  文章摘要分布式状态机（DSM）是一个分布式计算模型，特别适用于反应系统，有广泛的用途.但一般其正确性证明与模型检验的复杂性却很高，不易实用.作者曾提出了一个DSM的代 数模型及其模型检验算法，复杂性较低，但模型推导过程有点问题.该文加强了对DSM模型检验问题的提法，研究了解的结构特征，证明了可将DSM模型检验问题归结为不动点计算问题，并将Cleaveland和Steffen求不动点的方法用于同步模型不动点计算过程，然后将Bertsekas关于欧氏空间上的异步收敛定理推广到完备格上，从而将求解异步DSM方程不动点问题转化为求解同步方程不动点问题，证明了在适当的条件下，有υgEA=υgES，υgES与υgEA分别是DSM同步方程与异步方程的最大不动点.该同步算法的复杂性为O（|S|log|TRAN|），S为状态集，TRAN为转移关系式集.利用本文结果，可以有效地克服DSM进程之间的并发干扰所带来的各种困难，对分布式反应系统的可靠设计有很大的帮助. 关键词 分布式状态机,模型检验,最大不动点,DSM收敛定理,异步收敛定理 中图法分类号：TP391