分布式Model Checking线性时态逻辑属性

摘要：

提出了一种验证LTL属性的分布式嵌套深度优先算法(Distributed Double Depth First Algorithm—DDDFA).DDDFA运行在工作站网络或集群等分布主存环境上,通过验证一个自动机所接收的语言是否为空来判断模型系统是否满足某个LTL属性.为了加快验证速度,算法采用并行处理技术.此外还给出了算法正确性的证明.

关键词： 分布式 线性时态逻辑 Buchi自动机 深度优先搜索 分布式算法

作者: 徐蔚文 陆鑫达 曾志勇

作者单位: 上海交通大学计算机工程系(上海)

会议类型: 国内会议

会议名称: 2001年全国开放式分布与并行计算学术会议

会议地点: 南京

会议语种:中文

页码: 240-244

在线出版日期: 2001-10-01（万方平台首次上网日期，不代表论文的发表时间）