Shepherding hordes of Markov chains

DOI10.1007/978-3-030-17465-1_10MaRDI QIDQ6091408zbMATH OpenOpenAlexFDO

Authors Milan Češka, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen

Publication date 24 November 2023

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1902.05727

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Markov and semi-Markov decision processes (90C40)

Abstract: This paper considers large families of Markov chains (MCs) that are defined over a set of parameters with finite discrete domains. Such families occur in software product lines, planning under partial observability, and sketching of probabilistic programs. Simple questions, like `does at least one family member satisfy a property?', are NP-hard. We tackle two problems: distinguish family members that satisfy a given quantitative property from those that do not, and determine a family member that satisfies the property optimally, i.e., with the highest probability or reward. We show that combining two well-known techniques, MDP model checking and abstraction refinement, mitigates the computational complexity. Experiments on a broad set of benchmarks show that in many situations, our approach is able to handle families of millions of MCs, providing superior scalability compared to existing solutions.

Recommendations

• Finding provably optimal Markov chains
• Parameter synthesis in Markov models: a gentle survey
• Are parametric Markov chains monotonic?
• Distributed Markov chains
• scientific article; zbMATH DE number 1538048

Cited in

(8)

• Parameter synthesis in Markov models: a gentle survey
• Featured Team Automata
• Search and explore: symbiotic policy synthesis in POMDPs
• Counterexample-driven synthesis for probabilistic program sketches
• Deductive controller synthesis for probabilistic hyperproperties
• Parameter synthesis for Markov models: covering the parameter space
• Search and explore: symbiotic policy synthesis in POMDPs
• An oracle-guided approach to constrained policy synthesis under uncertainty

This page was built for publication: Shepherding hordes of Markov chains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6091408)