Accelerating LTL satisfiability checking by SAT solvers

DOI10.1093/LOGCOM/EXY013zbMATH Open1410.68235OpenAlexW2796612952WikidataQ130117311 ScholiaQ130117311MaRDI QIDQ4612433FDOQ4612433

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

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

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)

Cited In (14)

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

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)