A symbolic model checker for propositional projection temporal logic

DOI10.13328/J.CNKI.JOS.004689zbMATH Open1340.68048MaRDI QIDQ3461297FDOQ3461297

Authors: Tao Pang, Zhenhua Duan, Xiaofang Liu 

Publication date: 15 January 2016

Recommendations

• PPTL\_SPIN: a SPIN based model checker for propositional projection temporal logic
• Bounded model checking for propositional projection temporal logic
• Symbolic model checking for alternating projection temporal logic
• A canonical form based decision procedure and model checking approach for propositional projection temporal logic
• Expressiveness of propositional projection temporal logic with star

zbMATH Keywords

temporal logicsymbolic model checkingmodel checkerembedded system verification

Mathematics Subject Classification ID

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

Cited In (7)

• Model checking of pushdown systems for projection temporal logic
• PPTL\_SPIN: a SPIN based model checker for propositional projection temporal logic
• Linear temporal logic symbolic model checking
• Bounded model checking for propositional projection temporal logic
• Symbolic model checking for alternating projection temporal logic
• Bounded model checking of traffic light control system
• Model checking open systems with alternating projection temporal logic

Uses Software

• NuSMV
• CUDD
• PLSMC

This page was built for publication: A symbolic model checker for propositional projection temporal logic

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