{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:48:19Z","timestamp":1765547299682,"version":"3.40.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656323"},{"type":"electronic","value":"9783031656330"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present an automata-based algorithm to synthesize <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular causes for <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular effects on executions of a reactive system, such as counterexamples uncovered by a model checker. Our theory is a generalization of <jats:italic>temporal causality<\/jats:italic>, which has recently been proposed as a framework for drawing causal relationships between trace properties on a given trace. So far, algorithms exist only for verifying a single causal relationship and, as an extension, cause synthesis through enumeration, which is complete only for a small fragment of effect properties. This work presents the first complete cause-synthesis algorithm for the class of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular effects. We show that in this case, causes are guaranteed to be <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-regular themselves and can be computed as, e.g., nondeterministic B\u00fcchi automata. We demonstrate the practical feasibility of this algorithm with a prototype tool and evaluate its performance for cause synthesis and cause checking.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_5","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"87-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Synthesis of\u00a0Temporal Causality"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3566-0338","authenticated-orcid":false,"given":"Hadar","family":"Frenkel","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3184-6335","authenticated-orcid":false,"given":"Niklas","family":"Metzger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0842-0029","authenticated-orcid":false,"given":"Julian","family":"Siber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Baier, C., van\u00a0den Bossche, R., Kl\u00fcppelholz, S., Lehmann, J., Piribauer, J.: Backward responsibility in transition systems using general power indices. In: Wooldridge, M.J., Dy, J.G., Natarajan, S. (eds.) 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, 20-27 February 2024, Vancouver, Canada, pp. 20320\u201320327. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I18.30013","DOI":"10.1609\/AAAI.V38I18.30013"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"894","DOI":"10.1007\/978-3-030-81685-8_42","volume-title":"Computer Aided Verification","author":"C Baier","year":"2021","unstructured":"Baier, C., Coenen, N., Finkbeiner, B., Funke, F., Jantsch, S., Siber, J.: Causality-based game solving. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 894\u2013917. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_42"},{"key":"5_CR3","unstructured":"Baier, C., Dubslaff, C., Funke, F., Jantsch, S., Majumdar, R., Piribauer, J., Ziemek, R.: From Verification to Causality-Based Explications. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0198, pp. 1:1\u20131:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/14070"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., Dubslaff, C., Funke, F., Jantsch, S., Piribauer, J., Ziemek, R.: Operational causality - necessarily sufficient and sufficiently necessary. In: Jansen, N., Stoelinga, M., van\u00a0den Bos, P. (eds.) A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13560, pp. 27\u201345. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15629-8_2","DOI":"10.1007\/978-3-031-15629-8_2"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: Aiken, A., Morrisett, G. (eds.) Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, 15-17 January 2003, pp. 97\u2013105. ACM (2003). https:\/\/doi.org\/10.1145\/604131.604140","DOI":"10.1145\/604131.604140"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1007\/978-3-030-81685-8_33","volume-title":"Computer Aided Verification","author":"J Baumeister","year":"2021","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: A temporal logic for asynchronous hyperproperties. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 694\u2013717. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_33"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-642-02658-4_11","volume-title":"Computer Aided Verification","author":"I Beer","year":"2009","unstructured":"Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining counterexamples using causality. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 94\u2013108. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_11"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Beutner, R., Finkbeiner, B.: HyperATL*: A logic for hyperproperties in multi-agent systems. Log. Methods Comput. Sci. 19, 13:1\u201313:44 (2023)","DOI":"10.46298\/lmcs-19(2:13)2023"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Model checking omega-regular hyperproperties with autohyperq. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. EPiC Series in Computing, vol.\u00a094, pp. 23\u201335. EasyChair (2023). https:\/\/doi.org\/10.29007\/1XJT","DOI":"10.29007\/1XJT"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., Frenkel, H., Metzger, N.: Second-order hyperproperties. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17-22 July 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 309\u2013332. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_15","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., Frenkel, H., Siber, J.: Checking and sketching causes on temporal sequences. In: Andr\u00e9, \u00c9., Sun, J. (eds.) Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, 24-27 October 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14216, pp. 314\u2013327. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_18","DOI":"10.1007\/978-3-031-45332-8_18"},{"key":"5_CR12","unstructured":"Biere, A.: The AIGER And-Inverter Graph (AIG) format version 20071012. Tech. Rep.\u00a007\/1, Inst. f. Form. Model. u. Verifikation, Johannes Kepler University (2007)"},{"key":"5_CR13","unstructured":"Buechi, J.R.: On a decision method in restricted second-order arithmetic. In: International Congress on Logic, Methodology, and Philosophy of Science (1962)"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Caltais, G., Guetlein, S.L., Leue, S.: Causality for general LTL-definable properties. In: Workshop on Formal Reasoning About Causation, Responsibility, and Explanations in Science and Technology, CREST 2018. EPTCS, vol.\u00a0286 (2018). https:\/\/doi.org\/10.4204\/EPTCS.286.1","DOI":"10.4204\/EPTCS.286.1"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Chaki, S., Groce, A., Strichman, O.: Explaining abstract counterexamples. In: Taylor, R.N., Dwyer, M.B. (eds.) Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2004, Newport Beach, CA, USA, October 31 - November 6, 2004, pp. 73\u201382. ACM (2004). https:\/\/doi.org\/10.1145\/1029894.1029908","DOI":"10.1145\/1029894.1029908"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"5_CR17","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Coenen, N., Dachselt, R., Finkbeiner, B., Frenkel, H., Hahn, C., Horak, T., Metzger, N., Siber, J.: Explaining hyperproperty violations. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. LNCS, vol. 13371, pp. 407\u2013429. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_20","DOI":"10.1007\/978-3-031-13185-1_20"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Frenkel, H., Hahn, C., Metzger, N., Siber, J.: Temporal causality in reactive systems. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, 25-28 October 2022, Proceedings. LNCS, vol. 13505, pp. 208\u2013224. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_13","DOI":"10.1007\/978-3-031-19992-9_13"},{"key":"5_CR20","unstructured":"Cosler, M., Schmitt, F., Hahn, C., Finkbeiner, B.: Iterative circuit repair against formal specifications. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, 1-5 May 2023. OpenReview.net (2023). https:\/\/openreview.net\/pdf?id=SEcSahl0Ql"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: What\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, 7-10 August 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 174\u2013187. Springer, Cham (2022. https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Frenkel, H., Metzger, N., Siber, J.: Synthesis of temporal causality. CoRR (2024). https:\/\/doi.org\/10.48550\/ARXIV.2405.10912, https:\/\/arxiv.org\/abs\/2405.10912, full version","DOI":"10.48550\/ARXIV.2405.10912"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Siber, J.: Counterfactuals modulo temporal logics. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. EPiC Series in Computing, vol.\u00a094, pp. 181\u2013204. EasyChair (2023). https:\/\/doi.org\/10.29007\/QTW7","DOI":"10.29007\/QTW7"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-319-07602-7_11","volume-title":"Formal Aspects of Component Software","author":"G G\u00f6ssler","year":"2014","unstructured":"G\u00f6ssler, G., Le M\u00e9tayer, D.: A general trace-based framework of logical causality. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 157\u2013173. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07602-7_11"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"G\u00f6ssler, G., Stefani, J.: Causality analysis and fault ascription in component-based systems. Theor. Comput. Sci. 837 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2020.06.010","DOI":"10.1016\/j.tcs.2020.06.010"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. Int. J. Softw. Tools Technol. Transf. 8(3) (2006). https:\/\/doi.org\/10.1007\/s10009-005-0202-0","DOI":"10.1007\/s10009-005-0202-0"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-27813-9_35","volume-title":"Computer Aided Verification","author":"A Groce","year":"2004","unstructured":"Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with explain. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 453\u2013456. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_35"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Propositional dynamic logic for hyperproperties. In: International Conference on Concurrency Theory, CONCUR 2020. LIPIcs, vol.\u00a0171. Schloss Dagstuhl (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.50","DOI":"10.4230\/LIPIcs.CONCUR.2020.50"},{"key":"5_CR29","unstructured":"Halpern, J.Y.: A modification of the Halpern-pearl definition of causality. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25-31 July 2015, pp. 3022\u20133033. AAAI Press (2015). http:\/\/ijcai.org\/Abstract\/15\/427"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y.: Actual Causality. MIT Press (2016)","DOI":"10.7551\/mitpress\/10809.001.0001"},{"key":"5_CR31","unstructured":"Halpern, J.Y., Pearl, J.: Causes and explanations: a structural-model approach: Part 1: Causes. In: Breese, J.S., Koller, D. (eds.) UAI 2001: Proceedings of the 17th Conference in Uncertainty in Artificial Intelligence, University of Washington, Seattle, Washington, USA, 2-5 August 2001, pp. 194\u2013202. Morgan Kaufmann (2001)"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Horak, T., et al.: Visual analysis of hyperproperties for understanding model checking results. IEEE Trans. Vis. Comput. Graph. 28(1) (2022) https:\/\/doi.org\/10.1109\/TVCG.2021.3114866","DOI":"10.1109\/TVCG.2021.3114866"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Hume, D.: An Enquiry Concerning Human Understanding. London (1748)","DOI":"10.1093\/oseo\/instance.00032980"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-030-59152-6_19","volume-title":"Automated Technology for Verification and Analysis","author":"A Ibrahim","year":"2020","unstructured":"Ibrahim, A., Pretschner, A.: From checking to inference: actual causality computations as optimization problems. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 343\u2013359. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_19"},{"key":"5_CR35","first-page":"241","volume":"53","author":"A Ibrahim","year":"2019","unstructured":"Ibrahim, A., Rehwald, S., Pretschner, A.: Efficiently checking actual causality with sat solving. Eng. Secure Dependable Softw. Syst. 53, 241\u2013255 (2019)","journal-title":"Eng. Secure Dependable Softw. Syst."},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-40184-8_19","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"A Kupriyanov","year":"2013","unstructured":"Kupriyanov, A., Finkbeiner, B.: Causality-based verification of multi-threaded programs. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 257\u2013272. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_19"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"814","DOI":"10.1007\/978-3-319-08867-9_54","volume-title":"Computer Aided Verification","author":"A Kupriyanov","year":"2014","unstructured":"Kupriyanov, A., Finkbeiner, B.: Causal termination of multi-threaded programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 814\u2013830. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_54"},{"key":"5_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-35873-9_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Leitner-Fischer","year":"2013","unstructured":"Leitner-Fischer, F., Leue, S.: Causality checking for complex system models. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 248\u2013267. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_16"},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Leitner-Fischer, F., Leue, S.: SpinCause: a tool for causality checking. In: International Symposium on Model Checking of Software, SPIN 2014. ACM (2014). https:\/\/doi.org\/10.1145\/2632362.2632371","DOI":"10.1145\/2632362.2632371"},{"issue":"17","key":"5_CR40","doi-asserted-by":"publisher","first-page":"556","DOI":"10.2307\/2025310","volume":"70","author":"DK Lewis","year":"1973","unstructured":"Lewis, D.K.: Causation. J. Philos. 70(17), 556\u2013567 (1973). https:\/\/doi.org\/10.2307\/2025310","journal-title":"J. Philos."},{"key":"5_CR41","volume-title":"Counterfactuals","author":"DK Lewis","year":"1973","unstructured":"Lewis, D.K.: Counterfactuals. Blackwell, Cambridge, MA, USA (1973)"},{"key":"5_CR42","doi-asserted-by":"publisher","unstructured":"Mascle, C., Baier, C., Funke, F., Jantsch, S., Kiefer, S.: 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, pp. 1\u201314. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470597","DOI":"10.1109\/LICS52264.2021.9470597"},{"key":"5_CR43","doi-asserted-by":"publisher","unstructured":"Parreaux, J., Piribauer, J., Baier, C.: Counterfactual causality for reachability and safety based on distance functions. In: Achilleos, A., Monica, D.D. (eds.) Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2023, Udine, Italy, 18-20 September 2023. EPTCS, vol.\u00a0390, pp. 132\u2013149 (2023). https:\/\/doi.org\/10.4204\/EPTCS.390.9","DOI":"10.4204\/EPTCS.390.9"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR45","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, 11-13 January 1989, pp. 179\u2013190. ACM Press (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"5_CR46","doi-asserted-by":"publisher","unstructured":"Sallinger, S., Weissenbacher, G., Zuleger, F.: A formalization of heisenbugs and their causes. In: Ferreira, C., Willemse, T.A.C. (eds.) Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, 6-10 November 2023, Proceedings. Lecture Notes in Computer Science, vol. 14323, pp. 282\u2013300. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47115-5_16","DOI":"10.1007\/978-3-031-47115-5_16"},{"key":"5_CR47","doi-asserted-by":"publisher","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: Albers, S., Marion, J. (eds.) 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, 26-28 February 2009, Freiburg, Germany, Proceedings. LIPIcs, vol.\u00a03, pp. 661\u2013672. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany (2009). https:\/\/doi.org\/10.4230\/LIPICS.STACS.2009.1854","DOI":"10.4230\/LIPICS.STACS.2009.1854"},{"key":"5_CR48","unstructured":"Schmitt, F., Hahn, C., Rabe, M.N., Finkbeiner, B.: Neural circuit synthesis from specification patterns. In: Ranzato, M., Beygelzimer, A., Dauphin, Y.N., Liang, P., Vaughan, J.W. (eds.) Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, 6-14 December 2021, virtual, pp. 15408\u201315420 (2021). https:\/\/proceedings.neurips.cc\/paper\/2021\/hash\/8230bea7d54bcdf99cdfe85cb07313d5-Abstract.html"},{"key":"5_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11901914_9","volume-title":"Automated Technology for Verification and Analysis","author":"C Wang","year":"2006","unstructured":"Wang, C., Yang, Z., Ivan\u010di\u0107, F., Gupta, A.: Whodunit? Causal analysis for counterexamples. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 82\u201395. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901914_9"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:04:03Z","timestamp":1721891043000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}