| 区间时序逻辑的模型检查 |
| |
| 引用本文： | 张海宾,段振华.区间时序逻辑的模型检查[J].西安电子科技大学学报,2009,36(2):338-342. |
| |
| 作者姓名： | 张海宾 段振华 |
| |
| 作者单位： | (西安电子科技大学 计算机学院，陕西 西安 710071) |
| |
| 基金项目： | 国家自然科学基金，国家自然科学基金重大项目，高等学校博士学科点专项科研基金 |
| |
| 摘 要： | 为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质，定义了一套转换规则．利用这些规则，可以构造一个chop-自动机，该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合．同时，定义了一套转换规则把一个chop-自动机转换为一个标注有限状态自动机，使得它们接受相同的原子命题序列集．这样，区间时序逻辑的模型检查问题就等价地转换成了很容易解决的两个标注有限状态自动机的语言包含问题．
|
| 关 键 词： | 模型检查 时序逻辑 自动机 |
| 收稿时间： | 2008-02-20 |
Model checking interval temporal logic |
| |
| ZHANG Hai-bin,DUAN Zhen-hua.Model checking interval temporal logic[J].Journal of Xidian University,2009,36(2):338-342. |
| |
| Authors: | ZHANG Hai-bin DUAN Zhen-hua |
| |
| Affiliation: | (School of Computer Science and Technology, Xidian Univ., Xi’an 710071， China) ; |
| |
| Abstract: | To check whether a system represented by a labelled finite state automaton meets a property described by an interval temporal logic formula, a set of rules are defined. Using such rules, a chop-automaton which accepts all intervals satisfying this interval temporal logic formula can be constructed. In addition, a rule for translating a chop-automaton to a labelled finite state automaton is also defined. Thus, the model checking problem for the interval temporal logic can be solved by testing language inclusion between two labelled finite state automata. |
| |
| Keywords: | model checking temporal logic automata |
| 本文献已被 维普 万方数据 等数据库收录！ |
| 点击此处可从《西安电子科技大学学报》浏览原始摘要信息 |
|
点击此处可从《西安电子科技大学学报》下载全文 |
