一种命题投影时序逻辑的分布式模型检测方法
Journal of Xidian University(Natural Science)（2020）
摘要
为缓解模型检测的状态空间爆炸问题,提出一种基于命题投影时序逻辑的分布式模型检测方法.通过标记范式图技术将命题投影时序逻辑公式描述的待验证性质转换为自动机;根据强连通分量将其状态空间划分为多个子自动机,将各个子自动机与层次语法图描述的待验证系统模型分发至验证服务器集群中,使用动态验证技术进行多机协同完成系统模型检测验证.实验结果表明,该方法和单机模型检测相比验证时间明显降低,且能够验证更复杂的系统.
更多AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要