枚举 LTLf 公式的最小不可满足核心
人工智能
2024-09-17 v1 计算机科学中的逻辑
摘要
线性时间逻辑有限迹迹（Linear Temporal Logic over finite traces, ）是一种广泛使用的形式化方法，已在人工智能、过程矿业、模型检查等领域得到应用。 的主要推理任务为可满足性检查；然而，随着可解释人工智能的近期关注，分析不一致公式的兴趣日益增加，使得枚举 不可满足性解释的最低解释（minimal explanations for infeasibility）也成为相关任务。本文引入了一种新颖技术，用于枚举 规范的最小不可满足核心（MUCs）。主要思想是将 公式编码为答案集编程（Answer Set Programming, ASP）规范，使得 ASP 程序的最小不可满足子集（MUSes）直接对应原始 规范的 MUCs。利用 ASP 求解的最新进展，本文构建的 MUC 枚举器在文献中既定基准的实验中取得良好性能。
引用
@article{arxiv.2409.09485,
title = {Enumerating Minimal Unsatisfiable Cores of LTLf formulas},
author = {Antonio Ielo and Giuseppe Mazzotta and Rafael Peñaloza and Francesco Ricca},
journal= {arXiv preprint arXiv:2409.09485},
year = {2024}
}