摘要
通过结合自动机技术实现了有穷论域区间时序逻辑的判定算法,给出了有穷论域下区间时序逻辑变量、函数的处理方法,并提出了利用自动机进行系统建模的方法。最终实现了一个基于有穷论域区间时序逻辑的模型检测工具。
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.
作者
李超
LI Chao(School of Computer Science,Xi'an University of Posts and Telecommunications,Xi'an 710061)
出处
《计算机与数字工程》
2018年第7期1302-1305,1451,共5页
Computer & Digital Engineering
关键词
区间时序逻辑
模型检测
自动机
interval temporal logic
model checking
automaton
