Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications
Authors: Petr Čermák, Alessio Lomuscio, Aniello Murano
AAAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We report on a BDD-based model checker implementing the algorithm and evaluate its performance on the fair process scheduler synthesis. To evaluate the proposed approach, we present the experimental results obtained for the problem of fair process scheduler synthesis. |
| Researcher Affiliation | Academia | Petr ˇCerm ak and Alessio Lomuscio Imperial College London, UK Aniello Murano Universit a degli Studi di Napoli Federico II, Italy |
| Pseudocode | No | The paper describes algorithms in prose but does not contain any structured pseudocode or algorithm blocks labeled as such. |
| Open Source Code | Yes | We implemented the algorithm presented in the previous section as part of the new experimental model checker MCMAS-SL[1G]. The tool, available from (MCMAS-SL[1G])... MCMAS-SL[1G] a model checker for the verification of one-goal strategy logic specifications. http://vas.doc.ic.ac.uk/software/tools/, 2014. |
| Open Datasets | No | The paper evaluates the approach on the 'fair process scheduler synthesis' problem, which seems to be a synthetic problem setup rather than using an external, publicly available dataset with a specific name or access information. |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology). |
| Hardware Specification | Yes | The experiments were run on an Intel R Core TM i7-3770 CPU 3.40GHz machine with 16GB RAM running Linux kernel version 3.8.0-35-generic. |
| Software Dependencies | No | The paper mentions 'Linux kernel version 3.8.0-35-generic' but does not provide specific version numbers for ancillary software or libraries (e.g., Python, PyTorch, or other solvers). |
| Experiment Setup | No | The paper describes the algorithms and the input specification used ('absence of starvation' SL[1G] specification) but does not provide specific experimental setup details such as hyperparameters, learning rates, batch sizes, or optimizer settings typically found in machine learning experiments. |