Natasha Alechina
On the Complexity of Resource-Bounded Logics
Alechina, Natasha; Bulling, Nils; Demri, Stephane; Logan, Brian
Authors
Nils Bulling
Stephane Demri
Brian Logan
Abstract
© Springer International Publishing Switzerland 2016. 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.
Citation
Alechina, N., Bulling, N., Demri, S., & Logan, B. (2016). On the Complexity of Resource-Bounded Logics. In Reachability problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings (36-50). https://doi.org/10.1007/978-3-319-45994-3_3
Conference Name | 10th International Workshop on Reachability Problems (RP 2016) |
---|---|
Conference Location | Aalborg, Denmark |
Start Date | Sep 19, 2016 |
End Date | Sep 21, 2016 |
Acceptance Date | Jul 11, 2016 |
Online Publication Date | Sep 12, 2016 |
Publication Date | 2016 |
Deposit Date | Sep 26, 2016 |
Publicly Available Date | Mar 29, 2024 |
Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Electronic ISSN | 1611-3349 |
Publisher | Springer |
Peer Reviewed | Peer Reviewed |
Volume | 2016-September |
Pages | 36-50 |
Series Title | Lecture Notes In Computer Science |
Series Number | 9899 |
Series ISSN | 1611-3349 |
Book Title | Reachability problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings |
ISBN | 978-3-319-45993-6 |
DOI | https://doi.org/10.1007/978-3-319-45994-3_3 |
Public URL | https://nottingham-repository.worktribe.com/output/818023 |
Publisher URL | http://link.springer.com/chapter/10.1007%2F978-3-319-45994-3_3 |
Additional Information | In volume 9899 of Lecture Notes in Computer Science (doi:10.1007/978-3-319-45994-3_3) |
Files
final-rp16.pdf
(182 Kb)
PDF
You might also like
Decidable Model Checking with Uniform Strategies
(2019)
Conference Proceeding
Strategic Responsibility Under Imperfect Information
(2019)
Conference Proceeding
Groups Versus Coalitions: On the Relative Expressivity of GAL and CAL
(2019)
Conference Proceeding
Unbounded orchestrations of transdeucers for manufacturing
(2019)
Conference Proceeding
Synthesis of orchestrations of transducers for manufacturing
(2018)
Conference Proceeding
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search