Model checking interval temporal logic

被引：0

作者：

Zhang, Hai-Bin ^{[1
]}

Duan, Zhen-Hua ^{[1
]}

机构：

[1] School of Computer Science and Technology, Xidian Univ., Xi'an 710071, China

来源：

Xi'an Dianzi Keji Daxue Xuebao/Journal of Xidian University | 2009年 / 36卷 / 02期

关键词：

Automata - Interval temporal logic - Model checking problem - Set of rules;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

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.

引用

页码：338 / 342