基于非交互式Petri网的异步程序验证模型和方法

摘要：

异步程序使用异步非阻塞调用方式来实现程序的并发,被广泛应用于并行与分布式系统中.验证异步程序复杂性很高,无论是安全性还是活性均达到EXPSPACE难.提出一个异步程序的程序模型系统,并在其上定义两个异步程序上的问题:等价性问题和 可达性问题.通过将 3-CNF-SAT规约到这两个问题,再将其规约至非交互? ?式Petri网的可达性证明两个问题是NP完备的.案例表明,这两个问题可以解决异步程序上一系列的程序验证问题.

关键词：异步程序、非交互式Petri网、ϵ可达性、ϵ等价性

所属期刊栏目：34

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金;国家自然科学基金

在线出版日期：2023-08-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：3674-3685