| 分布式状态机的代数模型及其模型检验算法 |
| |
| 引用本文： | 刘键.分布式状态机的代数模型及其模型检验算法[J].计算机学报,2002,25(4):381-391. |
| |
| 作者姓名： | 刘键 |
| |
| 作者单位： | 华中科技大学计算机学院,武汉,430074 |
| |
| 摘 要： | 分布式状态机（DSM）是一个分布式计算模型，特别适用于反应系统，有广泛的用途，但一般其正确性证明与模型检验的复杂性却很高，不易实用。作者曾提出了一个DSM的代数模型及其模型检验算法，复杂较低，但模型推导过程有点问题。该文加强了对DSM模型检验问题的提法，研究了解的结构特征，证明了可将DSM模型检验问题归结为不动点计算问题，并将Cleaveland和Steffen求不动点的方法用于同步模型不动点计算过程，然后将Bertsekas关于欧氏空间上的异步收敛定理推广到完备格上，从而将求解异步DSM方程不动点问题转化为求解同步方程不动点问题，证明了在适当的条件下，有vgEA＝vgES,vgES与vgEA分别是DSM同步方程与异步方程的大不同动点，该同步算法的复杂性为O（|S|log|TRAN|),S为状态集，TRAN为转移关系式集，利用本文结果，可以有效地克服了DSM进程之间的并发干扰所带来的各种困难，对分布式反应系统的可靠设计有很大的帮助。
|
| 关 键 词： | 分布式状态机 模型检验 异步收敛定理 代数模型 算法 程序设计方法 |
| 修稿时间： | 2000年4月22日 |
Algebraic Model for Distributed State Machine and Its Model Checking Algorithm |
| |
| LIU Jian.Algebraic Model for Distributed State Machine and Its Model Checking Algorithm[J].Chinese Journal of Computers,2002,25(4):381-391. |
| |
| Authors: | LIU Jian |
| |
| Abstract: | |
| |
| Keywords: | distributed state machine model checking greatest fixed point DSM convergence theorem asynchronous convergence theorem |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
