{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T21:40:08Z","timestamp":1729719608948,"version":"3.28.0"},"reference-count":40,"publisher":"Oxford University Press (OUP)","issue":"7","license":[{"start":{"date-parts":[[2023,8,4]],"date-time":"2023-08-04T00:00:00Z","timestamp":1691107200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,10,23]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>In this paper, we consider the minimal unsatisfiable core (MUC) problem for linear temporal logic over finite traces (LTL$_{f}$), which nowadays is a popular formal-specification language for AI-related systems. Efficient algorithms to compute such MUCs can help locate the inconsistency rapidly in the written LTL$_{f}$ specification and are very useful for the system designers to amend the flawed requirement. As far as we know, there are no available tools off-the-shelf so far that provide MUC computation for LTL$_{f}$. We present here two generic approaches NaiveMUC and BinaryMUC to compute an MUC for LTL$_{f}$. Moreover, we introduce heuristics that are based on the Boolean unsatisfiable core (UC) technique to accelerate the two approaches, which are named NaiveMUC+UC and BinaryMUC+UC, respectively. In particular, for global LTL$_{f}$ formulas, we show that the MUC computation can be reduced to the pure Boolean MUC computation, which therefore conducts the GlobalMUC approach. Our experiments show that GlobalMUC performs the best to compute an MUC for global formulas, and BinaryMUC+UC is the best for an arbitrary unsatisfiable formula.<\/jats:p>","DOI":"10.1093\/logcom\/exad049","type":"journal-article","created":{"date-parts":[[2023,8,7]],"date-time":"2023-08-07T03:06:37Z","timestamp":1691377597000},"page":"1274-1294","source":"Crossref","is-referenced-by-count":0,"title":["Computing minimal unsatisfiable core for LTL over finite traces"],"prefix":"10.1093","volume":"34","author":[{"given":"Tong","family":"Niu","sequence":"first","affiliation":[{"name":"Software Engineering , East China Normal University, Shanghai 200062,","place":["China"]}]},{"given":"Shengping","family":"Xiao","sequence":"additional","affiliation":[{"name":"Software Engineering , East China Normal University, Shanghai 200062,","place":["China"]}]},{"given":"Xiaoyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"Software Engineering , East China Normal University, Shanghai 200062,","place":["China"]}]},{"given":"Jianwen","family":"Li","sequence":"additional","affiliation":[{"name":"East China Normal University , Shanghai Key Laboratory of Trustworthy Computing"}]},{"given":"Yanhong","family":"Huang","sequence":"additional","affiliation":[{"name":"East China Normal University , National Trusted Embedded Software Engineering Technology Research Center"}]},{"given":"Jianqi","family":"Shi","sequence":"additional","affiliation":[{"name":"East China Normal University , National Trusted Embedded Software Engineering Technology Research Center"}]}],"member":"286","published-online":{"date-parts":[[2023,8,4]]},"reference":[{"key":"2024102321261963400_ref1","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1018985923441","article-title":"Planning for temporally extended goals","volume":"22","author":"Bacchus","year":"1998","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2024102321261963400_ref2","first-page":"9766","article-title":"Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications","volume-title":"The Thirty-Fourth AAAI Conference on Artificial Intelligence","author":"Bansal","year":"2020"},{"key":"2024102321261963400_ref3","doi-asserted-by":"crossref","first-page":"123","DOI":"10.3233\/SAT190094","article-title":"Muser2: an efficient mus extractor","volume":"8","author":"Belov","year":"2012","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"2024102321261963400_ref4","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Computing Surveys"},{"key":"2024102321261963400_ref5","first-page":"593","article-title":"Reasoning about actions and planning in LTL action theories","volume-title":"Principles of Knowledge Representation and Reasoning","author":"Calvanese","year":"2002"},{"key":"2024102321261963400_ref6","article-title":"Bridging the gap between LTL synthesis and automated planning","volume-title":"Technical Report","author":"Camacho","year":"2017"},{"key":"2024102321261963400_ref7","doi-asserted-by":"crossref","first-page":"532","DOI":"10.1007\/978-3-540-73368-3_53","article-title":"Boolean abstraction for temporal logic satisfiability","volume-title":"Proc. 15th Int\u2019l Conf. On Computer Aided Verification","author":"Cimatti","year":"2007"},{"key":"2024102321261963400_ref8","first-page":"1027","article-title":"Reasoning on LTL on finite traces: insensitivity to infiniteness","volume-title":"AAAI","author":"De Giacomo","year":"2014"},{"key":"2024102321261963400_ref9","first-page":"2000","article-title":"Linear temporal logic and linear dynamic logic on finite traces","volume-title":"IJCAI","author":"De Giacomo","year":"2013"},{"key":"2024102321261963400_ref10","first-page":"226","article-title":"Automata-theoretic approach to planning for temporally extended goals","volume-title":"Proc. European Conf. On Planning","author":"De Giacomo","year":"1999"},{"key":"2024102321261963400_ref11","doi-asserted-by":"crossref","DOI":"10.1609\/icaps.v31i1.15954","article-title":"Compositional approach to translate ltlf\/ldlf into deterministic finite automata","volume-title":"Proceedings of the International Conference on Automated Planning and Scheduling (ICAPS)","author":"De Giacomo","year":"2021"},{"key":"2024102321261963400_ref12","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1145\/3238147.3238220","article-title":"A genetic algorithm for goal-conflict identification","volume-title":"Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering","author":"Degiovanni","year":"2018"},{"key":"2024102321261963400_ref13","first-page":"507","article-title":"Goal-conflict detection based on temporal satisfiability checking","volume-title":"In 2016 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Degiovanni","year":"2016"},{"key":"2024102321261963400_ref14","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1016\/j.is.2016.09.005","article-title":"Resolving inconsistencies and redundancies in declarative process models","volume":"64","author":"Di Ciccio","year":"2017","journal-title":"Information Systems"},{"key":"2024102321261963400_ref15","first-page":"502","article-title":"An extensible SAT-solver","volume-title":"Sat","author":"E\u00e9n","year":"2003"},{"key":"2024102321261963400_ref16","first-page":"146","article-title":"Consistency-based diagnosis of configuration knowledge bases","volume-title":"Proceedings of the 14th European Conference on Artificial Intelligence, ECAI\u201900","author":"Felfernig","year":"2000"},{"key":"2024102321261963400_ref17","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/371282.371311","article-title":"Clausal temporal resolution","volume":"2","author":"Fisher","year":"2001","journal-title":"ACM Transactions on Computational Logic"},{"key":"2024102321261963400_ref18","doi-asserted-by":"crossref","first-page":"3292","DOI":"10.24963\/ijcai.2022\/359","article-title":"Ltlf synthesis as and-or graph search: knowledge compilation at work","volume-title":"Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence","author":"De Giacomo","year":"2022"},{"article-title":"Finding minimal unsatisfiable subsets in linear temporal logic using bdds","year":"2013","author":"Gor\u00e9","key":"2024102321261963400_ref19"},{"article-title":"On the complexity of computing minimal unsatisfiable LTL formulas","year":"2012","author":"Hantry","key":"2024102321261963400_ref20"},{"key":"2024102321261963400_ref21","first-page":"274","article-title":"Trp++ 2.0: a temporal resolution prover","volume-title":"Proc. CADE-19, LNAI","author":"Hustadt","year":"2003"},{"key":"2024102321261963400_ref22","first-page":"167","article-title":"Quickxplain: preferred explanations and relaxations for over-constrained problems","volume-title":"AAAI Conference on Artificial Intelligence, AAAI\u201904","author":"Junker","year":"2004"},{"key":"2024102321261963400_ref23","first-page":"2946","article-title":"Sat-based explicit ltlf satisfiability checking","volume-title":"The Thirty-Third AAAI Conference on Artificial Intelligence","author":"Li","year":"2019"},{"key":"2024102321261963400_ref24","first-page":"91","article-title":"$LTL_f$ satisfibility checking","volume-title":"ECAI","author":"Li","year":"2014"},{"key":"2024102321261963400_ref25","first-page":"209","article-title":"SAT-based explicit LTL reasoning","volume-title":"HVC","author":"Li","year":"2015"},{"key":"2024102321261963400_ref26","first-page":"1","article-title":"Sat-based explicit ltl reasoning and its application to satisfiability checking","author":"Li","year":"2019","journal-title":"Formal Methods in System Design"},{"key":"2024102321261963400_ref27","doi-asserted-by":"crossref","first-page":"1473","DOI":"10.1109\/ICSE43902.2021.00132","article-title":"How to identify boundary conditions with contrasty metric","volume-title":"2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE)","author":"Luo","year":"2021"},{"key":"2024102321261963400_ref28","first-page":"2003","article-title":"Computing infinite plans for LTL goals using a classical planner","volume-title":"IJCAI","author":"Patrizi","year":"2011"},{"key":"2024102321261963400_ref29","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1109\/SFCS.1977.32","article-title":"The temporal logic of programs","volume-title":"18th Annual Symposium on Foundations of Computer Science (Sfcs 1977)","author":"Pnueli","year":"1977"},{"article-title":"Computing unsatisfiable cores for ltlf specifications","year":"2022","author":"Roveri","key":"2024102321261963400_ref30"},{"key":"2024102321261963400_ref31","doi-asserted-by":"crossref","first-page":"908","DOI":"10.1016\/j.scico.2010.11.004","article-title":"Towards a notion of unsatisfiable and unrealizable cores for ltl","volume":"77","author":"Schuppan","year":"2012","journal-title":"Science of Computer Programming"},{"key":"2024102321261963400_ref32","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/TIME.2013.15","article-title":"Extracting unsatisfiable cores for ltl via temporal resolution","volume-title":"2013 20th International Symposium on Temporal Representation and Reasoning","author":"Schuppan","year":"2013"},{"key":"2024102321261963400_ref33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/APSEC51365.2020.00008","article-title":"Sat-based automata construction for ltl over finite traces","volume-title":"2020 27th Asia-Pacific Software Engineering Conference (APSEC)","author":"Shi","year":"2020"},{"key":"2024102321261963400_ref34","first-page":"5599","article-title":"Partitioning techniques in ltlf synthesis","volume-title":"Proceedings of the 28th International Joint Conference on Artificial Intelligence, IJCAI 19","author":"Tabajara","year":"2019"},{"key":"2024102321261963400_ref35","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/978-3-540-68237-0_23","article-title":"Finding minimal unsatisfiable cores of declarative specifications","volume-title":"FM 2008: Formal Methods","author":"Torlak","year":"2008"},{"key":"2024102321261963400_ref36","first-page":"466","volume-title":"On the Complexity of Derivation in Propositional Calculus","author":"Tseitin","year":"1983"},{"key":"2024102321261963400_ref37","doi-asserted-by":"crossref","first-page":"908","DOI":"10.1109\/32.730542","article-title":"Managing conflicts in goal-driven requirements engineering","volume":"24","author":"Van Lamsweerde","year":"1998","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2024102321261963400_ref38","first-page":"6530","article-title":"On the fly synthesis for ltl over finite traces","volume-title":"The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2021, February 7\u201312, 2021","author":"Xiao","year":"2021"},{"key":"2024102321261963400_ref39","first-page":"3088","article-title":"Ltl $f$ synthesis with fairness and stability assumptions","volume-title":"The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, New York, NY, USA, February 7\u201312, 2020","author":"Zhu","year":"2020"},{"key":"2024102321261963400_ref40","first-page":"684","article-title":"First-order vs. second-order encodings for ltlf-to-automata translation","volume-title":"Theory and Applications of Models of Computation\u201415th Annual Conference, TAMC 2019, Kitakyushu, Japan, April 13\u201316, 2019, Proceedings","author":"Zhu","year":"2019"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/34\/7\/1274\/59997667\/exad049.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/34\/7\/1274\/59997667\/exad049.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T21:26:35Z","timestamp":1729718795000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/34\/7\/1274\/7236710"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,4]]},"references-count":40,"journal-issue":{"issue":"7","published-online":{"date-parts":[[2023,8,4]]},"published-print":{"date-parts":[[2024,10,23]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exad049","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2024,10]]},"published":{"date-parts":[[2023,8,4]]}}}