Verifying Existence of Resource-Bounded Coalition Uniform Strategies
Authors: Natasha Alechina, Mehdi Dastani, Brian Logan
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | The main contribution of this paper is a decidable model-checking procedure for RB ATSEL with coalition-uniform strategies (wrt any decidable notion of indistinguishability). To prove decidability we give an algorithm which, given a structure M = (Φ, Agt, Res, S, , Act, d, c, δ) and a formula φ0, returns the set of states [φ0]M satisfying φ0: [φ0]M = {s | M, s |= φ0}. The theorem follows from Lemmas 1 and 2 which establish termination and correctness of the algorithm respectively. |
| Researcher Affiliation | Academia | Natasha Alechina University of Nottingham nza@cs.nott.ac.uk Mehdi Dastani University of Utrecht m.m.dastani@uu.nl Brian Logan University of Nottingham bsl@cs.nott.ac.uk |
| Pseudocode | Yes | Algorithm 1 Labelling φ0; Algorithm 2 Labelling hh Abiiφ U; Algorithm 3 Labelling hh Abii2φ |
| Open Source Code | No | The paper does not provide any statement or link indicating that the source code for the described methodology is publicly available. |
| Open Datasets | No | The paper is theoretical and focuses on logic and model-checking decidability. It does not involve empirical experiments with datasets that would require training, validation, or testing. |
| Dataset Splits | No | The paper is theoretical and focuses on logic and model-checking decidability. It does not involve empirical experiments with datasets that would require training, validation, or testing splits. |
| Hardware Specification | No | The paper does not mention any specific hardware used for experiments, as it is a theoretical work focusing on logical formalisms and algorithms. |
| Software Dependencies | No | The paper describes a logical formalism and algorithms but does not specify any software dependencies with version numbers for their implementation or application. |
| Experiment Setup | No | The paper is theoretical and presents algorithms and proofs. It does not describe an experimental setup with hyperparameters or training settings as it does not involve empirical model training. |