Combining quantitative and qualitative reasoning in concurrent multi-player games
Nils Bulling, Valentin Goranko
Abstract
Abstract We propose a general framework for modelling and formal reasoning about multi-agent systems and, in particular, multi-stage games where both quantitative and qualitative objectives and constraints are involved. Our models enrich concurrent game models with payoffs and guards on actions associated with each state of the model and propose a quantitative extension of the logic $${\textsf {ATL}}^{*}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>ATL</mml:mi> </mml:mrow> <mml:mrow> <mml:mrow/> <mml:mo>∗</mml:mo> </mml:mrow> </mml:msup> </mml:math> that enables the combination of quantitative and qualitative reasoning. We illustrate the framework with some detailed examples. Finally, we consider the model-checking problems arising in our framework and establish some general undecidability and decidability results for them.