Towards certified model checking for PLTL using one-pass tableaux

DOI10.4230/LIPICS.TIME.2019.12zbMath1515.68171MaRDI QIDQ6487556

De Cerio Unai Díaz, Alexander Bolotov, Paqui Lucio, Alex Abuin, Montserrat Hermo

Publication date: 3 February 2023

zbMATH Keywords

fairnesstemporal logicexpressivenesslinear timecertified model checking

Mathematics Subject Classification ID

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

Related Items (2)

One-pass Context-based Tableaux Systems for CTL and ECTL ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models

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