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\\(\\pm \\)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\\(\\pm \\)ATL\\(^*\\) is decidable by a reduction to parity games, and show how to synthesise values for resource parameters.