@inbook{9d3ab21fdd81485890a5cbf82e1dde1f,
title = "On the complexity of resource-bounded logics",
abstract = "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.",
author = "Natasha Alechina and Nils Bulling and Stephane Demri and Brian Logan",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.",
year = "2016",
doi = "10.1007/978-3-319-45994-3_3",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "36--50",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "Germany",
}