Document Open Access Logo

From Quantified CTL to QBF

Authors Akash Hossain, François Laroussinie

PDF
Thumbnail PDF

File

LIPIcs.TIME.2019.11.pdf
  • Filesize: 0.6 MB
  • 20 pages

Document Identifiers

Author Details

Akash Hossain
  • IRIF, Univ. Paris Diderot, France
François Laroussinie
  • IRIF, Univ. Paris Diderot, France

Funding

Project FREDDA ANR-17-CE40-0013

Cite AsGet BibTex

Akash Hossain and François Laroussinie. From Quantified CTL to QBF. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TIME.2019.11

Abstract

QCTL extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over Kripke structures (it is as expressive as MSO). Several semantics exist for the quantifications: here, we work with the structure semantics, where the extra propositions label the Kripke structure (and not its execution tree), and the model-checking problem is known to be PSPACE-complete in this framework. We propose a model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies, and we compare them with a prototype (based on the SMT-solver Z3) on several examples.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
Keywords
  • Model-checking
  • Quantified CTL
  • QBF solvers
  • SAT based model-checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. Bounded model checking. Advances in Computers, 58:117-148, 2003. Google Scholar
  2. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic Model Checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, volume 1579 of Lecture Notes in Computer Science, pages 193-207. Springer, 1999. Google Scholar
  3. Edmund M. Clarke and E. Allen Emerson. Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. In Dexter C. Kozen, editor, Proceedings of the 3rd Workshop on Logics of Programs (LOP'81), volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer-Verlag, 1982. Google Scholar
  4. Arnaud Da Costa, François Laroussinie, and Nicolas Markey. Quantified CTL: Expressiveness and Model Checking. In Maciej Koutny and Irek Ulidowski, editors, Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12), volume 7454 of Lecture Notes in Computer Science, pages 177-192. Springer-Verlag, September 2012. Google Scholar
  5. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Budapest, Hungary, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. Google Scholar
  6. Nachum Dershowitz, Ziyad Hanna, and Jacob Katz. Bounded Model Checking with QBF. In Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 408-414. Springer, 2005. Google Scholar
  7. Tim French. Decidability of Quantified Propositional Branching Time Logics. In Markus Stumptner, Dan Corbett, and Mike Brooks, editors, Proceedings of the 14th Australian Joint Conference on Artificial Intelligence (AJCAI'01), volume 2256 of Lecture Notes in Computer Science, pages 165-176. Springer-Verlag, December 2001. Google Scholar
  8. Tim French. Quantified Propositional Temporal Logic with Repeating States. In Proceedings of the 10th International Symposium on Temporal Representation and Reasoning and of the 4th International Conference on Temporal Logic (TIME-ICTL'03), pages 155-165. IEEE Comp. Soc. Press, July 2003. Google Scholar
  9. Orna Kupferman. Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. In Pierre Wolper, editor, Proceedings of the 7th International Conference on Computer Aided Verification (CAV'95), volume 939 of Lecture Notes in Computer Science, pages 325-338. Springer-Verlag, July 1995. Google Scholar
  10. François Laroussinie and Nicolas Markey. Quantified CTL: Expressiveness and Complexity. Logical Methods in Computer Science, 10(4), 2014. Google Scholar
  11. François Laroussinie and Nicolas Markey. Augmenting ATL with strategy contexts. Inf. Comput., 245:98-123, 2015. Google Scholar
  12. Kenneth L. McMillan. Applying SAT Methods in Unbounded Symbolic Model Checking. In Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, volume 2404 of Lecture Notes in Computer Science, pages 250-264. Springer, 2002. Google Scholar
  13. Anindya C. Patthak, Indrajit Bhattacharya, Anirban Dasgupta, Pallab Dasgupta, and P. P. Chakrabarti. Quantified Computation Tree Logic. Information Processing Letters, 82(3):123-129, 2002. Google Scholar
  14. Amir Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS'77), pages 46-57. IEEE Comp. Soc. Press, October-November 1977. Google Scholar
  15. Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, Proceedings of the 5th International Symposium on Programming (SOP'82), volume 137 of Lecture Notes in Computer Science, pages 337-351. Springer-Verlag, April 1982. Google Scholar
  16. A. Prasad Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University, Cambridge, Massachussets, USA, 1983. Google Scholar
  17. Johan van Benthem. An Essay on Sabotage and Obstruction. In Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, volume 2605 of Lecture Notes in Computer Science, pages 268-276. Springer, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact