国内刊号：11-2560/TP
国际刊号：1000-9825
发布日期:
作者：吴志文，李国强
单位：吴志文，上海交通大学 软件学院, 上海 20024011,李国强，上海交通大学 软件学院, 上海 20024002
关键词：异步程序;非交互式Petri网;∈可达性;∈等价性;可达性
基金：国家自然科学基金(61872232,61732013)
异步程序使用异步非阻塞调用方式来实现程序的并发, 被广泛应用于并行与分布式系统中. 验证异步程序复杂性很高, 无论是安全性还是活性均达到EXPSPACE难. 提出一个异步程序的程序模型系统, 并在其上定义两个异步程序上的问题: $ \epsilon $等价性问题和$ \epsilon $可达性问题. 通过将3-CNF-SAT规约到这两个问题, 再将其规约至非交互式Petri网的可达性证明两个问题是NP完备的. 案例表明, 这两个问题可以解决异步程序上一系列的程序验证问题.
来源：2023年第8期
《软件学报》期刊编辑部