Verification of Agent-Based Artifact Systems
Authors: F. Belardinelli, A. Lomuscio, F. Patrizi
JAIR 2014 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper we put forward artifact-centric multi-agent systems, a novel formalisation of artifact systems in the context of multi-agent systems operating on them. ... We study the model checking problem for artifact-centric multi-agent systems against specifications expressed in a quantified version of temporal-epistemic logic ... we also show that the corresponding model checking problem is EXPSPACE-complete. ... We exemplify the theoretical results here pursued through a mainstream procurement scenario from the artifact systems literature. |
| Researcher Affiliation | Academia | Francesco Belardinelli EMAIL Laboratoire Ibisc, Universit e d Evry, France Alessio Lomuscio EMAIL Department of Computing, Imperial College London, UK Fabio Patrizi EMAIL Dipartimento di Ingegneria Informatica, Automatica e Gestionale A. Ruberti Universit a di Roma La Sapienza , Italy |
| Pseudocode | No | The paper defines formal grammars (BNF for FO-formulas, FO-CTLK), mathematical definitions, and tables describing preconditions and postconditions in logic, but it does not include any clearly labeled 'Pseudocode' or 'Algorithm' blocks with structured procedural steps. |
| Open Source Code | No | The paper does not provide any explicit statement about releasing source code for the methodology described, nor does it include links to a code repository. It mentions other tools like 'IBM engine BARCELONA' and 'Ver ICS 2007', but these are not the authors' own code for the paper's contribution. |
| Open Datasets | No | The paper discusses a 'mainstream procurement scenario' or 'order-to-cash scenario' as a theoretical example or case study to exemplify the techniques. It describes 'artifact data models are represented as database schemas' and uses an 'infinite set Uotc of alphanumeric strings as the interpretation domain' within this example. No actual empirical dataset is used or provided for public access. |
| Dataset Splits | No | The paper does not use any empirical datasets, and therefore, no information regarding training, testing, or validation splits is provided. |
| Hardware Specification | No | The paper focuses on theoretical model checking problems and formalisms. It does not describe any experimental setup that would require specific hardware, thus no hardware specifications are mentioned. |
| Software Dependencies | No | The paper discusses formal logic (e.g., FO-CTLK, µ-calculus) and conceptual systems (e.g., artifact-centric programs, Turing machines, WS-BPEL, GSM) but does not list specific software libraries, tools, or frameworks with version numbers that were used by the authors for their research or experiments. |
| Experiment Setup | No | The paper is theoretical and does not describe any empirical experiments. Therefore, there are no details provided regarding experimental setup, hyperparameters, training configurations, or system-level settings. |