On Computational Tractability for Rational Verification
Authors: Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge
IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper we show that the complexity of rational verification can be greatly reduced by restricting specifications to GR(1), a fragment of LTL that can represent most response properties of reactive systems. We also provide improved complexity results for rational verification when considering players goals given by mean-payoff utility functions arguably the most widely used quantitative objective for agents in concurrent and multiagent systems. In particular, we show that for a number of relevant settings, rational verification can be done in polynomial space or even in polynomial time. |
| Researcher Affiliation | Academia | Julian Gutierrez1 , Muhammad Najib1 , Giuseppe Perelli2 , Michael Wooldridge1 1Department of Computer Science, University of Oxford, UK 2Department of Informatics, University of Leicester, UK |
| Pseudocode | Yes | Algorithm 1: E-NASH of GR(1) games. and Algorithm 2: E-NASH of mp games. |
| Open Source Code | No | The paper does not provide any links to open-source code or state that the code for the described methodology is publicly available. |
| Open Datasets | No | This is a theoretical paper focusing on complexity results for formal verification problems. It does not involve empirical experiments with datasets, training, or public dataset availability. |
| Dataset Splits | No | This is a theoretical paper and does not involve empirical validation on datasets, thus no dataset split information for validation is provided. |
| Hardware Specification | No | The paper is theoretical and focuses on computational complexity. It does not describe any specific hardware used for experiments. |
| Software Dependencies | No | The paper describes theoretical algorithms and reductions. It does not mention any specific software dependencies with version numbers needed to replicate the work. |
| Experiment Setup | No | The paper is theoretical and focuses on complexity analysis and algorithm design. It does not describe an empirical experimental setup with hyperparameters or training configurations. |