QLTL model-checking

DOI10.4230/LIPICS.CSL.2024.35MaRDI QIDQ6856017zbMATH OpenFDO

Authors François Laroussinie, Loriane Leclercq, Arnaud Sangnier

Publication date 19 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2024.35

zbMATH Keywords

automata theorymodel-chekingquantified linear-time temporal logicverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• Alternation
• Complete Proof System for QPTL
• Deciding full branching time logic
• scientific article; zbMATH DE number 2084388 (Why is no real title available?)
• scientific article; zbMATH DE number 2102709 (Why is no real title available?)
• scientific article; zbMATH DE number 7577569 (Why is no real title available?)
• scientific article; zbMATH DE number 2196589 (Why is no real title available?)
• Mu-calculus path checking
• Quantified CTL: expressiveness and complexity
• Taming past LTL and flat counter systems
• Temporal logic can be more expressive
• The complementation problem for Büchi automata with applications to temporal logic
• Weak Kripke structures and LTL

This page was built for publication: QLTL model-checking

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