一个一阶完备的结构化上下文无关语言的时态逻辑
摘要：针对模型检验过程性程序的问题，进行了许多研究以定义用于推理上下文无关结构的时间逻辑。其中最著名的是基于嵌套单词的时间逻辑，如CaRet和NWTL。最近，引入了基于运算符优先级语言（OPL）的逻辑OPTL，比嵌套单词更强大。我们定义了基于OPL的新逻辑POTL，并证明了其FO完备性。在异常类似结构下，POTL改进了NWTL，使得能够更好地表达包括前/后条件、堆栈检查等要求。它也改进了OPTL，我们展示了OPTL不是FO完备的，并且允许更容易地表达堆栈检查和函数本地属性。在一篇相关论文中，我们报告了POTL的模型检验过程和基于开发的原型工具的实验结果。为了完整起见，本文还提供了对这一补充结果的简要总结。
作者：Michele Chiari (1), Dino Mandrioli (1), Matteo Pradella (1 and 2) ((1) DEIB, Politecnico di Milano, (2) IEIIT, Consiglio Nazionale delle Ricerche)
论文ID：2105.10740
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22