超性质监控的复杂性
计算机科学中的逻辑
2021-01-21 v1
摘要
我们研究以时序逻辑 HyperLTL 表达的超性质在运行时验证，作为针对安全策略检查系统的手段。超性质的运行时监控器分析按公共前缀组织为树形 Kripke 结构、或按公共前缀与公共后缀组织为无环 Kripke 结构的迹日志。与迹性质的运行时验证技术（监控器跟踪规约状态但通常无需存储迹）不同，超性质监控器反复对不断增长的 Kripke 结构进行模型检测。这需要对树形与无环 Kripke 结构上的模型检测问题进行严格的复杂性分析。我们证明，对于树结构，复杂性在 Kripke 结构大小上独立于 HyperLTL 公式中量词交替次数为 L-完全。对于无环 Kripke 结构，复杂性为 PSPACE-完全（对应于量词交替次数的多项式层级级别）。在 Kripke 结构大小与 HyperLTL 公式长度上的联合复杂性，对树与无环 Kripke 结构均为 PSPACE-完全，而在相关的树与无交替 HyperLTL 公式情形下低至 NC。因此，Kripke 结构与公式的大小及形状对模型检测问题的复杂性有显著影响。
引用
@article{arxiv.2101.07847,
title = {The Complexity of Monitoring Hyperproperties},
author = {Borzoo Bonakdarpour and Bernd Finkbeiner},
journal= {arXiv preprint arXiv:2101.07847},
year = {2021}
}