On the complexity of resource-bounded logics
We revisit decidability results for resource-bounded logics and use decision problems on vector addition systems with states (VASS) in order to establish complexity characterisations of (decidable) model checking problems. We show that the model checking problem for the logic RB+-ATL is 2EXPTIME-com...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Published: |
Elsevier
2018
|
| Online Access: | https://eprints.nottingham.ac.uk/49359/ |
| _version_ | 1848797980355723264 |
|---|---|
| author | Alechina, N. Bulling, N. Demri, S. Logan, B. |
| author_facet | Alechina, N. Bulling, N. Demri, S. Logan, B. |
| author_sort | Alechina, N. |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | We revisit decidability results for resource-bounded logics and use decision problems on vector addition systems with states (VASS) in order to establish complexity characterisations of (decidable) model checking problems. We show that the model checking problem for the logic RB+-ATL is 2EXPTIME-complete by using recent results on alternating VASS (and in EXPTIME when the number of resources is bounded). Moreover, we establish that the model checking problem for RBTL is EXPSPACE-complete. The problem is decidable and of the same complexity for RBTL*, proving a new decidability result as a by-product of the approach. When the number of resources is bounded, the problem is in PSPACE. We also establish that the model checking problem for RB+-ATL*, the extension of RB+-ATL with arbitrary path formulae, is decidable by a reduction to parity games for single-sided VASS (a variant of alternating VASS). Furthermore, we are able to synthesise values for resource parameters. Hence, the paper establishes formal correspondences between model checking problems for resource bounded logics advocated in the AI literature and decision problems on alternating VASS, paving the way for more applications and cross-fertilizations. |
| first_indexed | 2025-11-14T20:12:30Z |
| format | Article |
| id | nottingham-49359 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T20:12:30Z |
| publishDate | 2018 |
| publisher | Elsevier |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-493592020-05-04T19:29:34Z https://eprints.nottingham.ac.uk/49359/ On the complexity of resource-bounded logics Alechina, N. Bulling, N. Demri, S. Logan, B. We revisit decidability results for resource-bounded logics and use decision problems on vector addition systems with states (VASS) in order to establish complexity characterisations of (decidable) model checking problems. We show that the model checking problem for the logic RB+-ATL is 2EXPTIME-complete by using recent results on alternating VASS (and in EXPTIME when the number of resources is bounded). Moreover, we establish that the model checking problem for RBTL is EXPSPACE-complete. The problem is decidable and of the same complexity for RBTL*, proving a new decidability result as a by-product of the approach. When the number of resources is bounded, the problem is in PSPACE. We also establish that the model checking problem for RB+-ATL*, the extension of RB+-ATL with arbitrary path formulae, is decidable by a reduction to parity games for single-sided VASS (a variant of alternating VASS). Furthermore, we are able to synthesise values for resource parameters. Hence, the paper establishes formal correspondences between model checking problems for resource bounded logics advocated in the AI literature and decision problems on alternating VASS, paving the way for more applications and cross-fertilizations. Elsevier 2018-02-02 Article PeerReviewed Alechina, N., Bulling, N., Demri, S. and Logan, B. (2018) On the complexity of resource-bounded logics. Theoretical Computer Science . ISSN 0304-3975 https://www.sciencedirect.com/science/article/pii/S0304397518300665 doi:10.1016/j.tcs.2018.01.019 doi:10.1016/j.tcs.2018.01.019 |
| spellingShingle | Alechina, N. Bulling, N. Demri, S. Logan, B. On the complexity of resource-bounded logics |
| title | On the complexity of resource-bounded logics |
| title_full | On the complexity of resource-bounded logics |
| title_fullStr | On the complexity of resource-bounded logics |
| title_full_unstemmed | On the complexity of resource-bounded logics |
| title_short | On the complexity of resource-bounded logics |
| title_sort | on the complexity of resource-bounded logics |
| url | https://eprints.nottingham.ac.uk/49359/ https://eprints.nottingham.ac.uk/49359/ https://eprints.nottingham.ac.uk/49359/ |