一种基于时态逻辑的有限状态系统验证方法

杜慧敏; 杨红丽; 高德远; 韩俊刚

首页> 中文期刊> 《西北工业大学学报》 >一种基于时态逻辑的有限状态系统验证方法

一种基于时态逻辑的有限状态系统验证方法

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

LPTL(Linear Proposition Temporal Logic)与自动机之间有着紧密的联系,结合LPTL语义和语法,提出一种从LPTL公式导出Bchi自动机的方法.导出的Bchi自动机所接受的语言准确地表达了LPTL公式所描述的特性.从而把由LPTL公式描述的系统设计规范的验证问题转换成检验Bchi自动机的包含问题.

著录项

来源
《西北工业大学学报》 |2000年第1期|111-115|共5页
作者
杜慧敏; 杨红丽; 高德远; 韩俊刚;
展开▼
作者单位

西北工业大学,计算机科学系,陕西,西安,710072;

西安邮电学院,计算机系,陕西,西安,710061;

西北工业大学,计算机科学系,陕西,西安,710072;

西安邮电学院,计算机系,陕西,西安,710061;

展开▼
原文格式 PDF
正文语种 chi
中图分类自动机理论;
关键词
命题时态逻辑; Bchi自动机; 形式化验证;

相似文献

中文文献
外文文献
专利

1. 一种基于有限状态机的逻辑看门狗实现方案 [J] . 唐启翔 ,康健 ,邹旭军 . 信息通信 . 2018,第009期
2. 一种基于微分代数动态逻辑的CPS建模与验证方法 [J] . 陈乔乔 ,李必信 ,吉顺慧 . 计算机研究与发展 . 2013,第004期
3. 一种基于描述逻辑的UML模型验证方法 [J] . 郝斐 ,董庆超 ,曾广军 . 计算机与数字工程 . 2011,第011期
4. 一种基于逻辑约束的软件设计过程验证方法及其工程实践 [J] . 何俊梅 ,邹显春 . 西南师范大学学报（自然科学版） . 2007,第004期
5. 一种基于SVO逻辑的新形式化验证方法 [J] . 王茜 ,杨德礼 . 计算机集成制造系统 . 2004,第003期
6. 一种基于时态逻辑的有限状态系统验证方法1 [C] . 杜慧敏 ,袁立行 . 中国电子学会第四届青年学术年会 . 1998
7. 基于SystemC的时态逻辑属性验证方法研究 [A] . 王胜 . 2009

一种基于时态逻辑的有限状态系统验证方法

摘要

著录项

相似文献

相关主题

期刊订阅