Reasoning about equilibria in game-like concurrent systems

详细信息    查看全文

• 作者：Julian Gutierrez ; ^{Julian.Gutierrez@cs.ox.ac.uk} ; Paul Harrenstein ; Michael Wooldridge
• 关键词：03B44 ; 03B70 ; 68T27 ; 91A40
• 刊名：Annals of Pure and Applied Logic
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：168
• 期：2
• 页码：373-403
• 全文大小：780 K
• 卷排序：168

文摘

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]φ[NE]φ, which asserts that φ holds on all Nash equilibrium computations of the system.