Reasoning about Equilibria in Game-Like Concurrent Systems

Our aim is to develop techniques for reasoning about game-like concurrent systems, where the components of the sys-tem act rationally and strategically in pursuit of logically-specified goals. We first present a computational model for such systems, and investigate its properties. We then define and investigate a branching-time logic for reasoning about the equilibrium properties of such systems. The key opera-tor in this logic is a path quantifier [NE]', which asserts that ' holds on all Nash equilibrium computations of the system.