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..
Symbolic Model Checking for One-Resource RB+-ATL
Authors: Natasha Alechina, Brian Logan, Hoang Nga Nguyen, Franco Raimondi
IJCAI 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In this paper, we consider a fragment of RB ATL, 1RB ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces. and 5 Experimental Evaluation of Performance |
| Researcher Affiliation | Academia | 1 School of Computer Science, University of Nottingham, UK 2 Department of Computer Science, Middlesex University, UK |
| Pseudocode | Yes | Algorithm 1 Labelling ϕ0 and Algorithm 2 Labelling ϕ0 |
| Open Source Code | Yes | 1Available from www.vrbmas.org/dl/ijcai15.zip |
| Open Datasets | No | The paper describes a custom-designed example problem ('scenario in which three agents compete in an infinite sequence of car races') that is scaled up, but does not provide access information or refer to a standard public dataset. |
| Dataset Splits | No | The paper uses an example problem scaled with engine types |T| {3, 4, 5, 6} and tests formulas with resource bounds b {|T| 1, |T|}. This describes the problem parameters, not a dataset split for training/validation/testing. |
| Hardware Specification | Yes | The experiment was carried out on a quad-core 64-bit Processor running at 2.66 GHz with 32GB of memory. |
| Software Dependencies | No | The paper states, 'We have implemented Algorithm 2 on top of the model checker MCMAS [Lomuscio et al., 2009]', but it does not specify the version number of MCMAS or any other software. |
| Experiment Setup | Yes | Consider a scenario in which three agents compete in an infinite sequence of car races by spending and earning money. Each car is equipped with one of three possible types of engine T = {1, 2, 3}. and We have encoded examples in which the number of engine types |T| {3, 4, 5, 6}. and we want to check if the formulas ϕ1(b) = {1}b U 1fst for b {|T| 1, |T|} and ϕ2 = {1, 2}1 U 1fst where 1fst is a proposition that is only true in states where agent 1 ranks first. |