A symbolic model checker for propositional projection temporal logic

DOI10.13328/J.CNKI.JOS.004689MaRDI QIDQ3461297zbMATHFDO

Authors Tao Pang, Zhenhua Duan, Xiaofang Liu

Publication date 15 January 2016

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)

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

Cited in

(7)

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

Describes a project that uses

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)