SAT-based bounded model checking for propositional projection temporal logic

DOI10.1016/J.TCS.2025.115368MaRDI QIDQ6956048zbMATH OpenFDO

Authors Zhenhua Duan, Cong Tian, Nan Zhang, Chaofeng Yu, Mengfei Yang, Jia He

Publication date 21 July 2025

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.TCS.2025.115368

zbMATH Keywords

bounded model checkingpropositional projection temporal logicrate-monotonic scheduling

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Computational aspects of satisfiability (68R07)

Cites work

• A canonical form based decision procedure and model checking approach for propositional projection temporal logic
• A decision procedure for propositional projection temporal logic with infinite models
• A machine program for theorem-proving
• A proof system for unified temporal logic
• Bounded model checking for propositional projection temporal logic
• Bounded model checking using satisfiability solving
• Expressiveness of propositional projection temporal logic with star
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3651705 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 1982210 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Model Checking Security Protocols
• Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions
• PySAT: a Python toolkit for prototyping with SAT oracles
• SAT-Based Model Checking
• Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment
• Software model checking
• Symbolic model checking: \(10^{20}\) states and beyond
• Theory and Applications of Satisfiability Testing

This page was built for publication: SAT-based bounded model checking for propositional projection temporal logic

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