Symbolic Model Checking for One-Resource RB+-ATL
Authors: Natasha Alechina, Brian Logan, Hoang Nga Nguyen, Franco Raimondi
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | 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. |