\(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers

DOI10.1016/j.ic.2020.104642OpenAlexW3095063913MaRDI QIDQ821566

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-checkingtemporal logicsQBF solversquantified CTL

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• MiniSat
• z3
• CESAR
• CaDiCaL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Augmenting ATL with strategy contexts
• Quantified computation tree logic
• Circuit-based search space pruning in QBF
• 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. Proceedings
• Quantified CTL: Expressiveness and Model Checking
• Quantified CTL: Expressiveness and Complexity
• Augmenting branching temporal logics with existential quantification over atomic propositions
• Modal logics of sabotage revisited
• Relation-changing modal operators: Fig. 1.
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Theory and Applications of Satisfiability Testing
• Mathematical Foundations of Computer Science 2003
• Theory and Applications of Satisfiability Testing
• Mechanizing Mathematical Reasoning