An explicit transition system construction approach to LTL satisfiability checking

DOI10.1007/s00165-017-0442-2zbMath1382.68142OpenAlexW2767756541MaRDI QIDQ1707341

Geguang Pu, Jifeng He, Jianwen Li, Shufang Zhu, Moshe Y. Vardi, Li-jun Zhang

Publication date: 29 March 2018

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-017-0442-2

zbMATH Keywords

LTL satisfiability checkingLTL transition systemobligation set

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• MiniSat
• SPIN
• NuSMV
• Cadence SMV
• SPOT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic model checking: \(10^{20}\) states and beyond
• NuSMV: A new symbolic model checker
• A decision procedure for propositional projection temporal logic with infinite models
• On the Relationship between LTL Normal Forms and Büchi Automata
• SAT-Based Model Checking without Unrolling
• Towards a Notion of Unsatisfiable Cores for LTL
• Graph-Based Algorithms for Boolean Function Manipulation
• The complexity of propositional linear temporal logics
• Theory and Applications of Satisfiability Testing
• Boolean Abstraction for Temporal Logic Satisfiability
• Automata-Theoretic Model Checking Revisited
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Depth-First Search and Linear Graph Algorithms
• Clausal temporal resolution
• Symbolic Implementation of Alternating Automata
• Computer Aided Verification
• Bounded model checking using satisfiability solving

This page was built for publication: An explicit transition system construction approach to LTL satisfiability checking