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

摘要

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