LTLf 与 LDLf 监控：技术报告
人工智能
2014-05-02 v1 软件工程
摘要
运行时监控是为运行中的业务流程提供操作决策支持并即时检查其是否合规的核心任务之一。我们研究在有限迹上表达的 LTL (LTLf) 及其扩展 LDLf 所述性质的运行时监控。LDLf 是一种强大的逻辑，能够刻画有限迹上的所有单子二阶逻辑，它通过结合正则表达式与 LTLf 并采用命题动态逻辑 (PDL) 的语法获得。有趣的是，尽管表达能力更强，LDLf 的计算复杂度与 LTLf 完全相同。我们表明，LDLf 能够在逻辑自身内部不仅刻画待监控的约束，还能刻画事实上的标准 RV-LTL 监控器。这使得声明式地刻画监控元约束成为可能，并可通过依赖常规逻辑服务而非特设算法对其进行检查。这进而能够灵活地监控依赖于其他约束监控状态的约束，例如仅在检测到其他约束被违反时才检查的“补偿”约束。此外，我们设计了一种将 LDLf 公式直接翻译为非确定性自动机的方法，避免了绕道至 Buechi 自动机或交替自动机，并利用该方法为 PROM 套件实现了一个监控插件。
引用
@article{arxiv.1405.0054,
title = {LTLf and LDLf Monitoring: A Technical Report},
author = {Giuseppe De Giacomo and Riccardo De Masellis and Marco Grasso and Fabrizio Maggi and Marco Montali},
journal= {arXiv preprint arXiv:1405.0054},
year = {2014}
}