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

DOI10.1016/J.TCS.2015.08.039MaRDI QIDQ896152zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 4076583 (Why is no real title available?)
• scientific article; zbMATH DE number 1361121 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 1903358 (Why is no real title available?)
• A decision procedure for propositional projection temporal logic with infinite models
• A practical decision procedure for propositional projection temporal logic with infinite models
• Bounded model checking of traffic light control system
• Complexity of propositional projection temporal logic with star
• Counterexample-guided abstraction refinement for symbolic model checking
• Expressiveness of propositional projection temporal logic with star
• Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions

Cited in

(13)

• SAT-based bounded model checking for propositional projection temporal logic
• 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
• A symbolic model checker for propositional projection temporal logic
• Bounded model checking 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

Describes a project that uses

Uses Software

• LTL2BA
• CESAR
• DART
• SPIN

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)