Towards certified model checking for PLTL using one-pass tableaux

DOI10.4230/LIPICS.TIME.2019.12MaRDI QIDQ6487556zbMATH OpenFDO

Authors Alex Abuin, Alexander Bolotov, De Cerio Unai Díaz, M. Hermo, P. Lucio

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPICS.TIME.2019.12

zbMATH Keywords

certified model checkingexpressivenessfairnesslinear timetemporal logic

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1798181
• scientific article; zbMATH DE number 1189110
• One-Pass Tableaux for Computation Tree Logic
• Certifying proofs for SAT-based model checking
• A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL

Cited in

(4)

• Partitioned PLTL model-checking for refined transition systems
• Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
• MTL and TPTL for One-Counter Machines
• One-pass Context-based Tableaux Systems for CTL and ECTL

This page was built for publication: Towards certified model checking for PLTL using one-pass tableaux

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