A symbolic model checker for propositional projection temporal logic

DOI10.13328/J.CNKI.JOS.004689MaRDI QIDQ3461297zbMATH OpenFDO

Authors Tao Pang, Zhenhua Duan, Xiaofang Liu

Publication date 15 January 2016

Full work available at URL https://doi.org/10.13328/J.CNKI.JOS.004689

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)

• 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
• Symbolic model checking for alternating projection temporal logic
• Bounded model checking for propositional projection temporal logic
• Bounded model checking of traffic light control system
• Model checking open systems with alternating projection temporal logic

Describes a project that uses

Uses Software

• PLSMC
• CUDD
• NuSMV

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)