基于有穷论域下区间时序逻辑的模型检测研究  

Model Checking Based on Interval Temporal Logic under Finite Domain

作　　者：李超 LI Chao(School of Computer Science,Xi'an University of Posts and Telecommunications,Xi'an 710061)

机构地区：[1]西安邮电大学计算机学院

出　　处：《计算机与数字工程》2018年第7期1302-1305,1451,共5页Computer & Digital Engineering

摘　　要：通过结合自动机技术实现了有穷论域区间时序逻辑的判定算法,给出了有穷论域下区间时序逻辑变量、函数的处理方法,并提出了利用自动机进行系统建模的方法。最终实现了一个基于有穷论域区间时序逻辑的模型检测工具。Design and implementation of a model checker based on finite domain interval temporal logic are given,through the combination with automaton technology the decision algorithm of finite domain interval temporal logic is realized,a processing method of finite domain under interval temporal logic variable and function is given,and the method of system modeling using automaton is put forward.

关 键 词：区间时序逻辑 模型检测 自动机 

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