Adaptive Strategies for GR(1) Games
Logic in Computer ScienceFormal Languages and Automata TheoryComputer Science and Game Theory
Summary
The authors study a game between two players, where one player (Eve) must fulfill certain ongoing guarantees as long as the other player (Adam) keeps making certain assumptions true. Instead of using fixed plans that can be too cautious or give up too easily, the authors create a new adaptive method where Eve watches what Adam actually does and changes her plan on the fly to meet as many guarantees as possible. They develop a way for Eve to estimate in real time which assumptions will hold and choose the best strategy accordingly. Their method is more efficient and better at handling broken assumptions than previous approaches.
GR(1) gamestwo-player gamesliveness propertiesassumptions and guaranteesadaptive strategiesmonitoringrandomized strategiesformal verificationtemporal logicruntime adaptation
Authors
S. Krishna, Kaushik Mallik, Abhilasha Sharma Suman
Abstract
We consider two-player GR(1) games on graphs, where the system player Eve must satisfy \[ \Box\Diamond A_1\land\cdots\land\Box\Diamond A_m \;\implies\; \Box\Diamond G_1\land\cdots\land\Box\Diamond G_n \] against the environment player Adam. Here $A_1,\ldots,A_m$ are assumptions on the environment, $G_1,\ldots,G_n$ are guarantees the system must provide, and $\Box\Diamond S$ denotes ``always eventually $S$''. Traditional static strategies are overly conservative: they may actively violate assumptions to trivially satisfy the implication, or abandon all guarantees when any assumption is violated. Existing methods to prevent such behaviors incur doubly exponential blowup. We introduce an adaptive framework treating Adam as a non-adversarial agent with unknown objectives. Eve monitors which assumptions Adam actually meets and adapts her strategy at runtime to maximize satisfied guarantees. Central to our approach is a novel algorithm for monitoring liveness properties $\Box\Diamond S$, enabling Eve to maintain real-time likelihood estimates of which assumptions will be fulfilled. Eve pre-computes strategies optimal for different assumption subsets, deploying a probability distribution over them that dynamically adjusts based on monitor outputs. We prove that when assumptions are violated, Eve's randomized adaptive strategy converges asymptotically to the deterministic strategy maximizing guarantees. A prototype demonstrates effectiveness and superior computational performance compared to the state of the art.