定量与近似监控

在运行时验证中，监视器观察系统的轨迹，并尽可能在观察到每个有限前缀后，判定未知的无限轨迹是否满足给定规约。我们将运行时验证理论推广到试图估计定量轨迹属性（而非试图得出轨迹规约的布尔值）数值的监视器，例如轨迹上的最大或平均响应时间。定量监视器是近似的：对于每个有限前缀，它们可以改进对无限轨迹未知属性值的估计。因此，定量监视器可以在精度-代价权衡方面进行比较：对属性值更好的近似需要更多的监视器资源，例如状态（在有限状态监视器的情况下）或寄存器，而额外的资源会带来更好的近似。我们引入了定量与近似监控的形式化框架，展示了它如何保守地推广经典的布尔监控设定，并给出了监视器的若干精度-代价权衡。例如，我们证明存在某些定量属性，对于它们，每一个额外的寄存器都能提高监控精度。