Computing minimal unsatisfiable core for LTL over finite traces

DOI10.1093/LOGCOM/EXAD049MaRDI QIDQ7004096zbMATH OpenFDO

Authors Tong Niu, Shengping Xiao, Xiao-Yu Zhang, Jianwen Li, Yan-Hong Huang, Jianqi Shi

Publication date 3 April 2025

Published in Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/LOGCOM/EXAD049

zbMATH Keywords

Boolean unsatisfiable corelinear temporal logic over finite tracesminimal unsatisfiable core

Mathematics Subject Classification ID

Temporal logic (03B44)

Cites work

• Boolean Abstraction for Temporal Logic Satisfiability
• Clausal temporal resolution
• First-order vs. second-order encodings for \textsc{ltl}\(_f\)-to-automata translation
• MUSer2: an efficient MUS extractor
• Planning for temporally extended goals.
• Theory and Applications of Satisfiability Testing
• Towards a notion of unsatisfiable and unrealizable cores for LTL

This page was built for publication: Computing minimal unsatisfiable core for LTL over finite traces

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7004096)