Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Reduction Techniques for Model Checking and Learning in MDPs
Authors: Suda Bharadwaj, Stephane Le Roux, Guillermo Perez, Ufuk Topcu
IJCAI 2017 | Venue PDF | 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 EMAIL, EMAIL |
| 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. |