区间时序逻辑的模型检查  

Model checking interval temporal logic

作　　者：张海宾[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算机学院,陕西西安710071

出　　处：《西安电子科技大学学报》2009年第2期338-342,共5页Journal of Xidian University

基　　金：国家自然科学基金资助(60873018;60871097);国家自然科学基金重大项目资助(60433010);博士点基金资助(200807010012)

摘　　要：为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则.利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合.同时,定义了一套转换规则把一个chop-自动机转换为一个标注有限状态自动机,使得它们接受相同的原子命题序列集.这样,区间时序逻辑的模型检查问题就等价地转换成了很容易解决的两个标注有限状态自动机的语言包含问题.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.

关 键 词：模型检查 时序逻辑 自动机 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]