On the complexity of resource-bounded logics
We revisit decidability results for resource-bounded logics and use decision problems for vector addition systems with states (VASS) to characterise the complexity of (decidable) model-checking problems. We show that the model-checking problem for the logic RB+-ATL is 2EXPTIME-complete by using rec...
| Main Authors: | , , , |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
2016
|
| Online Access: | https://eprints.nottingham.ac.uk/37145/ |
| _version_ | 1848795400694136832 |
|---|---|
| author | Alechina, Natasha Bulling, Nils Demri, Stephane Logan, Brian |
| author_facet | Alechina, Natasha Bulling, Nils Demri, Stephane Logan, Brian |
| author_sort | Alechina, Natasha |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | We revisit decidability results for resource-bounded logics and use decision problems for vector addition systems with states (VASS) to characterise the complexity 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.
In addition, we establish that the model-checking problem for RBTL is decidable and has the same complexity as for RBTL* (the extension of RBTL with arbitrary path formulae), namely EXPSPACE-complete, proving a new decidability result as a by-product of the approach. Finally, we establish that the model-checking problem for RB+-ATL* is decidable by a reduction to parity games, and show how to synthesise values for resource parameters. |
| first_indexed | 2025-11-14T19:31:29Z |
| format | Conference or Workshop Item |
| id | nottingham-37145 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:31:29Z |
| publishDate | 2016 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-371452020-05-04T18:12:33Z https://eprints.nottingham.ac.uk/37145/ On the complexity of resource-bounded logics Alechina, Natasha Bulling, Nils Demri, Stephane Logan, Brian We revisit decidability results for resource-bounded logics and use decision problems for vector addition systems with states (VASS) to characterise the complexity 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. In addition, we establish that the model-checking problem for RBTL is decidable and has the same complexity as for RBTL* (the extension of RBTL with arbitrary path formulae), namely EXPSPACE-complete, proving a new decidability result as a by-product of the approach. Finally, we establish that the model-checking problem for RB+-ATL* is decidable by a reduction to parity games, and show how to synthesise values for resource parameters. 2016-09-13 Conference or Workshop Item PeerReviewed Alechina, Natasha, Bulling, Nils, Demri, Stephane and Logan, Brian (2016) On the complexity of resource-bounded logics. In: 10th International Workshop on Reachability Problems (RP 2016), 19-12 September 2016, Aalborg, Denmark. http://link.springer.com/chapter/10.1007%2F978-3-319-45994-3_3 |
| spellingShingle | Alechina, Natasha Bulling, Nils Demri, Stephane Logan, Brian 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/37145/ https://eprints.nottingham.ac.uk/37145/ |