线性逻辑规范的模型检查

本文的总体目标是探讨面向 first order linear logic 规范的算法验证技术的理论基础。我们在本文中考虑的线性逻辑片段基于一种名为 LO 的线性逻辑编程语言，该语言以普遍量化目标公式为特征。尽管 LO 最初被引入作为扩展逻辑编程语言的理论基础，但它也可以被视为一种非常通用的语言，用于指定广泛的 infinite-state 并发系统。我们的方法基于我们在针对命题 LO 程序中所发现的 backward reachability 与可证性关系。沿着这一研究线索，我们在此定义了一种用于评估 first order linear logic 规范的通用框架。该评估过程基于一种在符号表示的 infinite first order linear logic 公式集合上工作的有效 fixpoint 运算符。良好准则理论可用于提供评估 first order linear logic 非平凡片段的终止性的充分条件。