Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic

Authors: Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, Sasha Rubin

IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical We study a class of synchronous, perfect-recall multi-agent systems with imperfect information and broadcasting, i.e., fully observable actions. We define an epistemic extension of strategy logic with incomplete information and the assumption of uniform and coherent strategies. In this setting, we prove that the model checking problem, and thus rational synthesis, is non-elementary decidable.
Researcher Affiliation Academia Francesco Belardinelli Laboratoire IBISC, UEVE and IRIT Toulouse belardinelli@ibisc.fr Alessio Lomuscio Department of Computing Imperial College London a.lomuscio@imperial.ac.uk Aniello Murano and Sasha Rubin DIETI Universit a degli Studi di Napoli murano@na.infn.it rubin@unina.it
Pseudocode No The paper does not contain any pseudocode or clearly labeled algorithm blocks.
Open Source Code No The paper does not provide any statement or link regarding the availability of open-source code for the described methodology.
Open Datasets No The paper is theoretical and does not conduct experiments with datasets, thus it does not mention public datasets or provide access information for training data.
Dataset Splits No The paper is theoretical and does not conduct experiments with datasets, thus it does not provide any dataset split information for validation.
Hardware Specification No The paper is theoretical and focuses on logic and model checking; it does not describe any computational experiments requiring hardware specifications.
Software Dependencies No The paper is theoretical and does not detail any experimental setups or software implementations that would require listing specific software dependencies with version numbers.
Experiment Setup No The paper is theoretical and describes formalisms and proofs rather than empirical experiments. Therefore, it does not include details on experimental setup, hyperparameters, or training settings.