用于简单线性算术下监督器验证条件的Datalog重锤
计算机科学中的逻辑
2021-07-08 v1
摘要
基于简单线性实数算术约束的Bernays-Schönfinkel一阶逻辑片段BS(SLR)已知是可判定的。我们证明，带有全称和存在量词验证条件（猜想）的BS(SLR)子句集可翻译为基于有限一阶常量集的BS(SLR)子句集。对于Horn情形，我们提供了一种保持有效性和可满足性的Datalog重锤。从BS(LRA)证明器SPASS-SPL到Datalog推理器VLog的工具链，确立了判定Horn片段中验证条件的有效途径。这通过验证汽车换道辅助器的监督器代码和增压燃烧发动机的电子控制单元得以例证。
引用
@article{arxiv.2107.03189,
title = {A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic},
author = {Martin Bromberger and Irina Dragoste and Rasha Faqeh and Christof Fetzer and Markus Krötzsch and Christoph Weidenbach},
journal= {arXiv preprint arXiv:2107.03189},
year = {2021}
}
备注
26 pages