Document Open Access Logo

Model Checking Linear Temporal Properties on Polyhedral Systems

Authors Massimo Benerecetti , Marco Faella , Fabio Mogavero

PDF
Thumbnail PDF

File

LIPIcs.TIME.2024.19.pdf
  • Filesize: 1 MB
  • 23 pages

Document Identifiers

Author Details

Massimo Benerecetti
  • Università di Napoli Federico II, Italy
Marco Faella
  • Università di Napoli Federico II, Italy
Fabio Mogavero
  • Università di Napoli Federico II, Italy

Funding

PNRR MUR project PE0000013-FAIR and Indam GNCS 2024 project "Certificazione, Monitoraggio, ed Interpretabilità in Sistemi di Intelligenza Artificiale". The authors are members of the Gruppo Nazionale Calcolo Scientifico-Istituto Nazionale di Alta Matematica (GNCS-INdAM).

Cite AsGet BibTex

Massimo Benerecetti, Marco Faella, and Fabio Mogavero. Model Checking Linear Temporal Properties on Polyhedral Systems. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.TIME.2024.19

Abstract

We study the problem of model checking linear temporal logic formulae on finite trajectories generated by polyhedral differential inclusions, thus enriching the landscape of models where such specifications can be effectively verified. Each model in the class comprises a static and a dynamic component. The static component features a finite set of observables represented by (non-necessarily convex) polyhedra. The dynamic one is given by a convex polyhedron constraining the dynamics of the system, by specifying the possible slopes of the trajectories in each time instant. We devise an exact algorithm that computes a symbolic representation of the region of points that existentially satisfy a given formula φ, i.e., the points from which there exists a trajectory satisfying φ.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Model Checking
  • Real-Time Systems
  • LTLf
  • RTLf

Metrics

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

References

  1. R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  2. R. Alur, T. Feder, and T.A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM (JACM), 43(1):116-146, 1996. URL: https://doi.org/10.1145/227595.227602.
  3. R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng., 22:181-201, March 1996. URL: https://doi.org/10.1109/32.489079.
  4. R. Alur, A. Trivedi, and D. Wojtczak. Optimal scheduling for constant-rate multi-mode systems. In Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, pages 75-84, 2012. Google Scholar
  5. R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 72(1-2):3-21, 2008. URL: https://doi.org/10.1016/j.scico.2007.08.001.
  6. M. Benerecetti and M. Faella. Automatic synthesis of switching controllers for linear hybrid systems: Reachability control. ACM Trans. on Embedded Computing Systems, 16(4), 2017. URL: https://doi.org/10.1145/3047500.
  7. M. Benerecetti, M. Faella, and S. Minopoli. Automatic synthesis of switching controllers for linear hybrid systems: Safety control. Theoretical Computer Science, 493:116-138, 2013. URL: https://doi.org/10.1016/J.TCS.2012.10.042.
  8. M. Blondin, P. Offtermatt, and A. Sansfaçon-Buchanan. Verifying linear temporal specifications of constant-rate multi-mode systems. In LICS, pages 1-13, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175721.
  9. E. Davis. Infinite loops in finite time: Some observations. In Proc. of the 3rd Int. Conf. on Principles of Knowledge Representation and Reasoning (KR'92). Cambridge, MA, USA, October 25-29, 1992, pages 47-58. Morgan Kaufmann, 1992. Google Scholar
  10. G. De Giacomo and M.Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pages 854-860. IJCAI/AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997.
  11. A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu. Spot 2.0—a framework for ltl and-automata manipulation. In International Symposium on Automated Technology for Verification and Analysis, pages 122-129. Springer, 2016. Google Scholar
  12. G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. Spaceex: Scalable verification of hybrid systems. In CAV 11: Proc. of 23rd Conf. on Computer Aided Verification, pages 379-395, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_30.
  13. T.A. Henzinger. The theory of hybrid automata. In 11th IEEE Symp. Logic in Comp. Sci., pages 278-292, 1996. URL: https://doi.org/0.1109/LICS.1996.561342.
  14. T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? J. of Computer and System Sciences, 57(1):94-124, 1998. URL: https://doi.org/10.1006/jcss.1998.1581.
  15. M. Kloetzer and C. Belta. A fully automated framework for control of linear systems from temporal logic specifications. IEEE Transactions on Automatic Control, 53(1):287-297, 2008. URL: https://doi.org/10.1109/TAC.2007.914952.
  16. R. Koymans. Specifying real-time properties with metric temporal logic. Real-time systems, 2(4):255-299, 1990. URL: https://doi.org/10.1007/BF01995674.
  17. O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pages 152-166. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30206-3_12.
  18. O. Maler, D. Nickovic, and A. Pnueli. Checking temporal properties of discrete, timed and continuous behaviors. Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, pages 475-505, 2008. URL: https://doi.org/10.1007/978-3-540-78127-1_26.
  19. A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  20. R. Poovendran. Cyber-physical systems: Close encounters between two parallel worlds. Proceedings of the IEEE, 98(8):1363-1366, 2010. Google Scholar
  21. M. Reynolds. The complexity of the temporal logic with “until” over general linear time. Journal of Computer and System Sciences, 66(2):393-426, 2003. URL: https://doi.org/10.1016/S0022-0000(03)00005-9.
  22. M. Reynolds. The complexity of temporal logic over the reals. Annals of Pure and Applied Logic, 161(8):1063-1096, 2010. URL: https://doi.org/10.1016/J.APAL.2010.01.002.
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