线性逻辑规范的模型检验
Model Checking Linear Logic Specifications
摘要：
本文的总体目标是研究一阶线性逻辑规格说明的算法验证技术的理论基础。我们在本文中考虑的线性逻辑片段是基于线性逻辑程序设计语言LO，它富含普遍量化的目标公式。虽然LO最初是作为逻辑程序设计语言扩展的理论基础引入的，但它也可以被视为一种非常通用的语言，用于指定各种无限状态并发系统。我们的方法是基于向后可达性和可证明性之间的关系，在我们以前的工作中强调命题LO程序。根据这条研究路线，我们在这里定义了一个一般框架，自下而上的评估一阶线性逻辑规范。评估过程是基于一个有效的不动点算子工作的一阶线性逻辑公式的无限集合的符号表示。良好拟序理论可以用来提供一阶线性逻辑非平凡片段求值终止的充分条件。
英文摘要：
The overall goal of this paper is to investigate the theoretical foundations of algorithmic verification techniques for first order linear logic specifications. The fragment of linear logic we consider in this paper is based on the linear logic programming language called LO enriched with universally quantified goal formulas. Although LO was originally introduced as a theoretical foundation for extensions of logic programming languages, it can also be viewed as a very general language to specify a wide range of infinite-state concurrent systems. Our approach is based on the relation between backward reachability and provability highlighted in our previous work on propositional LO programs. Following this line of research, we define here a general framework for the bottom-up evaluation of first order linear logic specifications. The evaluation procedure is based on an effective fixpoint operator working on a symbolic representation of infinite collections of first order linear logic formulas. The theory of well quasi-orderings can be used to provide sufficient conditions for the termination of the evaluation of non trivial fragments of first order linear logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
