Rational Verification : A Progress Report

We provide a survey of the state of the art of rational verification: the prob8 lem of checking whether a given temporal logic formula φ is satisfied in some or all 9 game theoretic equilibrium computations of a multi-agent system – that is, whether 10 the system will exhibit the behaviour φ represents under the assumption that agents 11 within the system act rationally in pursuit of their preferences. After motivating and 12 introducing the overall framework of rational verification, we discuss key results ob13 tained in the past few years as well as relevant related work in logic, AI, and Computer 14 Science. 15