Document Open Access Logo

RobTL: Robustness Temporal Logic for CPS

Authors Valentina Castiglioni , Michele Loreti , Simone Tini

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.15.pdf
  • Filesize: 1.08 MB
  • 23 pages

Document Identifiers

Author Details

Valentina Castiglioni
  • Eindhoven University of Technology, The Netherlands
Michele Loreti
  • University of Camerino, Italy
Simone Tini
  • University of Insubria, Italy

Funding

  • Tini, Simone: This study received funding from the European Union - Next-GenerationEU - National Recovery and Resilience Plan (NRRP) – MISSION 4 COMPONENT 2, INVESTMENT N. 1.1, CALL PRIN 2022 D.D. 104 02-02-2022 – MEDICA Project, CUP N. J53D23007180006. This publication is part of the project NODES which has received funding from the MUR – M4C2 1.5 of PNRR with grant agreement no. ECS00000036.

Cite AsGet BibTex

Valentina Castiglioni, Michele Loreti, and Simone Tini. RobTL: Robustness Temporal Logic for CPS. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.15

Abstract

We propose Robustness Temporal Logic (RobTL), a novel temporal logic for the specification and analysis of distances between the behaviours of Cyber-Physical Systems (CPS) over a finite time horizon. RobTL specifications allow us to measure the differences in the behaviours of systems with respect to various objectives and temporal constraints, and to study how those differences evolve in time. Specifically, the unique features of RobTL allow us to specify robustness properties of CPS against uncertainty and perturbations. As an example, we use RobTL to analyse the robustness of an engine system that is subject to attacks aimed at inflicting overstress of equipment.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Theory of computation → Modal and temporal logics
Keywords
  • Cyber-physical systems
  • robustness
  • temporal logic
  • uncertainty

Metrics

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

Supplementary Materials

References

  1. Alessandro Abate, Maria Prandini, John Lygeros, and Shankar Sastry. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Autom., 44(11):2724-2734, 2008. URL: https://doi.org/10.1016/J.AUTOMATICA.2008.03.027.
  2. Erika Ábrahám and Borzoo Bonakdarpour. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Proceedings of QEST 2018, volume 11024 of Lecture Notes in Computer Science, pages 20-35. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99154-2_2.
  3. Shiraj Arora, René Rydhof Hansen, Kim Guldstrand Larsen, Axel Legay, and Danny Bøgsted Poulsen. Statistical model checking for probabilistic hyperproperties of real-valued signals. In Proceedings of SPIN 2022, volume 13255 of Lecture Notes in Computer Science, pages 61-78. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15077-7_4.
  4. Christel Baier. Probabilistic model checking. In Javier Esparza, Orna Grumberg, and Salomon Sickert, editors, Dependable Software Systems Engineering, volume 45 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 1-23. IOS Press, 2016. URL: https://doi.org/10.3233/978-1-61499-627-9-1.
  5. Naama Barkai and Stanislas Leibler. Robustness in simple biochemical networks. Nature, 387:913-917, 1997. URL: https://doi.org/10.1038/43199.
  6. Vladimir I. Bogachev. Measure Theory, vol. 2,. Measure Theory. Springer-Verlag, Berlin/Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-34514-5.
  7. Christos G. Cassandras, John Lygeros, and (eds.). Stochastic Hybrid Systems. Number 24 in Control Engineering. CRC Press, Boca Raton, 1st edition, 2007. URL: https://doi.org/10.1201/9781315221625.
  8. Valentina Castiglioni, Ruggero Lanotte, Michele Loreti, and Simone Tini. Evaluating the effectiveness of digital twins through statistical model checking with feedback and perturbations. In Proceedings of FMICS 2024, Lecture Notes in Computer Science. Springer, 2024. Google Scholar
  9. Valentina Castiglioni, Michele Loreti, and Simone Tini. STARK: A Software Tool for the Analysis of Robusness in the unKnown environment. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:ddfb418d5a080b8e83323a1b2c38d9f7065e2554;origin=https://github.com/quasylab/jspear;visit=swh:1:snp:8132c5d3ed79097d14de6b333de38b74741c7f2f;anchor=swh:1:rev:c6b2386d36b72ab790999d2963203b7d5aa03ce7 (visited on 2024-08-21). URL: https://github.com/quasylab/jspear/tree/working.
  10. Valentina Castiglioni, Michele Loreti, and Simone Tini. How adaptive and reliable is your program? In Proceedings of FORTE 2021, volume 12719 of LNCS, pages 60-79. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-78089-0_4.
  11. Valentina Castiglioni, Michele Loreti, and Simone Tini. A framework to measure the robustness of programs in the unpredictable environment. Log. Methods Comput. Sci., 19(3), 2023. URL: https://doi.org/10.46298/LMCS-19(3:2)2023.
  12. Valentina Castiglioni, Michele Loreti, and Simone Tini. Stark: A Software Tool for the Analysis of Robustness in the unKnown environment. In Proceedings of COORDINATION 2023, volume 13908 of Lecture Notes in Computer Science, pages 115-132. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-35361-1_6.
  13. Valentina Castiglioni, Michele Loreti, and Simone Tini. Bio-Stark: A tool for the time-point robustness analysis of biological systems. In Proceedings of CMSB 2024, Lecture Notes in Computer Science. Springer, 2024. To appear. Google Scholar
  14. Valentina Castiglioni, Michele Loreti, and Simone Tini. STARK: A tool for the analysis of CPSs robustness. Science of Computer Programming, 236:103134, 2024. URL: https://doi.org/10.1016/j.scico.2024.103134.
  15. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  16. Thomas J. DiCiccio and Bradley Efron. Bootstrap confidence intervals. Statistical Science, 11(3):189-228, 1996. URL: https://doi.org/10.1214/ss/1032280214.
  17. Alexandre Donzé, Thomas Ferrère, and Oded Maler. Efficient robust monitoring for STL. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 264-279, Berlin, Heidelberg, 2013. Springer. Google Scholar
  18. Alexandre Donzé and Oded Maler. Robust satisfaction of temporal logic over real-valued signals. In Proceedings of FORMATS 2010, volume 6246 of LNCS, pages 92-106. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15297-9_9.
  19. Bradley Efron. Bootstrap Methods: Another Look at the Jackknife. The Annals of Statistics, 7(1):1-26, 1979. URL: https://doi.org/10.1214/aos/1176344552.
  20. Bradley Efron. Nonparametric standard errors and confidence intervals. Canadian Journal of Statistics, 9(2):139-158, 1981. URL: https://doi.org/10.2307/3314608.
  21. François Fages and Aurélien Rizk. On temporal logic constraint solving for analyzing numerical data time series. Theor. Comput. Sci., 408(1):55-65, 2008. URL: https://doi.org/10.1016/j.tcs.2008.07.004.
  22. Georgios E. Fainekos and George J. Pappas. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci., 410(42):4262-4291, 2009. URL: https://doi.org/10.1016/j.tcs.2009.06.021.
  23. Olivier P. Faugeras and Ludeger Rüschendorf. Risk excess measures induced by hemi-metrics. Probability, Uncertainty and Quantitative Risk, 3:6, 2018. URL: https://doi.org/10.1186/s41546-018-0032-0.
  24. Martin Fränzle, James Kapinski, and Pavithra Prabhakar. Robustness in cyber-physical systems. Dagstuhl Reports, 6(9):29-45, 2016. Google Scholar
  25. Dieter Gollmann, Pavel Gurikov, Alexander Isakov, Marina Krotofil, Jason Larsen, and Alexander Winnicki. Cyber-Physical Systems Security: Experimental Analysis of a Vinyl Acetate Monomer Plant. In Proceedings of CPSS 2015, pages 1-12. ACM, 2015. Google Scholar
  26. Michael Grieves and John Vickers. Digital Twin: Mitigating Unpredictable, Undesirable Emergent Behavior in Complex Systems, pages 85-113. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-38756-7_4.
  27. Jianghai Hu, John Lygeros, and Shankar Sastry. Towars a theory of stochastic hybrid systems. In Proceedings of HSCC 2000, volume 1790 of LNCS, pages 160-173, 2000. URL: https://doi.org/10.1007/3-540-46430-1_16.
  28. Hiroaki Kitano. Towards a theory of biological robustness. Molecular Systems Biology, 3(1):137, 2007. URL: https://doi.org/10.1038/msb4100179.
  29. Stephen Cole Kleene. Introduction to Metamathematics. Princeton, NJ, USA: North Holland, 1952. URL: https://doi.org/10.2307/2268620.
  30. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Stochastic model checking. In Proceedings of SFM 2007, volume 4486 of LNCS, pages 220-270. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72522-0_6.
  31. Ruggero Lanotte, Massimo Merro, Andrei Munteanu, and Simone Tini. Formal impact metrics for cyber-physical attacks. In Proceedings of CSF 2021, pages 1-16. IEEE, 2021. URL: https://doi.org/10.1109/CSF51468.2021.00040.
  32. Lucia Nasti, Roberta Gori, and Paolo Milazzo. Formalizing a notion of concentration robustness for biochemical networks. In Proceedings of STAF 2018, volume 11176 of LNCS, pages 81-97. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-04771-9_8.
  33. Nicola Paoletti, Kin Sum Liu, Hongkai Chen, Scott A. Smolka, and Shan Lin. Data-driven robust control for a closed-loop artificial pancreas. IEEE ACM Trans. Comput. Biol. Bioinform., 17(6):1981-1993, 2020. URL: https://doi.org/10.1109/TCBB.2019.2912609.
  34. Svetlozar T. Rachev, Lev B. Klebanov, Stoyan V. Stoyanov, and Frank J. Fabozzi. The Methods of Distances in the Theory of Probability and Statistics. Springer, 2013. Google Scholar
  35. Ragunathan Rajkumar, Insup Lee, Lui Sha, and John A. Stankovic. Cyber-physical systems: the next computing revolution. In Proceedings of DAC 2010, pages 731-736. ACM, 2010. URL: https://doi.org/10.1145/1837274.1837461.
  36. Aurélien Rizk, Grégory Batt, François Fages, and Sylvain Soliman. A general computational method for robustness analysis with applications to synthetic gene networks. Bioinform., 25(12), 2009. URL: https://doi.org/10.1093/bioinformatics/btp200.
  37. Aurélien Rizk, Grégory Batt, François Fages, and Sylvain Soliman. Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. Theor. Comput. Sci., 412(26):2827-2839, 2011. URL: https://doi.org/10.1016/j.tcs.2010.05.008.
  38. Matthias Rungger and Paulo Tabuada. A notion of robustness for cyber-physical systems. IEEE Trans. Autom. Control., 61(8):2108-2123, 2016. Google Scholar
  39. Koushik Sen, Mahesh Viswanathan, and Gul Agha. On statistical model checking of stochastic systems. In Proceedings of CAV 2005, volume 3576 of LNCS, pages 266-280. Springer, 2005. URL: https://doi.org/10.1007/11513988_26.
  40. Ali Shahrokni and Robert Feldt. A systematic review of software robustness. Information and Software Technology, 55(1):1-17, 2013. URL: https://doi.org/10.1016/j.infsof.2012.06.002.
  41. Guy Shinar and Martin Feinberg. Structural sources of robustness in biochemical reaction networks. Science, 327(5971):1389-1391, 2010. URL: https://doi.org/10.1126/science.1183372.
  42. Guy Shinar and Martin Feinberg. Design principles for robust biochemical reaction networks: what works, what cannot work, and what might almost work. Mathe. Biosci, 231(1):39-48, 2011. URL: https://doi.org/10.1016/j.mbs.
  43. Eduardo D. Sontag. Input to State Stability: Basic Concepts and Results, pages 163-220. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-77653-6_3.
  44. Bharath K. Sriperumbudur, Kenji Fukumizu, Arthur Gretton, Bernard Schölkopf, and Gert R. G. Lanckriet. On the empirical estimation of integral probability metrics. Electronic Journal of Statistics, 6:1550-1599, 2021. URL: https://doi.org/10.1214/12-EJS722.
  45. David Thorsley and Eric Klavins. Model reduction of stochastic processes using Wasserstein pseudometrics. In 2008 American Control Conference, pages 1374-1381. IEEE, 2008. URL: https://doi.org/10.1109/ACC.2008.4586684.
  46. David Thorsley and Eric Klavins. Approximating stochastic biochemical processes with Wasserstein pseudometrics. IET Syst. Biol., 4(3):193-211, 2010. URL: https://doi.org/10.1049/iet-syb.2009.0039.
  47. Leonid N. Vaserstein. Markovian processes on countable space product describing large systems of automata. Probl. Peredachi Inf., 5(3):64-72, 1969. Google Scholar
  48. Ludovica Luisa Vissat, Michele Loreti, Laura Nenzi, Jane Hillston, and Glenn Marion. Analysis of spatio-temporal properties of stochastic systems using TSTL. ACM Trans. Model. Comput. Simul., 29(4):20:1-20:24, 2019. URL: https://doi.org/10.1145/3326168.
  49. Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir E. Dullerud. Statistical verification of PCTL using antithetic and stratified samples. Formal Methods Syst. Des., 54(2):145-163, 2019. URL: https://doi.org/10.1007/s10703-019-00339-8.
  50. Kemin Zhou and John C. Doyle. Essentials of Robust Control. Prentice-Hall, 1997. 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