QCTL model-checking with QBF solvers

DOI10.1016/J.IC.2020.104642MaRDI QIDQ821566zbMATH OpenOpenAlexFDO

Authors Akash Hossain, François Laroussinie

Publication date 21 September 2021

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2010.03185

zbMATH Keywords

model-checkingQBF solversquantified CTLtemporal logics

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• From quantified CTL to QBF
• Quantified CTL: expressiveness and model checking (extended abstract)
• Quantified CTL: expressiveness and complexity
• On the expressiveness of QCTL
• Quantified computation tree logic

Cites work

• Augmenting ATL with strategy contexts
• Augmenting branching temporal logics with existential quantification over atomic propositions
• Circuit-based search space pruning in QBF
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Graph theory
• scientific article; zbMATH DE number 1701362 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 2084388 (Why is no real title available?)
• scientific article; zbMATH DE number 1903357 (Why is no real title available?)
• scientific article; zbMATH DE number 7438567 (Why is no real title available?)
• Mathematical Foundations of Computer Science 2003
• Mechanizing Mathematical Reasoning
• Modal logics of sabotage revisited
• Quantified computation tree logic
• Quantified CTL: expressiveness and complexity
• Quantified CTL: expressiveness and model checking (extended abstract)
• Relation-changing modal operators
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee

Cited in

(11)

• \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
• Quantified CTL: expressiveness and model checking (extended abstract)
• Quantified CTL: expressiveness and complexity
• scientific article; zbMATH DE number 5542982 (Why is no real title available?)
• On the expressiveness of QCTL
• CAQE and QuAbS: Abstraction Based QBF Solvers
• QBF-Based Symbolic Model Checking for Knowledge and Time
• Theory and Applications of Satisfiability Testing
• From quantified CTL to QBF
• QLTL model-checking
• CSL model checking algorithms for QBDs

Describes a project that uses

Uses Software

• MiniSat
• z3
• CESAR
• CaDiCaL

This page was built for publication: \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers

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