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

DOI10.1016/J.TCS.2015.08.039MaRDI QIDQ896152zbMATHOpenAlexFDO

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

(12)

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

Describes a project that uses

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)