Parameterised Verification of Infinite State Multi-Agent Systems via Predicate Abstraction
Authors: Panagiotis Kouvaros, Alessio Lomuscio
AAAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We define a class of parameterised infinite state multi-agent systems (MAS) that is unbounded in both the number of agents composing the system and the domain of the variables encoding the agents. We analyse their verification problem by combining and extending existing techniques in parameterised model checking with predicate abstraction procedures. The resulting methodology addresses both forms of unboundedness and provides a technique for verifying unbounded MAS defined on infinite-state variables. We illustrate the effectiveness of the technique on an infinite-domain variant of an unbounded version of the train-gate-controller. In future work we intend to implement the methodology here described. |
| Researcher Affiliation | Academia | Panagiotis Kouvaros and Alessio Lomuscio Department of Computing, Imperial College London, UK {p.kouvaros, a.lomuscio}@imperial.ac.uk |
| Pseudocode | No | The paper mentions giving 'an algorithm for the verification of MAS' in Section 3, but this algorithm is described textually rather than presented in a structured pseudocode block or formal algorithm format. |
| Open Source Code | No | The paper does not contain any statements about making source code open, providing links to repositories, or including code in supplementary materials. The conclusion states: 'In future work we intend to implement the methodology here described.' |
| Open Datasets | Yes | We exemplify the technical notions introduced above on a variant of the train-gate-controller (TGC) (Alur, Henzinger, and Kupferman 2002) where both the number of trains and some of the domains for the variables in the trains programs are unbounded. |
| Dataset Splits | No | The paper presents a theoretical framework and illustrates it with an example; it does not perform empirical experiments requiring training, validation, or test splits. No specific dataset splits are mentioned. |
| Hardware Specification | No | The paper is theoretical and outlines a methodology. It does not report on experimental setups or provide details about hardware specifications used for running experiments. |
| Software Dependencies | No | The paper mentions existing model checkers like 'Verics, MCK and MCMAS' as background, but it does not specify any software dependencies with version numbers for the methodology presented in this paper. The conclusion also states: 'In future work we intend to implement the methodology here described.' |
| Experiment Setup | No | The paper focuses on a theoretical methodology and its formal properties, illustrating it with an example. It does not describe an experimental setup with specific hyperparameters, training configurations, or system-level settings, as it does not involve empirical experiments. |