Accelerating LTL satisfiability checking by SAT solvers

DOI10.1093/LOGCOM/EXY013MaRDI QIDQ4612433zbMATH OpenOpenAlexWikidataFDO

Authors Jianwen Li, Geguang Pu, Moshe Y. Vardi, Jifeng He, Lijun Zhang

Publication date 31 January 2019

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/exy013

zbMATH Keywords

linear temporal logicsatisfiability checkingLTL satisfiability checkingobligation formulaSAT-based LTL satisfiability checking

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• SAT-based explicit LTL reasoning and its application to satisfiability checking
• An explicit transition system construction approach to LTL satisfiability checking
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• \(\mathrm{LTL}_{f}\) satisfiability checking
• Constraint LTL satisfiability checking without automata

Cited in

(14)

• scientific article; zbMATH DE number 5158957 (Why is no real title available?)
• SAT-based explicit LTL reasoning and its application to satisfiability checking
• scientific article; zbMATH DE number 2086516 (Why is no real title available?)
• An explicit transition system construction approach to LTL satisfiability checking
• Satisfiability checking for mission-time LTL
• \(\mathrm{LTL}_{f}\) satisfiability checking
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Simplification in a satisfiability checker for VLSI applications
• Constraint LTL satisfiability checking without automata
• Variable and clause elimination for LTL satisfiability checking
• Early verification of legal compliance via bounded satisfiability checking
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• Correct Hardware Design and Verification Methods
• scientific article; zbMATH DE number 7365811 (Why is no real title available?)

This page was built for publication: Accelerating LTL satisfiability checking by SAT solvers

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