Document Open Access Logo

Counterfactual Explanations for MITL Violations

Authors Bernd Finkbeiner , Felix Jahn , Julian Siber

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2024.22.pdf
  • Filesize: 1.06 MB
  • 25 pages

Document Identifiers

Author Details

Bernd Finkbeiner
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Felix Jahn
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
Julian Siber
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Funding

This work was partially supported by the DFG in project 389792660 (Center for Perspicuous Systems, TRR 248) and by the ERC Grant HYPER (No. 101055412).

Cite As Get BibTex

Bernd Finkbeiner, Felix Jahn, and Julian Siber. Counterfactual Explanations for MITL Violations. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 22:1-22:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSTTCS.2024.22

Abstract

MITL is a temporal logic that facilitates the verification of real-time systems by expressing the critical timing constraints placed on these systems. MITL specifications can be checked against system models expressed as networks of timed automata. A violation of an MITL specification is then witnessed by a timed trace of the network, i.e., an execution consisting of both discrete actions and real-valued delays between these actions. Finding and fixing the root cause of such a violation requires significant manual effort since both discrete actions and real-time delays have to be considered. In this paper, we present an automatic explanation method that eases this process by computing the root causes for the violation of an MITL specification on the execution of a network of timed automata. This method is based on newly developed definitions of counterfactual causality tailored to networks of timed automata in the style of Halpern and Pearl’s actual causality. We present and evaluate a prototype implementation that demonstrates the efficacy of our method on several benchmarks from the literature.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Modal and temporal logics
Keywords
  • Timed automata
  • actual causality
  • metric interval temporal logic

Metrics

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

Supplementary Materials

References

  1. Rajeev Alur. Timed automata. In Nicolas Halbwachs and Doron A. Peled, editors, Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings, volume 1633 of Lecture Notes in Computer Science, pages 8-22. Springer, 1999. URL: https://doi.org/10.1007/3-540-48683-6_3.
  2. Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 209-229. Springer, 1992. URL: https://doi.org/10.1007/3-540-57318-6_30.
  3. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  4. Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. The benefits of relaxing punctuality. J. ACM, 43(1):116-146, January 1996. URL: https://doi.org/10.1145/227595.227602.
  5. Uwe Aßmann, Christel Baier, Clemens Dubslaff, Dominik Grzelak, Simon Hanisch, Ardhi Putra Pratama Hartono, Stefan Köpsell, Tianfang Lin, and Thorsten Strufe. Tactile computing: Essential building blocks for the Tactile Internet, pages 293-317. Academic Press, 2021. 46.23.01; LK 01. URL: https://doi.org/10.1016/B978-0-12-821343-8.00025-3.
  6. Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer, and Robin Ziemek. From verification to causality-based explications (invited talk). In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 1:1-1:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.ICALP.2021.1.
  7. Christel Baier, Roxane van den Bossche, Sascha Klüppelholz, Johannes Lehmann, and Jakob Piribauer. Backward responsibility in transition systems using general power indices. In Michael J. Wooldridge, Jennifer G. Dy, and Sriraam Natarajan, editors, Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pages 20320-20327. AAAI Press, 2024. URL: https://doi.org/10.1609/AAAI.V38I18.30013.
  8. Thomas Ball and Orna Kupferman. Vacuity in testing. In Bernhard Beckert and Reiner Hähnle, editors, Tests and Proofs, pages 4-17, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-79124-9_2.
  9. Thomas Ball, Mayur Naik, and Sriram K. Rajamani. From symptom to cause: Localizing errors in counterexample traces. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '03, pages 97-105, New York, NY, USA, 2003. Association for Computing Machinery. URL: https://doi.org/10.1145/604131.604140.
  10. Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, and Richard Trefler. Explaining counterexamples using causality. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, pages 94-108, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02658-4_11.
  11. Ilan Beer, Shoham Ben-David, Cindy Eisner, and Yoav Rodeh. Efficient detection of vacuity in actl formulas. In Orna Grumberg, editor, Computer Aided Verification, pages 279-290, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-63166-6_28.
  12. Johan Bengtsson, Bengt Jonsson, Johan Lilius, and Wang Yi. Partial order reductions for timed systems. In Davide Sangiorgi and Robert de Simone, editors, CONCUR '98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings, volume 1466 of Lecture Notes in Computer Science, pages 485-500. Springer, 1998. URL: https://doi.org/10.1007/BFB0055643.
  13. Johan Bengtsson, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. UPPAAL - A tool suite for automatic verification of real-time systems. In Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors, Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop on Verification and Control of Hybrid Systems, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA, volume 1066 of Lecture Notes in Computer Science, pages 232-243. Springer, 1995. URL: https://doi.org/10.1007/BFB0020949.
  14. Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichstätt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned], volume 3098 of Lecture Notes in Computer Science, pages 87-124. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-27755-2_3.
  15. Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Julian Siber. Checking and sketching causes on temporal sequences. In Étienne André and Jun Sun, editors, Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part II, volume 14216 of Lecture Notes in Computer Science, pages 314-327. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-45332-8_18.
  16. Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. Updatable timed automata. Theor. Comput. Sci., 321(2-3):291-345, 2004. URL: https://doi.org/10.1016/J.TCS.2004.04.003.
  17. Georgiana Caltais, Sophie Linnea Guetlein, and Stefan Leue. Causality for general LTL-definable properties. Electronic Proceedings in Theoretical Computer Science, 286:1-15, January 2019. URL: https://doi.org/10.4204/eptcs.286.1.
  18. Hana Chockler, Joseph Y. Halpern, and Orna Kupferman. What causes a system to satisfy a specification? ACM Trans. Comput. Logic, 9(3), June 2008. URL: https://doi.org/10.1145/1352582.1352588.
  19. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and Aravinda Prasad Sistla, editors, Computer Aided Verification, pages 154-169, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/10722167_15.
  20. Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger, and Julian Siber. Explaining hyperproperty violations. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 407-429. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_20.
  21. Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Niklas Metzger, and Julian Siber. Temporal causality in reactive systems. In Ahmed Bouajjani, Lukás Holík, and Zhilin Wu, editors, Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings, volume 13505 of Lecture Notes in Computer Science, pages 208-224. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-19992-9_13.
  22. Anupam Datta, Deepak Garg, Dilsun Kaynar, Divya Sharma, and Arunesh Sinha. Program actions as actual causes: A building block for accountability. In 2015 IEEE 28th Computer Security Foundations Symposium, pages 261-275, 2015. URL: https://doi.org/10.1109/CSF.2015.25.
  23. Alexandre David and Wang Yi. Modelling and analysis of a commercial field bus protocol. In 12th Euromicro Conference on Real-Time Systems (ECRTS 2000), 19-21 June 2000, Stockholm, Sweden, Proceedings, pages 165-172. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/EMRTS.2000.854004.
  24. Henning Dierks, Sebastian Kupferschmid, and Kim Guldstrand Larsen. Automatic abstraction refinement for timed automata. In Jean-François Raskin and P. S. Thiagarajan, editors, Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings, volume 4763 of Lecture Notes in Computer Science, pages 114-129. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-75454-1_10.
  25. Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger, and Julian Siber. Synthesis of temporal causality. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III, volume 14683 of Lecture Notes in Computer Science, pages 87-111. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65633-0_5.
  26. Bernd Finkbeiner and Julian Siber. Counterfactuals modulo temporal logics. In Ruzica Piskac and Andrei Voronkov, editors, LPAR 2023: 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, June 4-9, 2023, volume 94 of EPiC Series in Computing, pages 181-204. EasyChair, 2023. URL: https://doi.org/10.29007/qtw7.
  27. Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner, and Hans-Jörg Peter. Model checking the flexray physical layer protocol. In Stefan Kowalewski and Marco Roveri, editors, Formal Methods for Industrial Critical Systems - 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010. Proceedings, volume 6371 of Lecture Notes in Computer Science, pages 132-147. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15898-8_9.
  28. Gregor Gössler and Daniel Le Métayer. A General Trace-Based Framework of Logical Causality. Research Report RR-8378, INRIA, October 2013. URL: https://inria.hal.science/hal-00873665.
  29. Gregor Gössler, Daniel Le Métayer, and Jean-Baptiste Raclet. Causality analysis in contract violation. In Howard Barringer, Ylies Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon Pace, Grigore Roşu, Oleg Sokolsky, and Nikolai Tillmann, editors, Runtime Verification, pages 270-284, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  30. Gregor Gössler, Thomas Mari, Yannick Pencolé, and Louise Travé-Massuyès. Towards Causal Explanations of Property Violations in Discrete Event Systems. In DX'19 - 30th International Workshop on Principles of Diagnosis, pages 1-8, Klagenfurt, Austria, November 2019. URL: https://inria.hal.science/hal-02369014.
  31. Alex Groce. Error explanation with distance metrics. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 108-122, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-24730-2_8.
  32. Gregor Gössler and Jean-Bernard Stefani. Causality analysis and fault ascription in component-based systems. Theoretical Computer Science, 837:158-180, 2020. URL: https://doi.org/10.1016/j.tcs.2020.06.010.
  33. Joseph Y. Halpern. A modification of the halpern-pearl definition of causality. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 3022-3033. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/427.
  34. Joseph Y. Halpern. Actual Causality. MIT Press, 2016. Google Scholar
  35. Joseph Y. Halpern and Judea Pearl. Causes and explanations: A structural-model approach. part i: Causes. The British Journal for the Philosophy of Science, 2005. Google Scholar
  36. Joseph Y. Halpern and Judea Pearl. Causes and explanations: A structural-model approach. part ii: Explanations. The British Journal for the Philosophy of Science, 2005. Google Scholar
  37. Joseph Y. Halpern and Spencer Peters. Reasoning about causal models with infinitely many variables. Proceedings of the AAAI Conference on Artificial Intelligence, 36(5):5668-5675, June 2022. URL: https://doi.org/10.1609/aaai.v36i5.20508.
  38. Mark Harman and Robert M. Hierons. An overview of program slicing. Softw. Focus, 2(3):85-92, 2001. URL: https://doi.org/10.1002/SWF.41.
  39. K. Havelund, A. Skou, K.G. Larsen, and K. Lund. Formal modeling and analysis of an audio/video protocol: an industrial case study using uppaal. In Proceedings Real-Time Systems Symposium, pages 2-13, 1997. URL: https://doi.org/10.1109/REAL.1997.641264.
  40. Tom Horak, Norine Coenen, Niklas Metzger, Christopher Hahn, Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd Finkbeiner, and Raimund Dachselt. Visual analysis of hyperproperties for understanding model checking results. IEEE Trans. Vis. Comput. Graph., 28(1):357-367, 2022. URL: https://doi.org/10.1109/TVCG.2021.3114866.
  41. Susan B. Horwitz, Thomas Reps, and Dave Binkley. Interprocedural slicing using dependence graphs. SIGPLAN Not., 23(7):35-46, June 1988. URL: https://doi.org/10.1145/960116.53994.
  42. Yatin Vasant Hoskote, Timothy Kam, Pei-Hsin Ho, and Xudong Zhao. Coverage estimation for symbolic model checking. In Mary Jane Irwin, editor, Proceedings of the 36th Conference on Design Automation, New Orleans, LA, USA, June 21-25, 1999, pages 300-305. ACM Press, 1999. URL: https://doi.org/10.1145/309847.309936.
  43. Felix Jahn. Prototype tool of our approach. URL: https://github.com/FelixJahnFJ/Real-Time-Causality-Tool.git.
  44. Felix Jahn. Real Time Causality Analysis Tool. Software, URL: https://github.com/reactive-systems/rt-causality.git (visited on 2024-10-11).
    Software Heritage Logo archived version
  45. Manu Jose and Rupak Majumdar. Cause clue clauses: error localization using maximum satisfiability. In Mary W. Hall and David A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 437-446. ACM, 2011. URL: https://doi.org/10.1145/1993498.1993550.
  46. Martin Kölbl, Stefan Leue, and Robert Schmid. Dynamic causes for the violation of timed reachability properties. In Nathalie Bertrand and Nils Jansen, editors, Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Vienna, Austria, September 1-3, 2020, Proceedings, volume 12288 of Lecture Notes in Computer Science, pages 127-143. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-57628-8_8.
  47. Martin Kölbl, Stefan Leue, and Thomas Wies. Clock bound repair for timed systems. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 79-96. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_5.
  48. Florian Leitner-Fischer and Stefan Leue. Causality checking for complex system models. In Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni, editors, Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, volume 7737 of Lecture Notes in Computer Science, pages 248-267. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-35873-9_16.
  49. David K. Lewis. Counterfactuals. Cambridge, MA, USA: Blackwell, 1973. Google Scholar
  50. Magnus Lindahl, Paul Pettersson, and Wang Yi. Formal design and analysis of a gear controller. In Bernhard Steffen, editor, Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1384 of Lecture Notes in Computer Science, pages 281-297. Springer, 1998. URL: https://doi.org/10.1007/BFB0054178.
  51. Oded Maler, Dejan Nickovic, and Amir Pnueli. From MITL to timed automata. In Eugene Asarin and Patricia Bouyer, editors, Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25-27, 2006, Proceedings, volume 4202 of Lecture Notes in Computer Science, pages 274-289. Springer, 2006. URL: https://doi.org/10.1007/11867340_20.
  52. Thomas Marix, Thao Dang, and Gregor Gössler. Explaining safety violations in real-time systems. In Catalin Dima and Mahsa Shirmohammadi, editors, Formal Modeling and Analysis of Timed Systems - 19th International Conference, FORMATS 2021, Paris, France, August 24-26, 2021, Proceedings, volume 12860 of Lecture Notes in Computer Science, pages 100-116. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-85037-1_7.
  53. Corto Mascle, Christel Baier, Florian Funke, Simon Jantsch, and Stefan Kiefer. Responsibility and verification: Importance value in temporal logics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470597.
  54. Julie Parreaux, Jakob Piribauer, and Christel Baier. Counterfactual causality for reachability and safety based on distance functions. In Antonis Achilleos and Dario Della Monica, editors, Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2023, Udine, Italy, 18-20th September 2023, volume 390 of EPTCS, pages 132-149, 2023. URL: https://doi.org/10.4204/EPTCS.390.9.
  55. Spencer Peters and Joseph Y. Halpern. Causal modeling with infinitely many variables. CoRR, abs/2112.09171, 2021. URL: https://arxiv.org/abs/2112.09171.
  56. Pyuppaal library webpage. URL: https://pypi.org/project/pyuppaal/1.0.0/.
  57. Arshia Rafieioskouei and Borzoo Bonakdarpour. Efficient discovery of actual causality using abstraction-refinement. CoRR, abs/2407.16629, 2024. URL: https://doi.org/10.48550/arXiv.2407.16629.
  58. Raymond Reiter. A theory of diagnosis from first principles. Artificial Intelligence, 32(1):57-95, 1987. URL: https://doi.org/10.1016/0004-3702(87)90062-2.
  59. Chao Wang, Zijiang Yang, Franjo Ivančić, and Aarti Gupta. Whodunit? causal analysis for counterexamples. In Susanne Graf and Wenhui Zhang, editors, Automated Technology for Verification and Analysis, pages 82-95, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  60. Shaohui Wang, Anaheed Ayoub, BaekGyu Kim, Gregor Gössler, Oleg Sokolsky, and Insup Lee. A causality analysis framework for component-based real-time systems. In Axel Legay and Saddek Bensalem, editors, Runtime Verification, pages 285-303, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-40787-1_17.
  61. Mark Weiser. Program slicing. IEEE Transactions on Software Engineering, SE-10(4):352-357, 1984. URL: https://doi.org/10.1109/TSE.1984.5010248.
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 About DROPS Imprint Privacy Contact