This thesis investigates the problem of computing the Minimal Unsatisfiable Core(MUC)of Linear Temporal Logic over finite traces(LTLf),which nowadays is a popular formal-specification language for AI-related systems.Efficient algorithms to compute such MUC can help locate the inconsistency rapidly in the written LTLf specification,and is very useful for the system designers to amend the flawed requirement.According to the research of this thesis,there are so far no available tools off-the-shelf that provide MUC computation for LTLf.The main work and contributions of this thesis are as follows:1.This thesis propose two general approaches based on deletion strategy for computing MUC in LTLf.The algorithms NaiveMUC and Binary MUC are designed and implemented to solve MUC,and correctness proofs are given for both algorithms.2.This thesis proposes a heuristic algorithm based on the Boolean unsatisfiable core(UC)technique with respect to the features of the LTLf language.The algorithm is integrated into two general algorithms,resulting in the optimized algorithms NaiveMUC+UC and BinaryMUC+UC.For special forms of global LTLf formulas,the article proves that the calculation of their MUC can be simplified to the MUC calculation of pure Boolean formulas,leading to the GlobalMUC method.3.This thesis presents a comparative analysis of the computational efficiency and size of the MUC obtained by the proposed algorithms on commonly used industrial benchmarks.This thesis also compares the proposed algorithm with other works that solve the LTLf unsatisfiable core,demonstrating the correctness of the proposed algorithm and the effectiveness of the UC heuristic through experimental results.4.This thesis describes the integration of five methods for solving the Minimal Unsatisfiable Core(MUC)problem in the LTLf satisfiability checking tool,called aaltafmuc.The tool also supports the verification of the correctness of the computed MUC.The source code of the solver is available on GitHub at https://github.com/nuutong/aaltafmuc.git. |