TL;DR
This paper introduces SEA-PARAM, a tool for analyzing optimal deterministic memoryless schedulers in parametric Markov decision processes across all parameter values, focusing on parameter-independent reachability probabilities.
Contribution
It presents a novel approach to characterizing optimal schedulers in PMDPs, differing from existing parameter synthesis methods by focusing on scheduler types over parameter ranges.
Findings
SEA-PARAM successfully computes optimal schedulers for PMDPs.
Experimental results demonstrate the effectiveness of the approach.
The method provides insights into scheduler behavior across parameter spaces.
Abstract
We study parametric Markov decision processes (PMDPs) and their reachability probabilities "independent" of the parameters. Different to existing work on parameter synthesis (implemented in the tools PARAM and PRISM), our main focus is on describing different types of optimal deterministic memoryless schedulers for the whole parameter range. We implement a simple prototype tool SEA-PARAM that computes these optimal schedulers and show experimental results.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
