基于约束的超性质监控
计算机科学中的逻辑
2019-06-03 v1
摘要
在运行时验证超性质是一个具有挑战性的问题，因为诸如非干扰和观测确定性等超性质将多条计算迹相互关联。有必要存储先前看到的迹，因为每一条新到达的迹都需要与迄今为止观察到的系统的每一次运行兼容。此外，新到达的迹对未来的迹提出了要求。在我们的监控方法中，我们通过将时序逻辑 HyperLTL 中的超性质重写为布尔约束系统来关注这些要求。如果约束系统变得不可满足，则系统多次运行违反了超性质。我们将利用 BDD 或 SAT 求解器来存储和评估约束的实现与基于自动机的监控工具 RVHyper 进行了比较。
引用
@article{arxiv.1905.13517,
title = {Constraint-Based Monitoring of Hyperproperties},
author = {Christopher Hahn and Marvin Stenger and Leander Tentrup},
journal= {arXiv preprint arXiv:1905.13517},
year = {2019}
}