On the complexity of resource-bounded logics

Alechina, Natasha; Bulling, Nils; Demri, Stephane; Logan, Brian

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 19, 2016
• Publication Date: Sep 19, 2016
• Deposit Date: Sep 26, 2016
• Publicly Available Date: Sep 26, 2016
• 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
• DOI: https://doi.org/10.1007/978-3-319-45994-3_3
• Public URL: http://eprints.nottingham.ac.uk/id/eprint/37145
• Publisher URL: http://link.springer.com/chapter/10.1007%2F978-3-319-45994-3_3
• Copyright Statement: Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf
• Additional Information: In volume 9899 of Lecture Notes in Computer Science (doi:10.1007/978-3-319-45994-3_3)