面向数据词的 LTLf 模论的统一自动机论方法（扩展版）
计算机科学中的逻辑
2024-08-19 v1
摘要
我们提出一种新颖的自动机方法，用于解决线性时序逻辑模论（LTL-MT），其作为数据词的规范语言。LTL-MT 通过将原子命题替换为解释于任意理论上的无量词多排序一阶公式，扩展了LTL_f。虽然标准LTL_f 被化简为有限自动机，但我们将LTL-MT 化简为符号数据词自动机（SDWAs），其转换由底层理论的约束所守卫。LTL-MT 和 SDWAs 的可满足性均不可判定，但后者可化简为受约束 Horn 子句系统，后者受到高效求解器和持续研究的支持。我们讨论了本方法超出可满足性之外的多个应用，包括模型检查和运行时监控。最后，一组实证实验表明，我们的方法在可满足性方面至少与前一种定制解决方案相当。
引用
@article{arxiv.2408.08817,
title = {A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)},
author = {Marco Faella and Gennaro Parlato},
journal= {arXiv preprint arXiv:2408.08817},
year = {2024}
}
备注
Published at ECAI'24 (Extended Version)