Rational Verification: From Model Checking to Equilibrium Checking
Authors: Michael Wooldridge, Julian Gutierrez, Paul Harrenstein, Enrico Marchioni, Giuseppe Perelli, Alexis Toumi
AAAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We give an overview of a prototype software tool for rational verification: the E AG L E system takes as input a R E AC T I V E M O D U L E S specification of a set of agents (Alur and Henzinger 1999), a goal for each agent, specified as a formula of the temporal logic CTL (Emerson 1990), and a collection of strategies, one for each agent in the system; the system then checks whether the strategies form a Nash equilibrium. We now describe a prototype tool we have developed as a proof of concept for equilibrium checking. We now present a case study based on the system presented in (Fisman, Kupferman, and Lustig 2010). One can show and formally verify using E A G L E that this game has a Nash equilibrium where no player gets its goal achieved, and another that is Pareto optimal, where both players get their goal achieved. |
| Researcher Affiliation | Academia | Michael Wooldridge, Julian Gutierrez, Paul Harrenstein, Enrico Marchioni, Giuseppe Perelli, Alexis Toumi Department of Computer Science, University of Oxford |
| Pseudocode | No | The paper presents RML module definitions (e.g., "module m0 controls u0, d0 init [] -> u 0 := , d 0 := update [] -> u 0 := , d 0 :=") which are concrete examples in a specific language for modeling agents, rather than general pseudocode or algorithm blocks describing a computational procedure. |
| Open Source Code | No | The paper mentions a prototype tool called E AG L E but does not provide any link or explicit statement about its public availability or open-source status. |
| Open Datasets | No | The paper uses a "case study based on the system presented in (Fisman, Kupferman, and Lustig 2010)" to demonstrate its prototype tool. This case study involves formal system specifications and agent goals, not a traditional dataset used for training, validation, or testing in an empirical study context. |
| Dataset Splits | No | The paper uses a case study involving a formal system model rather than a dataset, so there is no mention of dataset splits (training, validation, test) relevant for reproducibility. |
| Hardware Specification | No | The paper does not provide any specific hardware details (e.g., GPU/CPU models, memory) used for running the described case study or prototype tool. |
| Software Dependencies | No | The paper mentions "R E AC T I V E M O D U L E S Language (R M L)" and the prototype tool "E AG L E" but does not specify version numbers for these or any other software dependencies. |
| Experiment Setup | No | The paper describes the formal setup of the multi-agent system (RML modules, CTL formulas for goals) for the case study, but it does not include details on hyperparameters, optimizer settings, or other system-level training configurations typically found in experimental setups. |