将LTLf公式转为ASP求解，高效找出最小不满足核心
Enumerating Minimal Unsatisfiable Cores of LTLf formulas
- 把LTLf公式转化为ASP程序，利用其可解性找不满足核心
- 在标准基准上表现良好，能有效枚举最小不满足子集
- 适合做AI可解释性、模型检验中矛盾分析的研究者
线性时序逻辑有限轨迹（LTL_f）在人工智能、流程挖掘、模型检测等领域广泛应用。其主要推理任务是满足性检查；然而，随着可解释AI的发展，对不一致公式的分析日益重要，使得枚举不可行性的最小解释成为关键任务。本文提出一种新方法，用于枚举LTL_f规范的最小不满足核心（MUCs）。核心思想是将LTL_f公式编码为答案集编程（ASP）规范，使该ASP程序的最小不满足子集（MUSes）直接对应原LTL_f公式的MUCs。借助近年ASP求解技术的进步，实验表明该方法在文献中的标准基准上具有良好的性能。
原文摘要 · Abstract (English)
Linear Temporal Logic over finite traces ($\text{LTL}_f$) is a widely used formalism with applications in AI, process mining, model checking, and more. The primary reasoning task for $\text{LTL}_f$ is satisfiability checking; yet, the recent focus on explainable AI has increased interest in analyzing inconsistent formulas, making the enumeration of minimal explanations for infeasibility a relevant task also for $\text{LTL}_f$. This paper introduces a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an $\text{LTL}_f$ specification. The main idea is to encode a $\text{LTL}_f$ formula into an Answer Set Programming (ASP) specification, such that the minimal unsatisfiable subsets (MUSes) of the ASP program directly correspond to the MUCs of the original $\text{LTL}_f$ specification. Leveraging recent advancements in ASP solving yields a MUC enumerator achieving good performance in experiments conducted on established benchmarks from the literature.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。