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

【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.更多还原