On computational tractability for rational verification
Rational verification involves checking which temporal logic properties hold of a concurrent/multiagent system, under the assumption that agents in the system choose strategies in game theoretic equilibrium. Rational verification can be understood as a counterpart of model checking for multiagent sy...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Published: |
International Joint Conferences on Artificial Intelligence
2019
|
| _version_ | 1797105077625815040 |
|---|---|
| author | Gutierrez, J Najib, M Perelli, G Wooldridge, M |
| author_facet | Gutierrez, J Najib, M Perelli, G Wooldridge, M |
| author_sort | Gutierrez, J |
| collection | OXFORD |
| description | Rational verification involves checking which temporal logic properties hold of a concurrent/multiagent system, under the assumption that agents in the system choose strategies in game theoretic equilibrium. Rational verification can be understood as a counterpart of model checking for multiagent systems, but while model checking can be done in polynomial time for some temporal logic specification languages such as CTL, and polynomial space with LTL specifications, rational verification is much more intractable: 2EXPTIMEcomplete with LTL specifications, even when using explicit-state system representations. 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. |
| first_indexed | 2024-03-07T06:42:23Z |
| format | Conference item |
| id | oxford-uuid:f9bc4d0e-e2b6-4035-89fb-ffdce2060e01 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:42:23Z |
| publishDate | 2019 |
| publisher | International Joint Conferences on Artificial Intelligence |
| record_format | dspace |
| spelling | oxford-uuid:f9bc4d0e-e2b6-4035-89fb-ffdce2060e012022-03-27T13:00:06ZOn computational tractability for rational verificationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:f9bc4d0e-e2b6-4035-89fb-ffdce2060e01Symplectic Elements at OxfordInternational Joint Conferences on Artificial Intelligence2019Gutierrez, JNajib, MPerelli, GWooldridge, MRational verification involves checking which temporal logic properties hold of a concurrent/multiagent system, under the assumption that agents in the system choose strategies in game theoretic equilibrium. Rational verification can be understood as a counterpart of model checking for multiagent systems, but while model checking can be done in polynomial time for some temporal logic specification languages such as CTL, and polynomial space with LTL specifications, rational verification is much more intractable: 2EXPTIMEcomplete with LTL specifications, even when using explicit-state system representations. 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. |
| spellingShingle | Gutierrez, J Najib, M Perelli, G Wooldridge, M On computational tractability for rational verification |
| title | On computational tractability for rational verification |
| title_full | On computational tractability for rational verification |
| title_fullStr | On computational tractability for rational verification |
| title_full_unstemmed | On computational tractability for rational verification |
| title_short | On computational tractability for rational verification |
| title_sort | on computational tractability for rational verification |
| work_keys_str_mv | AT gutierrezj oncomputationaltractabilityforrationalverification AT najibm oncomputationaltractabilityforrationalverification AT perellig oncomputationaltractabilityforrationalverification AT wooldridgem oncomputationaltractabilityforrationalverification |