| 一种基于时态逻辑的有限状态系统验证方法 |
| |
| 引用本文： | 杜慧敏,杨红丽,高德远,韩俊刚.一种基于时态逻辑的有限状态系统验证方法[J].西北工业大学学报,2000,18(1):111-115. |
| |
| 作者姓名： | 杜慧敏 杨红丽 高德远 韩俊刚 |
| |
| 作者单位： | 1. 西北工业大学,计算机科学系,陕西,西安,710072
2. 西安邮电学院,计算机系,陕西,西安,710061 |
| |
| 基金项目： | 国家自然科学基金!694 73 0 17 |
| |
| 摘 要： | ＬＰＴＬ与自动机之间有着紧密的联系，结合ＬＰＴＬ语义和语法，提出一种从ＬＰＴＬ公式导出Ｂｕｃｈｉ自动机的方法。导出的Ｂｕｃｈｉ自动机所接受的语言准确地表达了ＬＰＴＬ公式所描述的特性。从而把由ＬＰＴＬ公式描述的系统设计规范的验证问题转换成检验Ｂｕｃｈｉ自动机的包含问题。
|
| 关 键 词： | 命题时态逻辑 形式化验证 有限状态系统 自动机 |
| 文章编号： | 1000-2758(2000)01-0111-05 |
| 修稿时间： | 1998-03-24 |
A Verification Method For Finite States Systems Based on Temporal Logic |
| |
| Du Huimin,Gao Deyuan,Yang Hongli,Han Jungang.A Verification Method For Finite States Systems Based on Temporal Logic[J].Journal of Northwestern Polytechnical University,2000,18(1):111-115. |
| |
| Authors: | Du Huimin Gao Deyuan Yang Hongli Han Jungang |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
