Parameterised Resource-Bounded ATL

It is often advantageous to be able to extract resource requirements in resource logics of strategic ability, rather than to verify whether a fixed resource requirement is sufficient for achieving a goal. We study Parameterised Resource-Bounded Alternating Time Temporal Logic where parameter extraction is possible. We give a parameter extraction algorithm and prove that the model-checking problem is 2EXPTIMEcomplete.

Authors

• Natasha Alechina
• Stéphane Demri CNRS, LMF, ENS Paris-Saclay, France
• Brian Logan

Keywords

No keywords are indexed for this paper.