PPTL\_SPIN: a SPIN based model checker for propositional projection temporal logic

DOI10.1007/978-3-319-31220-0_14MaRDI QIDQ2026564zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 20 May 2021

Full work available at URL https://doi.org/10.1007/978-3-319-31220-0_14

zbMATH Keywords

Büchi automatamodel checkingpropositional projection temporal logicSPINverification

Mathematics Subject Classification ID

Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A symbolic model checker for propositional projection temporal logic
• Bounded model checking for propositional projection temporal logic
• A canonical form based decision procedure and model checking approach for propositional projection temporal logic
• Checking satisfiability of two-dimensional logic PPTL\(^{\mathrm{SL}}\)
• An efficient decision procedure for propositional projection temporal logic

Cited in

(7)

• PPTL specification mining based on LNFG
• Temporal logic specification mining of programs
• scientific article; zbMATH DE number 1670559 (Why is no real title available?)
• Checking satisfiability of two-dimensional logic PPTL\(^{\mathrm{SL}}\)
• A symbolic model checker for propositional projection temporal logic
• Bounded model checking for propositional projection temporal logic
• PPTL_SPIN

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: PPTL\_SPIN: a SPIN based 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 Q2026564)