Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
5778166 | Annals of Pure and Applied Logic | 2017 | 31 Pages |
Abstract
In this paper we study techniques for reasoning about game-like concurrent systems, where the components of the system act rationally and strategically in pursuit of logically-specified goals. Specifically, we start by presenting a computational model for such concurrent systems, and investigate its computational, mathematical, and game-theoretic properties. We then define and investigate a branching-time temporal logic for reasoning about the equilibrium properties of game-like concurrent systems. The key operator in this temporal logic is a novel path quantifier [NE]Ï, which asserts that Ï holds on all Nash equilibrium computations of the system.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Julian Gutierrez, Paul Harrenstein, Michael Wooldridge,