A canonical form based decision procedure and model checking approach for propositional projection temporal logic

DOI10.1016/j.tcs.2015.08.039zbMath1370.68200OpenAlexW1835747325MaRDI QIDQ896152

Zhenhua Duan, Nan Zhang, Cong Tian

Publication date: 11 December 2015

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2015.08.039

zbMATH Keywords

model checkingspecificationBüchi automataautomatic verificationinterval temporal logicdecision procedurelinear-time temporal logicpropositional projection temporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (6)

Verifying a scheduling protocol of safety-critical systems ⋮ Efficient decision procedure for propositional projection temporal logic ⋮ Temporal logic specification mining of programs ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Index set expressions can represent temporal logic formulas ⋮ PPTL specification mining based on LNFG

Uses Software

• SPIN
• DART
• CESAR
• LTL2BA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A practical decision procedure for propositional projection temporal logic with infinite models
• Expressiveness of propositional projection temporal logic with star
• A decision procedure for propositional projection temporal logic with infinite models
• Bounded model checking of traffic light control system
• Counterexample-guided abstraction refinement for symbolic model checking
• Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions
• Complexity of propositional projection temporal logic with star

This page was built for publication: A canonical form based decision procedure and model checking approach for propositional projection temporal logic