不精确信息下的交通操纵监控
Monitoring of Traffic Manoeuvres with Imprecise Information
摘要：
在监控中，我们通过算法检查单个行为是否满足某个属性。这里，我们考虑多通道空间逻辑（MLSL）的监控。该行为是作为一个有限的转移序列的MLSL和属性是一个空间MLSL公式应保持在每一个时间点内的序列。在我们的过程中，我们转换的过渡序列和公式的一阶理论的实闭域，这是可判定的，使得由此产生的公式是有效的，当且仅当MLSL公式保持整个过渡序列。然后，我们假设时间数据可能具有高达$\varepsilon$的误差，并且空间数据可能具有高达$δ$的误差。我们扩展我们的程序来检查MLSL公式$\varepsilon$ - $δ$ -是否在整个过渡序列中鲁棒地保持。
英文摘要：
In monitoring, we algorithmically check if a single behavior satisfies a property. Here, we consider monitoring for Multi-Lane Spatial Logic (MLSL). The behavior is given as a finite transition sequence of MLSL and the property is that a spatial MLSL formula should hold at every point in time within the sequence. In our procedure we transform the transition sequence and the formula to the first-order theory of real-closed fields, which is decidable, such that the resulting formula is valid iff the MLSL formula holds throughout the transition sequence. We then assume that temporal data may have an error of up to $\varepsilon$, and that spatial data may have an error of up to $δ$. We extend our procedure to check if the MLSL formula $\varepsilon$-$δ$-robustly holds throughout the transition sequence.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
