Reasoning about equilibria in game-like concurrent systems

Our aim is to develop techniques for reasoning about gamelike concurrent systems, where the components of the system act rationally and strategically in pursuit of logicallyspecified 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 operator in this logic is a path quantifier [NE]ϕ, which asserts that ϕ holds on all Nash equilibrium computations of the syste