Probabilistic causes in Markov chains

Innovations in Systems and Software Engineering - Tập 18 - Trang 347-367 - 2022
Robin Ziemek1, Jakob Piribauer1, Florian Funke1, Simon Jantsch1, Christel Baier1
1Technische Universität Dresden, Dresden, Germany

Tóm tắt

By combining two of the central paradigms of causality, namely counterfactual reasoning and probability-raising, we introduce a probabilistic notion of cause in Markov chains. Such a cause consists of finite executions of the probabilistic system after which the probability of an $$\omega $$ -regular effect exceeds a given threshold. The cause, as a set of executions, then has to cover all behaviors exhibiting the effect. With these properties, such causes can be used for monitoring purposes where the aim is to detect faulty behavior before it actually occurs. In order to choose which cause should be computed, we introduce multiple types of costs to capture the consumption of resources by the system or monitor from different perspectives, and study the complexity of computing cost-minimal causes.

Tài liệu tham khảo

Baier C, Dubslaff C, Funke F, Jantsch S, Majumdar R, Piribauer J, Ziemek R (2021) From verification to causality-based explications. In: 48th International colloquium on automata, languages, and programming (ICALP 2021). Leibniz international proceedings in informatics (LIPIcs), vol 198. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, pp 1:1–1:20. https://doi.org/10.4230/LIPIcs.ICALP.2021.1 Baier C, Funke F, Jantsch S, Piribauer J, Ziemek R (2021) Probabilistic causes in Markov chains. In: Hou Z, Ganesh V (eds) 19th international symposium on automated technology for verification and analysis (ATVA). Programming and software engineering, vol 12971. Springer, Berlin, pp 205–221 Baier C, Funke F, Piribauer J, Ziemek R (2022) On probability-raising causality in markov decision processes, extended version of an accepted publication at FoSSaCS 2022 Baier C, Katoen JP (2008) Principles of model checking (representation and mind series). The MIT Press, Cambridge Bartocci E, Grosu R, Karmarkar A, Smolka SA, Stoller SD, Zadok E, Seyster J (2013) Adaptive runtime verification. In: Runtime verification. Springer, Berlin, pp 168–182. https://doi.org/10.1007/978-3-642-35632-2_18 Beer I, Ben-David S, Chockler H, Orni A, Trefler R (2009) Explaining counterexamples using causality. In: Computer aided verification (CAV’09). Springer, Berlin, pp 94–108. https://doi.org/10.1007/978-3-642-02658-4_11 Bertsekas DP, Tsitsiklis JN (1991) An analysis of stochastic shortest path problems. Math Oper Res 16(3):580–595 Braham M, van Hees M (2012) An anatomy of moral responsibility. Mind 121(483):601–634 Brihaye T, Geeraerts G, Haddad A, Monmege B (2015) To reach or not to reach? Efficient algorithms for total-payoff games. In: Proceedings of the 26th international conference on concurrency theory (CONCUR’15). LIPIcs, vol 42, pp 297–310. https://doi.org/10.4230/LIPIcs.CONCUR.2015.297 Chadha R, Sistla AP, Viswanathan M (2009) On the expressiveness and complexity of randomization in finite state monitors. J ACM. https://doi.org/10.1145/1552285.1552287 Chatterjee K, Chmelík M, Tracol M (2016) What is decidable about partially observable Markov decision processes with omega-regular objectives. J Comput Syst Sci 82(5):878–911. https://doi.org/10.1016/j.jcss.2016.02.009 Chatterjee K, Doyen L, Henzinger TA (2017) The cost of exactness in quantitative reachability. In: Models, algorithms, logics and tools, pp 367–381. Springer, Cham. https://doi.org/10.1007/978-3-319-63121-9_18 Chockler H, Halpern JY (2004) Responsibility and blame: a structural-model approach. J Artif Int Res 22(1):93–115 Chockler H, Halpern JY, Kupferman O (2008) What causes a system to satisfy a specification? ACM Trans Comput Logic 9(3):20:1-20:26 Cini C, Francalanza A (2015) An LTL proof system for runtime verification. In: Baier C, Tinelli C (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 581–595 Cormen TH, Leiserson CE, Rivest RL, Stein C (2009) Introduction to algorithms, 3rd edn. The MIT Press, Cambridge Daca P, Henzinger TA, Křetínský J, Petrov T (2016) Faster statistical model checking for unbounded temporal properties. In: Tools and algorithms for the construction and analysis of systems. Springer, Heidelberg, pp 112–129. https://doi.org/10.1007/978-3-662-49674-9_7 Dash D, Voortman M, De Jongh M (2013) Sequences of mechanisms for causal reasoning in artificial intelligence. In: Proceedings of the 23rd international joint conference on artificial intelligence. IJCAI ’13. AAAI Press, pp 839–845 Eells E (1991) Probabilistic causality. Cambridge studies in probability, induction and decision theory. Cambridge University Press, Cambridge Eiter T, Lukasiewicz T (2004) Complexity results for explanations in the structural-model approach. Artif Intell 154(1–2):145–198 Eiter T, Lukasiewicz T (2006) Causes and explanations in the structural-model approach: tractable cases. Artif Intell 170(6–7):542–580 Esparza J, Kiefer S, Kretinsky J, Weininger M (2020) Online monitoring \(\omega \)-regular properties in unknown Markov chains. arxiv:2010.08347 Faran R, Kupferman O (2018) Spanning the spectrum from safety to liveness. Acta Informat 55(8):703–732. https://doi.org/10.1007/s00236-017-0307-4 Feigenbaum J, Hendler JA, Jaggard AD, Weitzner DJ, Wright RN (2011) Accountability and deterrence in online life. In: Proceedings of WebSci ’11. ACM, New York, NY, USA. https://doi.org/10.1145/2527031.2527043 Fenton-Glynn L (2016) A proposed probabilistic extension of the Halpern and Pearl definition of ‘actual cause’. Br J Philos Sci 68(4):1061–1124 Gill J (1977) Computational complexity of probabilistic Turing machines. SIAM J Comput 6(4):675–695. https://doi.org/10.1137/0206049 Gondi K, Patel Y, Sistla AP (2009) Monitoring the full range of \(\omega \)-regular properties of stochastic systems. In: Proceedings of VMCAI’09. Springer, Berlin, pp 105–119. https://doi.org/10.1007/978-3-540-93900-9_12 Haase C, Kiefer S (2015) The odds of staying on budget. In: Automata, languages, and programming. Springer, Berlin, pp 234–246. https://doi.org/10.1007/978-3-662-47666-6_19 Haase C, Kiefer S (2016) The complexity of the Kth largest subset problem and related problems. Inf Process Lett 116(2):111–115. https://doi.org/10.1016/j.ipl.2015.09.015 Halpern JY (2015) A modification of the Halpern-Pearl definition of causality. In: Proceedings of IJCAI’15. AAAI Press, pp 3022–3033 Halpern JY, Pearl J (2001) Causes and explanations: a structural-model approach: part 1: causes. In: Proceedings of the 17th conference in uncertainty in artificial intelligence (UAI), pp 194–202 Huang Y, Kleinberg S (2015) Fast and Accurate causal inference from time series data. In: Proceedings of FLAIRS 2015. AAAI Press, pp 49–54 Ibrahim A, Pretschner A (2020) From checking to inference: actual causality computations as optimization problems. In: Proceedings of ATVA’20. Springer, Cham, , pp 343–359. https://doi.org/10.1007/978-3-030-59152-6_19 Ibrahim A, Pretschner A, Klesel T, Zibaei E, Kacianka S, Pretschner A (2020) Actual causality canvas: a general framework for explanation-based socio-technical constructs. In: Proceedings of ECAI’20. IOS Press Ebooks, pp 2978–2985. https://doi.org/10.3233/FAIA200472 Kalajdzic K, Bartocci E, Smolka SA, Stoller SD, Grosu R (2013) Runtime verification with particle filtering. In: Runtime verification. Springer, Berlin, pp 149–166. https://doi.org/10.1007/978-3-642-40787-1_9 Kao JY, Rampersad N, Shallit J (2009) On NFAs where all states are final, initial, or both. Theor Comput Sci 410(47–49):5010–5021 Kleinberg S (2011) A logic for causal inference in time series with discrete and continuous variables. In: Proceedings of IJCAI’11, pp 943–950 Kleinberg S, Hripcsak G (2011) A review of causal inference for biomedical informatics. J Biomed Inform 44(6):1102–12. https://doi.org/10.1016/j.jbi.2011.07.001 Kleinberg S, Mishra B (2009) The temporal logic of causal structures. In: Proceedings of the twenty-fifth conference on uncertainty in artificial intelligence (UAI), pp 303–312 Kleinberg S, Mishra B (2010) The temporal logic of token causes. In: Proceedings of KR’10. AAAI Press, pp 575–577 Madani O, Hanks S, Condon A (1999) On the undecidability of probabilistic planning and infinite-horizon partially observable markov decision problems. In: Proceedings of the sixteenth national conference on artificial intelligence and the eleventh innovative applications of artificial intelligence conference innovative applications of artificial intelligence. AAAI ’99/IAAI ’99, American Association for Artificial Intelligence, USA, pp 541–548 Miller T (2017) Explanation in artificial intelligence: insights from the social sciences. Artif Intell. https://doi.org/10.1016/j.artint.2018.07.007 Pearl J (2009) Causality, 2nd edn. Cambridge University Press, Cambridge Piribauer J, Baier C (2019) Partial and conditional expectations in Markov decision processes with integer weights. In: Proceedings of FoSSaCS’19. Lecture notes in computer science, vol 11425. Springer, pp 436–452 Reichenbach H (1956) The direction of time. Dover Publications, Mineola Sistla AP, Srinivas AR (2008) Monitoring temporal properties of stochastic systems. In: Logozzo F, Peled DA, Zuck LD (eds) Verification, model checking, and abstract interpretation. Springer, Berlin, pp 294–308 Stoller SD, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka SA, Zadok E (2012) Runtime verification with state estimation. In: Runtime verification. Springer, Berlin, pp 193–207. https://doi.org/10.1007/978-3-642-29860-8_15 Suppes P (1970) A probabilistic theory of causality. North-Holland Pub. Co., Amsterdam Toda S (1991) PP is as hard as the polynomial-time hierarchy. SIAM J Comput 20(5):865–877. https://doi.org/10.1137/0220053 Vennekens J, Bruynooghe M, Denecker M (2010) Embracing events in causal modelling: interventions and counterfactuals in CP-logic. In: Logics in artificial intelligence. Springer, Berlin, pp 313–325 Vennekens J, Denecker M, Bruynooghe M (2009) CP-logic: a language of causal probabilistic events and its relation to logic programming. Theory Pract Logic Program 9(3):245–308. https://doi.org/10.1017/S1471068409003767 Zheng M, Kleinberg S (2017) A method for automating token causal explanation and discovery. In: Proceedings of FLAIRS’17