Document Open Access Logo

Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker

Authors Luca Geatti , Nicola Gigante , Angelo Montanari , Gabriele Venturato

PDF
Thumbnail PDF

File

LIPIcs.TIME.2021.8.pdf
  • Filesize: 1.06 MB
  • 17 pages

Document Identifiers

Author Details

Luca Geatti
  • University of Udine, Italy
  • Fondazione Bruno Kessler, Trento, Italy
Nicola Gigante
  • Free University of Bozen-Bolzano, Italy
Angelo Montanari
  • University of Udine, Italy
Gabriele Venturato
  • University of Udine, Italy
  • KU Leuven, Belgium

Acknowledgements

The open access publication of this article was supported by the Alpen-Adria-Universität Klagenfurt, Austria. Nicola Gigante acknowledges the partial support of the TOTA project "Temporal Ontologies and Tableaux Algorithms". Gabriele Venturato acknowledges the partial support of the KU Leuven Research Fund (C14/18/062).

Cite AsGet BibTex

Luca Geatti, Nicola Gigante, Angelo Montanari, and Gabriele Venturato. Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TIME.2021.8

Abstract

LTL+Past is the extension of Linear Temporal Logic (LTL) supporting past temporal operators. The addition of the past does not add expressive power, but does increase the usability of the language both in formal verification and in artificial intelligence, e.g., in the context of multi-agent systems. In this paper, we add the support of past operators to BLACK, a satisfiability checker for LTL based on a SAT encoding of a tree-shaped tableau system. We implement two ways of supporting the past in the tool. The first one is an equisatisfiable translation that removes the past operators, obtaining a future-only formula that can be solved with the original LTL engine. The second one extends the SAT encoding of the underlying tableau to directly support the tableau rules that deal with past operators. We describe both approaches and experimentally compare the two between themselves and with the νXmv model checker, obtaining promising results.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • SAT
  • LTL
  • LTL+Past
  • Tableaux

Metrics

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

References

  1. Matteo Bertello, Nicola Gigante, Angelo Montanari, and Mark Reynolds. Leviathan: A new LTL satisfiability checking tool based on a one-pass tree-shaped tableau. In Proc. of the 25th International Joint Conference on Artificial Intelligence, pages 950-956. IJCAI/AAAI Press, 2016. URL: http://www.ijcai.org/Abstract/16/139.
  2. Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, and Viktor Schuppan. Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci., 2(5), 2006. URL: https://doi.org/10.2168/LMCS-2(5:5)2006.
  3. Laura Bozzelli, Aniello Murano, and Loredana Sorrentino. Alternating-time temporal logics with linear past. Theor. Comput. Sci., 813:199-217, 2020. URL: https://doi.org/10.1016/j.tcs.2019.11.028.
  4. Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, and Roberto Sebastiani. The MathSAT 4 SMT Solver. In Computer Aided Verification, LNCS, pages 299-303. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70545-1_28.
  5. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuXmv Symbolic Model Checker. In Computer Aided Verification, pages 334-342. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_22.
  6. Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Verifying LTL Properties of Hybrid Systems with K-Liveness. In Computer Aided Verification, LNCS, pages 424-440. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_28.
  7. Alessandro Cimatti, Marco Roveri, and Daniel Sheridan. Bounded Verification of Past LTL. In Formal Methods in Computer-Aided Design, LNCS, pages 245-259. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30494-4_18.
  8. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8.
  9. Michael Fisher. A resolution method for temporal logic. In John Mylopoulos and Raymond Reiter, editors, Proceedings of the 12th International Joint Conference on Artificial Intelligence, pages 99-104. Morgan Kaufmann, 1991. Google Scholar
  10. Michael Fisher. A normal form for temporal logics and its applications in theorem-proving and execution. J. Log. Comput., 7(4):429-456, 1997. URL: https://doi.org/10.1093/logcom/7.4.429.
  11. Michael Fisher, Dov M. Gabbay, and Lluís Vila, editors. Handbook of Temporal Reasoning in Artificial Intelligence, volume 1 of Foundations of Artificial Intelligence. Elsevier, 2005. URL: http://cgi.csc.liv.ac.uk/%7Emichael/handbook.html.
  12. Luca Geatti, Nicola Gigante, and Angelo Montanari. A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL. In Proc. of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 11714 of LNCS, pages 3-20. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29026-9_1.
  13. Luca Geatti, Nicola Gigante, Angelo Montanari, and Mark Reynolds. One-pass and tree-shaped tableau systems for TPTL and TPTLsubscriptb+Past. Information and Computation, 2021. in press. URL: https://doi.org/10.1016/j.ic.2020.104599.
  14. Ullrich Hustadt and Boris Konev. TRP++2.0: A Temporal Resolution Prover. In Proc. of the 19th International Conference on Automated Deduction, pages 274-278, 2003. Google Scholar
  15. Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi A. Junttila. Simple is better: Efficient bounded model checking for past LTL. In Proc. of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS, pages 380-395. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-30579-8_25.
  16. Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, and Jifeng He. Aalta: an LTL satisfiability checker over infinite/finite traces. In Proc. of the 22nd ACM International Symposium on Foundations of Software Engineering, pages 731-734. ACM, 2014. URL: https://doi.org/10.1145/2635868.2661669.
  17. Orna Lichtenstein and Amir Pnueli. Propositional Temporal Logics: Decidability and Completeness. Logic Journal of the IGPL, 8(1):55-85, 2000. URL: https://doi.org/10.1093/jigpal/8.1.55.
  18. Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. The Glory of the Past. In Proc. of the 1st Conference on Logics of Programs, volume 193 of LNCS, pages 196-218. Springer, 1985. URL: https://doi.org/10.1007/3-540-15648-8_16.
  19. Nicolas Markey. Temporal logic with past is exponentially more succinct. Bulletin of the EATCS, 79:122-128, 2003. Google Scholar
  20. Amir Pnueli. The Temporal Logic of Programs. In Proc. of the 18th Annual Symposium on Foundations of Computer Science, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  21. Mark Reynolds. More Past Glories. In Proc. of the 15th Annual IEEE Symposium on Logic in Computer Science, pages 229-240. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/LICS.2000.855772.
  22. Mark Reynolds. A New Rule for LTL Tableaux. In Proc. of the 7superscriptth International Symposium on Games, Automata, Logics and Formal Verification, volume 226 of EPTCS, pages 287-301, 2016. URL: https://doi.org/10.4204/EPTCS.226.20.
  23. A. Prasad Sistla and Edmund M. Clarke. The Complexity of Propositional Linear Temporal Logics. Journal of the ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  24. Heikki Tauriainen and Keijo Heljanko. Testing LTL formula translation into Büchi automata. International Journal on Software Tools for Technology Transfer, 4(1):57-70, 2002. URL: https://doi.org/10.1007/s100090200070.
  25. G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967endash 1970, Symbolic Computation, pages 466-483. Springer, Berlin, Heidelberg, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28.
  26. Pierre Wolper. Temporal Logic Can Be More Expressive. Information and Control, 56(1/2):72-99, 1983. URL: https://doi.org/10.1016/S0019-9958(83)80051-5.
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