Reduction Techniques for Model Checking and Learning in MDPs
Authors: Suda Bharadwaj, Stephane Le Roux, Guillermo Perez, Ufuk Topcu
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present some results of running the reduction techniques on two model checking case studies from PRISM [Kwiatkowska et al., 2011], a well-known probabilistic model checking tool, as well as a model-learning task in a gridworld. |
| Researcher Affiliation | Academia | University of Texas at Austin Universit e libre de Bruxelles {suda.b, utopcu}@utexas.edu, {stephane.le.roux, gperezme}@ulb.ac.be |
| Pseudocode | Yes | Algorithm 1 MDP reductions based on irrelevant distributions |
| Open Source Code | No | No concrete access to source code is provided. The paper states: "Our algorithm has been implemented in a prototype tool and empirical results suggest that our algorithm achieves a high reduction rate." but no link or explicit release statement. |
| Open Datasets | Yes | The protocol is modelled in the PRISM language by [Kwiatkowska et al., 2001].1 We implement our reduction techniques, as well as the currently-used ones, and the results are given in Tab. 1. 1Model details can be found on the PRISM case studies website. We use model parameters: 2 coins and K = 2, and reset = TRUE and K {1, 2}, respectively. |
| Dataset Splits | No | No specific dataset split information (percentages, sample counts, or explicit splitting methodology) is provided. The paper describes experiments on existing PRISM models and generated gridworlds. |
| Hardware Specification | No | No specific hardware details (like GPU/CPU models, memory amounts, or specific computer specifications) are provided. |
| Software Dependencies | No | The paper mentions "PRISM [Kwiatkowska et al., 2011]" as a tool used, but does not provide a specific version number. No other specific software dependencies with versions are listed. |
| Experiment Setup | Yes | For standardization, 20% of each gridworld was populated with obstacles." and "Explicitly, we aim to learn a policy that with probability at least 1 δ will be ε-optimal in maximizing reachability probability. We measure the decrease in sampling required before ε-optimality is achieved for ε = 0.01 and δ = 0.05. |