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

DOI10.1016/J.TCS.2015.08.039zbMATH Open1370.68200OpenAlexW1835747325MaRDI QIDQ896152FDOQ896152

Authors: Zhenhua Duan, Cong Tian, Nan Zhang 

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

Recommendations

• An efficient decision procedure for propositional projection temporal logic
• A decision procedure for propositional projection temporal logic with infinite models
• Efficient decision procedure for propositional projection temporal logic
• A practical decision procedure for propositional projection temporal logic with infinite models
• Complexity of propositional projection temporal logic with star

zbMATH Keywords

model checkinginterval temporal logicspecificationdecision procedureautomatic verificationlinear-time temporal logicpropositional projection temporal logicBüchi automata

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (12)

• An approach to agent path planning under temporal logic constraints
• PPTL\_SPIN: a SPIN based model checker for propositional projection temporal logic
• A decision procedure and complete axiomatization for projection temporal logic
• Some fixed-point issues in PPTL
• Bounded model checking for propositional projection temporal logic
• A symbolic model checker for propositional projection temporal logic
• Efficient decision procedure for propositional projection temporal logic
• An efficient decision procedure for propositional projection temporal logic
• PPTL specification mining based on LNFG
• Index set expressions can represent temporal logic formulas
• Temporal logic specification mining of programs
• Verifying a scheduling protocol of safety-critical systems

Uses Software

• SPIN
• DART
• CESAR
• LTL2BA

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

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