SaSTL：面向智慧城市运行时监控的空间聚合信号时序逻辑

我们提出 SaSTL——一种新颖的空间聚合信号时序逻辑（Spatial Aggregation Signal Temporal Logic）——用于智慧城市中安全与性能需求的高效运行时监控。我们首先描述了一项对超过 1,000 条智慧城市需求的研究，其中部分需求无法用现有逻辑如信号时序逻辑（STL）及其变体来规约。为应对此局限，我们在 SaSTL 中开发了两个新逻辑算子以扩充 STL，用于表达真实城市需求中常见的空间聚合与空间计数特征。我们还开发了高效监控算法，可跨多个数据流（例如由城市中空间分布的多个传感器生成的流）并行检查 SaSTL 需求。我们通过将两个案例研究应用于大规模真实城市感知数据（例如一条需求至多 10,000 个传感器）来评估 SaSTL 监控器。结果表明，SaSTL 比其他空间时序逻辑具有更高的覆盖表达力，并显著减少了需求监控的计算时间。我们还通过模拟实验证明 SaSTL 监控器可助力提升智慧城市的安全与性能。