| 基于线性时态逻辑的Petri网模型检测研究 |
| |
| 引用本文： | 赵晓凡,周清雷,赵东明.基于线性时态逻辑的Petri网模型检测研究[J].微计算机信息,2009,25(3). |
| |
| 作者姓名： | 赵晓凡 周清雷 赵东明 |
| |
| 作者单位： | 郑州,郑州大学信息工程学院,河南,450052
|
| |
| 基金项目： | 河南省教育厅项目，河南省自然科学基金 |
| |
| 摘 要： | 线性时态逻辑Petri网结合了Petri网和时序逻辑的优点,清晰简洁的描述并发系统事件间的时序和因果关系,包括系统的活性和安全性.其中自动机的体积是模型检验的一个关键性问题,为了得到尽可能小体积的自动机,在LTL公式转换为Büchi自动机之前,对LTL公式进行预处理来减少冗余,然后通过布尔技术优化自动机.
|
| 关 键 词： | 线性时态逻辑 Petri网 Büchi自动机 模型检测 |
Research on Model Checking of Petri Nets Based on Linear Temporal Logic |
| |
| ZHAO Xiao-fan,ZHOU Qing-lei,ZHAO Dong-ming.Research on Model Checking of Petri Nets Based on Linear Temporal Logic[J].Control & Automation,2009,25(3). |
| |
| Authors: | ZHAO Xiao-fan ZHOU Qing-lei ZHAO Dong-ming |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
