Playing Quantitative Games Against an Authority: On the Module Checking Problem

Module checking is a decision problem to formalize the verification of (possibly multi-agent) systems that must adapt their behavior to the input they receive from the environment, also viewed as an authority. So far, module checking has been only considered in the Boolean setting, which does not capture the different levels of quality inherent to complex systems (e.g., systems dealing with quantitative utilities or sensor inputs). In this paper, we address this issue by proposing quantitative module checking. We study the problem in the quantitative and multi-agent setting, which enables the verification of different levels of satisfaction in relation to a specification. We consider specifications given in Quantitative Alternating-time Temporal logics and investigate their complexity and expressivity.