conference paper published yes S. Akshay author Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Tobias Meggendorfer author b21b0c15-30a2-11eb-80dc-f13ca25802e10000-0002-1712-2165 Dorde Zikelic author 294AA7A6-F248-11E8-B48F-1D18A9856A870000-0002-4681-1699 KrCh department CAV: Computer Aided Verification International IST Doctoral Program project Formal Methods for Stochastic Models: Algorithms and Applications project 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. In 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. https://research-explorer.ista.ac.at/download/14317/14349/2023_LNCS_Akshay.pdf application/pdfno Springer Nature2023Paris, France eng 0302-9743 1611-3349 9783031377082 00131080560000510.1007/978-3-031-37709-9_5 1396686-112 S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic, in:, International Conference on Computer Aided Verification, Springer Nature, 2023, pp. 86–112. 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. 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> 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>. 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>. 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. 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> 143172023-09-10T22:01:12Z2025-09-09T12:56:00Z