Combining Quantitative and Qualitative Reasoning in Concurrent Multi-player Games

We propose and study a general framework for modelling and formal reasoning about multi-agent systems and, in particular, multistage 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. We propose a quantitative extension of the logic ATL * that enables combination of quantitative and qualitative reasoning. We illustrate the framework with some examples and then consider the model-checking problems arising in it and establish some general undecidability and decidability results for them.