Document Open Access Logo

Towards Certified Model Checking for PLTL Using One-Pass Tableaux

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

PDF
Thumbnail PDF

File

LIPIcs.TIME.2019.12.pdf
  • Filesize: 1.02 MB
  • 18 pages

Document Identifiers

Author Details

Alex Abuin
  • Ikerlan Technology Research Centre, P. J. M. Arizmendiarrieta, 2 20500 Arrasate-Mondragón Gipuzkoa, Spain
Alexander Bolotov
  • University of Westminster, W1W 6UW, London, UK
Unai Díaz de Cerio
  • Ikerlan Technology Research Centre, P. J. M. Arizmendiarrieta, 2 20500 Arrasate-Mondragón Gipuzkoa, Spain
Montserrat Hermo
  • University of the Basque Country, P. Manuel de Lardizabal, 1, 20018-San Sebastián, Spain
Paqui Lucio
  • University of the Basque Country, P. Manuel de Lardizabal, 1, 20018-San Sebastián, Spain.

Funding

  • Bolotov, Alexander: This author has been partially supported by the UK Knowledge Transfer Partnership KTP011063 Lumina Learning & University of Westminster, and the Spanish Project TIN2017- 86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182.
  • Hermo, Montserrat: This author has been partially supported by Spanish Project TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182.
  • Lucio, Paqui: This author has been partially supported by Spanish Project TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182.

Cite AsGet BibTex

Alex Abuin, Alexander Bolotov, Unai Díaz de Cerio, Montserrat Hermo, and Paqui Lucio. Towards Certified Model Checking for PLTL Using One-Pass Tableaux. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TIME.2019.12

Abstract

The standard model checking setup analyses whether the given system specification satisfies a dedicated temporal property of the system, providing a positive answer here or a counter-example. At the same time, it is often useful to have an explicit proof that certifies the satisfiability. This is exactly what the certified model checking (CMC) has been introduced for. The paper argues that one-pass (context-based) tableau for PLTL can be efficiently used in the CMC setting, emphasising the following two advantages of this technique. First, the use of the context in which the eventualities occur, forces them to fulfil as soon as possible. Second, a dual to the tableau sequent calculus can be used to formalise the certificates. The combination of the one-pass tableau and the dual sequent calculus enables us to provide not only counter-examples for unsatisfied properties, but also proofs for satisfied properties that can be checked in a proof assistant. In addition, the construction of the tableau is enriched by an embedded solver, to which we dedicate those (propositional) computational tasks that are costly for the tableaux rules applied solely. The combination of the above techniques is particularly helpful to reason about large (system) specifications.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Temporal logic
  • fairness
  • expressiveness
  • linear-time
  • Certified model checking

Metrics

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

References

  1. Hasan Amjad. Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. In Theorem Proving in Higher Order Logics, pages 171-187. Springer Berlin Heidelberg, 2003. URL: https://doi.org/10.1007/10930755_11.
  2. Mordechai Ben-Ari. Mathematical Logic for Computer Science. Springer-Verlag, London, 2012. URL: https://doi.org/10.1007/978-1-4471-4129-7.
  3. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, and Yunshan Zhu. Symbolic Model Checking Using SAT Procedures Instead of BDDs. In Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, DAC '99, pages 317-320, New York, NY, USA, 1999. ACM. URL: https://doi.org/10.1145/309847.309942.
  4. Armin Biere and Daniel Kröning. SAT-based model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 277-303. Springer International Publishing, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_10.
  5. Alexander Bolotov, Montserrat Hermo, and Paqui Lucio. Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach. In Natasha Alechina, Kjetil Nørvåg, and Wojciech Penczek, editors, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018), volume 120 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:22, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TIME.2018.5.
  6. Kai Brünnler and Martin Lange. Cut-free sequent systems for temporal logic. The Journal of Logic and Algebraic Programming, 76(2):216-225, 2008. URL: https://doi.org/10.1016/j.jlap.2008.02.004.
  7. CENELEC and EN50128. 50128. Railway applications-Communication, Signaling and Processing Systems-Software for Railway Control and Protection Systems, 2011. Google Scholar
  8. Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, and Marco Roveri. NUSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4):410-425, March 2000. URL: https://doi.org/10.1007/s100090050046.
  9. Koen Claessen and Niklas Sörensson. A liveness checking algorithm that counts. In Gianpiero Cabodi and Satnam Singh, editors, Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, pages 52-59. IEEE, 2012. Google Scholar
  10. Edmund M. Clarke and E. Allen Emerson. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, pages 52-71, 1981. URL: https://doi.org/10.1007/BFb0025774.
  11. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999. Google Scholar
  12. Marco Comini, Laura Titolo, and Alicia Villanueva. Abstract Diagnosis for tccp using a Linear Temporal Logic. Theory and Practice of Logic Programming, 14(4-5):787-801, 2014. URL: https://doi.org/10.1017/S1471068414000349.
  13. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A Fully Verified Executable LTL Model Checker. In Computer Aided Verification, pages 463-478. Springer Berlin Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_31.
  14. Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro, and Fernando Orejas. A Cut-Free and Invariant-Free Sequent Calculus for PLTL. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 481-495. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_36.
  15. Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro, and Fernando Orejas. Dual Systems of Tableaux and Sequents for PLTL. The Journal of Logic and Algebraic Programming, 78(8):701-722, 2009. URL: https://doi.org/10.1016/j.jlap.2009.05.001.
  16. Rajeev Goré. Tableau Methods for Modal and Temporal Logics. In Marcello D'Agostino, Dov M. Gabbay, Reiner Hähnle, and Joachim Posegga, editors, Handbook of Tableau Methods, pages 297-396. Springer Netherlands, Dordrecht, 1999. URL: https://doi.org/10.1007/978-94-017-1754-0_6.
  17. Alberto Griggio, Marco Roveri, and Stefano Tonetta. Certifying Proofs for LTL Model Checking. In Formal Methods in Computer-Aided Design, FMCAD 2018, Austin, USA, pages 1-9, October 2018. URL: https://doi.org/10.23919/FMCAD.2018.8603022.
  18. IEC. IEC 61508 Functional safety of electrical/electronic/programmable electronic safety-related systems, 2010. Google Scholar
  19. ISO. Road vehicles - Functional safety, 2011. Google Scholar
  20. Henry Kautz and Bart Selman. Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search. In Proceedings of the Thirteenth National Conference on Artificial Intelligence - Volume 2, AAAI'96, pages 1194-1201. AAAI Press, 1996. URL: http://dl.acm.org/citation.cfm?id=1864519.1864564.
  21. Jörg Kreiker, Andrzej Tarlecki, Moshe Y. Vardi, and Reinhard Wilhelm. Modeling, Analysis, and Verification - The Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482). Dagstuhl Manifestos, 1(1):21-40, 2011. URL: https://doi.org/10.4230/DagMan.1.1.21.
  22. Tuomas Kuismin and Keijo Heljanko. Increasing Confidence in Liveness Model Checking Results with Proofs. In Valeria Bertacco and Axel Legay, editors, Hardware and Software: Verification and Testing, pages 32-43. Springer International Publishing, 2013. Google Scholar
  23. Orna Kupferman and Moshe Y. Vardi. From complementation to certification. Theoretical Computer Science, 345(1):83-100, 2005. URL: https://doi.org/10.1007/978-3-540-24730-2_43.
  24. Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y Vardi, and Jifeng He. Accelerating LTL satisfiability checking by SAT solvers. Journal of Logic and Computation, 28(6):1011-1030, April 2018. URL: https://doi.org/10.1093/logcom/exy013.
  25. Jianwen Li, Shufang Zhu, Geguang Pu, Lijun Zhang, and Moshe Y. Vardi. SAT-based explicit LTL reasoning and its application to satisfiability checking. Formal Methods in System Design, January 2019. URL: https://doi.org/10.1007/s10703-018-00326-5.
  26. Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, Berlin, Heidelberg, 1992. URL: https://doi.org/10.1007/978-1-4612-0931-7.
  27. Daniel Matichuk, Toby Murray, and Makarius Wenzel. Eisbach: A Proof Method Language for Isabelle. Journal of Automated Reasoning, 56, January 2016. URL: https://doi.org/10.1007/s10817-015-9360-2.
  28. Alain Mebsout and Cesare Tinelli. Proof Certificates for SMT-based Model Checkers for Infinite-state Systems. In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD '16, pages 117-124, 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886669.
  29. Kedar S. Namjoshi. Certifying Model Checkers. In Proceedings of the 13th International Conference on Computer Aided Verification, CAV '01, pages 2-13. Springer-Verlag, 2001. URL: https://doi.org/10.1007/3-540-44585-4_2.
  30. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  31. Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, pages 337-351, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-11494-7_22.
  32. Kristin Y. Rozier and Moshe Y. Vardi. LTL Satisfiability Checking. In Dragan Bošnački and Stefan Edelkamp, editors, Model Checking Software, pages 149-167, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-73370-6_11.
  33. Aravinda P. Sistla and Edmund M. Clarke. The Complexity of Propositional Linear Temporal Logics. In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC '82, pages 159-168, New York, NY, USA, 1982. ACM. URL: https://doi.org/10.1145/800070.802189.
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