In the context of multi-agent systems, the rational verification problem is\nconcerned with checking which temporal logic properties will hold in a system\nwhen its constituent agents are assumed to behave rationally and strategically\nin pursuit of individual objectives. Typically, those objectives are expressed\nas temporal logic formulae which the relevant agent desires to see satisfied.\nUnfortunately, rational verification is computationally complex, and requires\nspecialised techniques in order to obtain practically useable implementations.\nIn this paper, we present such a technique. This technique relies on a\nreduction of the rational verification problem to the solution of a collection\nof parity games. Our approach has been implemented in the Equilibrium\nVerification Environment (EVE) system. The EVE system takes as input a model of\na concurrent/multi-agent system represented using the Simple Reactive Modules\nLanguage (SRML), where agent goals are represented as Linear Temporal Logic\n(LTL) formulae, together with a claim about the equilibrium behaviour of the\nsystem, also expressed as an LTL formula. EVE can then check whether the LTL\nclaim holds on some (or every) computation of the system that could arise\nthrough agents choosing Nash equilibrium strategies; it can also check whether\na system has a Nash equilibrium, and synthesise individual strategies for\nplayers in the multi-player game. After presenting our basic framework, we\ndescribe our new technique and prove its correctness. We then describe our\nimplementation in the EVE system, and present experimental results which show\nthat EVE performs favourably in comparison to other existing tools that support\nrational verification.\n