Quantitative rational verification - Steeples, T (2023)
Rational verification asks whether certain temporal properties hold within the equilibria of multi-agent systems. Typically, the literature considers games where the agents traverse some concurrent game structure (or some succinct representation of it), with player goals and specifications given by LTL formulae. Whilst this is an effective framework for reasoning about a variety of different systems, it has two clear shortcomings --- it assumes that agents are unrestricted in choosing their actions, and it only allows two possible player preferences over outcomes: a satisfied temporal goal and an unsatisfied one. Whilst this is sufficient for verifying binary properties (such as safety, fairness and liveness) of a system where agents can act arbitrarily, this framework lacks the ability to differentiate between non-functional behaviours of resource-constrained systems.