Probabilistic causes in Markov chains
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