计算LTLf规约的不可满足核心
Computing unsatisfiable cores for LTLf specifications
AI总结：
针对有限迹线性时序逻辑（LTLf）规约的不可满足核心提取问题，本文通过适配主流LTLf可满足性检查方法提出四种算法，经基准测试验证了算法的可行性、有效性与互补性。
摘要：
有限迹线性时序逻辑（Linear-time temporal logic on finite traces，LTLf）正迅速成为众多应用领域（如规划、业务流程管理、运行时监控、反应式综合）中制定规约的事实标准。已有多项研究针对其可满足性问题展开探讨。本文研究了LTLf规约中不可满足核心的提取问题。我们通过适配当前主流的LTLf可满足性检查方法，提出了四种提取不可满足核心的算法。我们在相应工具中实现了这些不同方法，并在一组参考基准（仅选取不可满足的基准样例）上开展了实验评估。结果表明，不同算法和工具均具备可行性与有效性，且各有互补性。
英文摘要：
Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several studies approached the respective satisfiability problem. In this paper, we investigate the problem of extracting the unsatisfiable core in LTLf specifications. We provide four algorithms for extracting an unsatisfiable core leveraging the adaptation of state-of-the-art approaches to LTLf satisfiability checking. We implement the different approaches within the respective tools and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable ones. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
