论文部分内容阅读
分布式状态机(DSM)是一个分布式计算模型,特别适用于反应系统,有广泛的用途.但一般其正确性证明与模型检验的复杂性却很高,不易实用.作者曾提出了一个DSM的代数模型及其模型检验算法,复杂性较低,但模型推导过程有点问题.该文加强了对DSM模型检验问题的提法,研究了解的结构特征,证明了可将DSM模型检验问题归结为不动点计算问题,并将Cleaveland和Steffen求不动点的方法用于同步模型不动点计算过程,然后将Bertsekas关于欧氏空间上的异步收敛定理推广到完备格上,从而将求解异步DSM方程不动点问题