超性质的一阶逻辑
计算机科学中的逻辑
2017-01-10 v2 密码学与安全
逻辑
摘要
我们研究超性质的逻辑基础。超性质将迹性质（即迹的集合）推广为迹的集合的集合。超性质最突出的应用是信息流安全：信息流策略通过比较两个或多个执行迹来刻画系统的保密性和完整性，例如比较外部观察者在由不同秘密变量值产生的执行迹上所做的观察。在本文中，我们首次建立了超性质的时序逻辑与一阶逻辑之间的联系。Kamp 的开创性定理（根据 Gabbay 等人的表述）指出，线性时序逻辑 (LTL) 在表达力上等价于带序的自然数上的一阶逻辑。我们引入迹集合上的一阶逻辑，并证明 HyperLTL（LTL 到超性质的扩展）被该逻辑严格包含。我们进一步展示了一个在表达力上与 HyperLTL 等价的片段，从而为超性质建立了 Kamp 定理。
引用
@article{arxiv.1610.04388,
title = {The First-Order Logic of Hyperproperties},
author = {Bernd Finkbeiner and Martin Zimmermann},
journal= {arXiv preprint arXiv:1610.04388},
year = {2017}
}