软件学报

作者：谭锦豪，李国强

单位：谭锦豪，上海交通大学 软件学院, 上海 20024011,李国强，上海交通大学 软件学院, 上海 20024002

关键词：基本并行进程;限界模型检测;活性;线性整数算术;SMT求解

基金：国家自然科学基金（61872232，61732013）

基本并行进程是一个用于描述和分析并发程序的模型，是Petri网的一个重要子类.EG逻辑是一种在Hennessy-Milner Logic的基础上增加EG算子的分支时间逻辑，其中的AF算子表示从当前的状态出发性质最终会被满足，因此EG逻辑是能够表达活性的逻辑.然而，基于基本并行进程的EG逻辑的模型检测问题是不可判定的.由此，提出了基本并行进程上EG逻辑的限界模型检测方法.首先给出了基本并行进程上EG逻辑的限界语义，然后采用基于约束的方法，将基本并行进程上EG逻辑的限界模型检测问题转化为线性整数算术公式的可满足性问题，最后利用SMT求解器进行求解.

来源：2020年第8期

《软件学报》期刊编辑部

查看软件学报杂志2020年第8期