基于稳定模型的限界线性时序逻辑模型检测

本文提出将异步并发系统的限界模型检测作为回答集编程的一个有前景的应用领域。作为异步系统的模型，我们使用了通信自动机的一种推广——1-安全Petri网。我们展示了如何将1-安全Petri网及其行为需求转换为逻辑程序，从而通过计算相应程序的稳定模型来解决网络的限界模型检测问题。稳定模型语义的使用使得限界可达性和死锁检测任务以及更一般的线性时序逻辑限界模型检测问题能够被紧凑地编码。我们给出了所设计转换的正确性证明，并展示了使用该转换和Smodels系统的一些实验结果。