使用前缀转换器监控超属性
摘要：通过使用（多重跟踪）前缀传导器，我们展示了如何对同步和异步超属性进行监控。前缀传导器将多个输入跟踪映射到一个或多个输出跟踪，通过逐步将输入跟踪的前缀与类似于正则表达式的表达式进行匹配。相同的跟踪的前缀在监视器的单个匹配步骤中可能具有不同的长度。前缀传导器的确定性和可执行性使它们比逻辑规范更适合作为运行时验证的中间形式，特别是在异步超属性的情况下，逻辑规范往往具有很高的非确定性。我们报告了一系列关于监测观测确定性异步版本的实验。
作者：Marek Chalupa and Thomas A. Henzinger
论文ID：2308.03626
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-08