[{"abstract":[{"text":"Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization.\r\nIn light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples.","lang":"eng"}],"doi":"10.1007/978-3-031-37709-9_5","day":"17","date_updated":"2025-07-14T09:09:56Z","year":"2023","citation":{"ista":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 86–112.","mla":"Akshay, S., et al. “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.” <i>International Conference on Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 86–112, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">10.1007/978-3-031-37709-9_5</a>.","short":"S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 86–112.","ieee":"S. Akshay, K. Chatterjee, T. Meggendorfer, and D. Zikelic, “MDPs as distribution transformers: Affine invariant synthesis for safety objectives,” in <i>International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 86–112.","chicago":"Akshay, S., Krishnendu Chatterjee, Tobias Meggendorfer, and Dorde Zikelic. “MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.” In <i>International Conference on Computer Aided Verification</i>, 13966:86–112. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">https://doi.org/10.1007/978-3-031-37709-9_5</a>.","ama":"Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. In: <i>International Conference on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:86-112. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">10.1007/978-3-031-37709-9_5</a>","apa":"Akshay, S., Chatterjee, K., Meggendorfer, T., &#38; Zikelic, D. (2023). MDPs as distribution transformers: Affine invariant synthesis for safety objectives. In <i>International Conference on Computer Aided Verification</i> (Vol. 13966, pp. 86–112). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_5\">https://doi.org/10.1007/978-3-031-37709-9_5</a>"},"ddc":["000"],"acknowledgement":"This work was supported in part by the ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385 as well as DST/CEFIPRA/INRIA project EQuaVE and SERB Matrices grant MTR/2018/00074.","volume":13966,"alternative_title":["LNCS"],"title":"MDPs as distribution transformers: Affine invariant synthesis for safety objectives","intvolume":"     13966","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2023-09-10T22:01:12Z","article_processing_charge":"Yes (in subscription journal)","author":[{"last_name":"Akshay","first_name":"S.","full_name":"Akshay, S."},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"_id":"14317","scopus_import":"1","publisher":"Springer Nature","file_date_updated":"2023-09-20T08:46:43Z","page":"86-112","ec_funded":1,"quality_controlled":"1","oa":1,"publication_identifier":{"isbn":["9783031377082"],"eissn":["1611-3349"],"issn":["0302-9743"]},"date_published":"2023-07-17T00:00:00Z","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"access_level":"open_access","relation":"main_file","success":1,"creator":"dernst","file_id":"14349","file_size":531745,"checksum":"f143c8eedf609f20f2aad2eeb496d53f","date_created":"2023-09-20T08:46:43Z","content_type":"application/pdf","file_name":"2023_LNCS_Akshay.pdf","date_updated":"2023-09-20T08:46:43Z"}],"month":"07","oa_version":"Published Version","project":[{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385","name":"International IST Doctoral Program"},{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"publication":"International Conference on Computer Aided Verification","has_accepted_license":"1","conference":{"name":"CAV: Computer Aided Verification","start_date":"2023-07-17","location":"Paris, France","end_date":"2023-07-22"},"language":[{"iso":"eng"}]},{"publisher":"Springer Nature","file_date_updated":"2023-09-20T08:24:47Z","ec_funded":1,"quality_controlled":"1","page":"16-39","intvolume":"     13966","alternative_title":["LNCS"],"title":"Automated tail bound analysis for probabilistic recurrence relations","department":[{"_id":"KrCh"}],"date_created":"2023-09-10T22:01:12Z","article_processing_charge":"Yes (in subscription journal)","publication_status":"published","author":[{"full_name":"Sun, Yican","last_name":"Sun","first_name":"Yican"},{"last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir Kafshdar","orcid":"0000-0003-1702-6584","last_name":"Goharshady","first_name":"Amir Kafshdar"}],"scopus_import":"1","_id":"14318","ddc":["000"],"volume":13966,"acknowledgement":"We thank Prof. Bican Xia for valuable information on the exponential theory of reals. The work is partially supported by the National Natural Science Foundation of China (NSFC) with Grant No. 62172271, ERC CoG 863818 (ForM-SMArt), the Hong Kong Research Grants Council ECS Project Number 26208122, the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055 and the HKUST Startup Grant R9272.","abstract":[{"text":"Probabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit κ, we consider the tail probability Pr[T≥κ], i.e., the probability that the randomized runtime T of the PRR exceeds κ. Our focus is the formal analysis of tail bounds that aims at finding a tight asymptotic upper bound u≥Pr[T≥κ]. To address this problem, the classical and most well-known approach is the cookbook method by Karp (JACM 1994), while other approaches are mostly limited to deriving tail bounds of specific PRRs via involved custom analysis.\r\nIn this work, we propose a novel approach for deriving the common exponentially-decreasing tail bounds for PRRs whose preprocessing time and random passed sizes observe discrete or (piecewise) uniform distribution and whose recursive call is either a single procedure call or a divide-and-conquer. We first establish a theoretical approach via Markov’s inequality, and then instantiate the theoretical approach with a template-based algorithmic approach via a refined treatment of exponentiation. Experimental evaluation shows that our algorithmic approach is capable of deriving tail bounds that are (i) asymptotically tighter than Karp’s method, (ii) match the best-known manually-derived asymptotic tail bound for QuickSelect, and (iii) is only slightly worse (with a loglogn factor) than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover, our algorithmic approach handles all examples (including realistic PRRs such as QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1 s, showing that our approach is efficient in practice.","lang":"eng"}],"day":"17","doi":"10.1007/978-3-031-37709-9_2","citation":{"ieee":"Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Automated tail bound analysis for probabilistic recurrence relations,” in <i>Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 16–39.","chicago":"Sun, Yican, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. “Automated Tail Bound Analysis for Probabilistic Recurrence Relations.” In <i>Computer Aided Verification</i>, 13966:16–39. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_2\">https://doi.org/10.1007/978-3-031-37709-9_2</a>.","ama":"Sun Y, Fu H, Chatterjee K, Goharshady AK. Automated tail bound analysis for probabilistic recurrence relations. In: <i>Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:16-39. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_2\">10.1007/978-3-031-37709-9_2</a>","apa":"Sun, Y., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2023). Automated tail bound analysis for probabilistic recurrence relations. In <i>Computer Aided Verification</i> (Vol. 13966, pp. 16–39). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_2\">https://doi.org/10.1007/978-3-031-37709-9_2</a>","ista":"Sun Y, Fu H, Chatterjee K, Goharshady AK. 2023. Automated tail bound analysis for probabilistic recurrence relations. Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 16–39.","short":"Y. Sun, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Computer Aided Verification, Springer Nature, 2023, pp. 16–39.","mla":"Sun, Yican, et al. “Automated Tail Bound Analysis for Probabilistic Recurrence Relations.” <i>Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 16–39, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_2\">10.1007/978-3-031-37709-9_2</a>."},"year":"2023","date_updated":"2025-07-14T09:09:57Z","conference":{"start_date":"2023-07-17","name":"CAV: Computer Aided Verification","location":"Paris, France","end_date":"2023-07-22"},"language":[{"iso":"eng"}],"month":"07","project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"Computer Aided Verification","status":"public","related_material":{"link":[{"relation":"software","url":"https://github.com/boyvolcano/PRR"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","access_level":"open_access","success":1,"creator":"dernst","file_id":"14348","checksum":"42917e086f8c7699f3bccf84f74fe000","file_size":624647,"date_created":"2023-09-20T08:24:47Z","content_type":"application/pdf","file_name":"2023_LNCS_Sun.pdf","date_updated":"2023-09-20T08:24:47Z"}],"oa":1,"publication_identifier":{"isbn":["9783031377082"],"issn":["0302-9743"],"eissn":["1611-3349"]},"type":"conference","date_published":"2023-07-17T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"}},{"type":"conference","date_published":"2023-07-16T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publication_identifier":{"eisbn":["9783031377099"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031377082"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","related_material":{"record":[{"id":"14994","relation":"research_data","status":"public"}]},"file":[{"access_level":"open_access","success":1,"relation":"main_file","creator":"dernst","file_id":"14765","checksum":"1a361d83db0244fd32c03b544c294b5a","file_size":405147,"date_created":"2024-01-09T10:01:07Z","content_type":"application/pdf","file_name":"2023_LNCSCAV_Majumdar.pdf","date_updated":"2024-01-09T10:01:07Z"}],"has_accepted_license":"1","publication":"35th International Conference on Computer Aided Verification","month":"07","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"location":"Paris, France","end_date":"2023-07-22","name":"CAV: Computer Aided Verification","start_date":"2023-07-17"},"year":"2023","citation":{"ama":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In: <i>35th International Conference on Computer Aided Verification</i>. Vol 13966. Springer Nature; 2023:3-15. doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>","apa":"Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.-K., &#38; Soudjani, S. (2023). A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. In <i>35th International Conference on Computer Aided Verification</i> (Vol. 13966, pp. 3–15). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>","ieee":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani, “A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties,” in <i>35th International Conference on Computer Aided Verification</i>, Paris, France, 2023, vol. 13966, pp. 3–15.","chicago":"Majumdar, Rupak, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, and Sadegh Soudjani. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” In <i>35th International Conference on Computer Aided Verification</i>, 13966:3–15. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">https://doi.org/10.1007/978-3-031-37709-9_1</a>.","short":"R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, S. Soudjani, in:, 35th International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 3–15.","mla":"Majumdar, Rupak, et al. “A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.” <i>35th International Conference on Computer Aided Verification</i>, vol. 13966, Springer Nature, 2023, pp. 3–15, doi:<a href=\"https://doi.org/10.1007/978-3-031-37709-9_1\">10.1007/978-3-031-37709-9_1</a>.","ista":"Majumdar R, Mallik K, Rychlicki M, Schmuck A-K, Soudjani S. 2023. A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties. 35th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 3–15."},"date_updated":"2024-02-27T07:39:51Z","abstract":[{"lang":"eng","text":"We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using these flexible game solvers as a back-end, we implemented a tool for computing correct-by-construction controllers for stochastic dynamical systems under LTL specifications. Our implementations use the recent theoretical result that all of these games can be solved using the same symbolic fixpoint algorithm but utilizing different, domain specific calculations of the involved predecessor operators. The main feature of our toolchain is the utilization of two programming abstractions: one to separate the symbolic fixpoint computations from the predecessor calculations, and another one to allow the integration of different BDD libraries as back-ends. In particular, we employ a multi-threaded execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan, which leads to enormous computational savings."}],"day":"16","doi":"10.1007/978-3-031-37709-9_1","ddc":["000"],"acknowledgement":"Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047.","volume":13966,"author":[{"first_name":"Rupak","last_name":"Majumdar","full_name":"Majumdar, Rupak"},{"last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598"},{"full_name":"Rychlicki, Mateusz","last_name":"Rychlicki","first_name":"Mateusz"},{"last_name":"Schmuck","first_name":"Anne-Kathrin","full_name":"Schmuck, Anne-Kathrin"},{"last_name":"Soudjani","first_name":"Sadegh","full_name":"Soudjani, Sadegh"}],"scopus_import":"1","_id":"14758","intvolume":"     13966","title":"A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"date_created":"2024-01-08T13:18:00Z","article_processing_charge":"Yes (in subscription journal)","publication_status":"published","file_date_updated":"2024-01-09T10:01:07Z","ec_funded":1,"quality_controlled":"1","page":"3-15","publisher":"Springer Nature"}]