Multi-Valued Verification of Strategic Ability

Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued ATL* (mv-ATL(less than or similar to)*), an expressive logic to specify strategic abilities in multi-agent systems. We show that our general method for model-independent translation from multi-valued to two-valued model checking cannot be directly extended to mv-ATL(less than or similar to)*. We also propose two ways of overcoming the problem. Firstly, we identify constraints on mv-ATL(less than or similar to)* formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL(less than or similar to)*. We show that, in all cases, the complexity of verification increases only polynomially when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL(less than or similar to)* and motivate its use for model checking MAS.