PaperlayerView exact revision on arXiv

Source-linked AI summary

Adaptive Strategies for GR(1) Games

S. Krishna, Kaushik Mallik, Abhilasha Sharma Suman

arXiv:2608.28391v1cs.LOcs.FLcs.GT

TL;DR

Standard GR(1) strategies can let Eve violate assumptions or abandon guarantees under partial violations, while addressing both issues naively incurs doubly exponential complexity. The paper combines an exponential strategy library with runtime liveness monitoring and randomized adaptation, proving asymptotic convergence to the optimal response under non-adversarial environments.

  • Problem

    Standard GR(1) winning strategies separately permit active assumption violation or guarantee abandonment, while prior methods do not address both limitations together.

  • Method

    A static phase precomputes optimal strategies for assumption subsets, while an adaptive phase monitors liveness and mixes those strategies according to observed behavior.

  • Results

    Under non-adversarial Adam behavior, the randomized adaptive strategy almost surely concentrates on the static strategy corresponding to the assumptions Adam fulfills, with exponentially smaller time and strategy complexity than the naïve baseline.

  • Takeaways & Limitations

    Gracefully robust strategies provide an adaptive response to partial assumption violations while retaining optimal guarantees asymptotically.

  • Takeaways & Limitations

    Combining graceful and robust strategies naively incurs doubly exponential complexity, and the lower complexity bound remains open.

Abstract

from arXiv · show

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.

1 Introduction

The paper addresses conservative GR(1) strategies by combining graceful, robust behavior with runtime adaptation to non-adversarial environments. Eve precomputes strategies for assumption subsets, monitors liveness assumptions, and probabilistically adapts toward the strategy matching the assumptions Adam fulfills.

  • Motivation: Standard GR(1) strategies may violate assumptions or abandon all guarantees when only some assumptions fail.Graceful strategies address active violation, while robust strategies address guarantee abandonment, but prior work does not address both together.
  • Guarantees: The paper reports exponentially smaller time and strategy complexity than the naïve graceful-robust baseline.The baseline combination has doubly exponential complexity in the number of assumptions and guarantees, motivating the library-based design.
  • Adaptive framework: Offline synthesis builds StrLib for every assumption subset, with each strategy maximizing guarantees when that subset is fulfilled.If Eve knew the fulfilled subset, she could deploy its corresponding library strategy directly.
  • Adaptive framework: Online monitors estimate individual and subset-level liveness likelihoods, producing a time-varying distribution over library strategies.The distribution is used to sample a strategy at each step, while the asymptotic monitor’s verdict converges to 1 for satisfaction and 0 otherwise.
  • Guarantees: The adaptive strategy almost surely concentrates on StrLib(Ainf), the optimal static strategy for Adam’s infinitely fulfilled assumptions.This convergence holds for arbitrary Adam strategies under the paper’s non-adversarial assumptions.
  • Motivation: The framework models Adam as non-adversarial and learns at runtime which assumptions he fulfills infinitely often.The framework assumes the fulfilled-assumption subset is independent of Eve’s graceful strategy and that visits to fulfilled assumptions have bounded gaps.

Contributions.

The paper introduces adaptive GR(1) strategies for non-adversarial environments, combining verified static strategy libraries with runtime adaptation. Its contributions include asymptotic liveness monitoring, probabilistic strategy mixing, convergence guarantees, and a prototype evaluation.

  • Contributions: The convergence proof shows that adaptive mixing asymptotically concentrates on the optimal deterministic strategy.The result concerns adaptation to assumption violations in the proposed framework.
  • Contributions: The Grace prototype reports exponential speedups over the baseline and fast convergence in practice.The evaluation is presented as evidence of computational performance and practical convergence.
  • Contributions: The framework adapts GR(1) strategies to observed environment behavior while retaining formal guarantees from verified static strategies.It differs from learning-based approaches by combining static verification with adaptive mixing.
  • Contributions: An asymptotic liveness monitor estimates whether assumptions are fulfilled, with verdicts converging to the true satisfaction value under mild frequency assumptions.The monitor addresses the non-monitorability of liveness properties without relying on safety-property relaxations.
  • Contributions: The adaptive framework learns which assumptions hold and deploys the corresponding optimal strategies through probabilistic mixing.This connects assumption learning with strategy selection in the runtime phase.

2 Preliminaries

This section defines graph games, paths, strategies, and temporal specifications used throughout the paper. It then formalizes GR(1) objectives, partial assumption and guarantee satisfaction, and obliging games.

  • Game graphs and paths: A game graph partitions vertices between Eve and Adam, who move a token along directed edges to generate finite or infinite paths.Graphs are assumed to have no dead-end vertices.
  • Strategies: Eve’s strategy maps each finite path ending at an Eve vertex to a successor, with memoryless and finite-memory strategies defined by their dependence on history.The strategy classes are represented by Π_E, Π_M^E, and Π_FM^E, with memoryless strategies contained in finite-memory strategies.
  • Specifications: Reachability, safety, Büchi, co-Büchi, generalized Büchi, and generalized Rabin specifications classify infinite paths by recurring or bounded visits to designated vertex sets.The generalized Rabin specification combines generalized Büchi requirements with co-Büchi requirements.
  • GR(1) specifications: A GR(1) specification is satisfied when some environment assumption is violated finitely often or all system guarantees are visited infinitely often.A path’s A_inf and G_inf record the largest subsets of assumptions and guarantees fulfilled infinitely often.
  • Obliging games: Obliging games require Eve to win a strong specification while preserving, after every compliant finite history, some Adam strategy that fulfills a weak specification.Winning strategies are prefix-independent for liveness specifications under the stated construction.

3 Gracefully Robust Strategies for GR(1) Specifications

Gracefully robust strategies address both major shortcomings of standard GR(1) strategies: Eve violating assumptions and abandoning guarantees when assumptions fail. The section formalizes these strategies, analyzes the doubly exponential naïve approach, and introduces terminal robustness as a practical relaxation.

  • Motivation: Standard GR(1) strategies may violate assumptions or abandon all guarantees when any assumption is violated; prior graceful and robust strategies address these separately.Gracefully robust strategies combine both requirements.
  • Graceful strategies: A graceful strategy wins its selected GR(1) sub-specification while allowing Adam to visit every assumption infinitely often.This is formalized through an obliging game with a Büchi objective for all assumptions.
  • Graceful robustness: A gracefully robust strategy is graceful and is not dominated by another graceful strategy from the initial vertex.Dominance compares strategies by the assumptions they permit Adam to fulfill and the guarantees they fulfill.
  • Naïve synthesis: The naïve synthesis approach inherits doubly exponential time and memory complexity from robust-strategy encodings and their generalized Büchi translations.The bound uses 𝑚 assumptions, 𝑛 guarantees, and k = min(𝑚,𝑛), with exponential factors Y and Z.
  • Practical relaxation: Terminal graceful robustness forgives domination in transient vertices while requiring robustness in every subgame where play settles in the long term.Every gracefully robust strategy is terminally gracefully robust.

4 Static Design of a Library of Individual Optimal Strategies

The static phase constructs a strategy library mapping every assumption subset to a finite-memory strategy that maximizes achievable guarantees while remaining graceful. Its construction is sound and uses single-exponential time and memory rather than the baseline’s doubly exponential complexity.

  • Optimality criteria: Optimality requires gracefulness, bounded-time assumption fulfillment by some Adam strategy, staying within the original winning region, and maximizing guarantees against A′.The final condition rules out another strategy satisfying the first three conditions while fulfilling more guarantees.
  • Library definition: The library StrLib maps each assumption subset A′ ⊆ A to an optimal finite-memory strategy for the assumptions in A′.These strategies are later mixed randomly during adaptive deployment.
  • Construction: Algorithm 1 incrementally computes Γ by solving obliging games for guarantee subsets in decreasing order and assumption subsets in increasing order.Each solution is stored for applicable vertices and assumption supersets when no strategy has yet been assigned.
  • Construction: Γ is converted into StrLib by stitching vertex-dependent optimal strategies into strategies indexed only by assumption subsets.The stitching preserves optimality by using the first strategy assigned to each vertex and assumption subset.
  • Complexity: Single-exponential time and memory replace the baseline’s doubly exponential bounds for the static library construction.The improvement applies under Assumption 1 and computes terminally gracefully robust strategies rather than gracefully robust strategies in the stronger baseline sense.

5 Adaptive Design of Terminally Gracefully Robust Policies

The adaptive design combines liveness monitoring with probabilistic mixing over precomputed strategies, allowing Eve to adjust to the assumptions Adam fulfills. Under stated conditions, the monitor and strategy converge toward the optimal policy for the fulfilled assumptions almost surely.

  • Adaptive strategy motivation: A deterministic phase-based alternative can achieve the maximum possible guarantees, but requires infinite memory and increasingly sparse successful matches.Its phases grow in length, so the correct action is selected in increasingly distant windows.
  • Adaptive strategy construction: The adaptive construction precomputes optimal strategies for assumption subsets, then dynamically mixes them using runtime monitor estimates.The static library contains one strategy for each possible fulfilled-assumption subset.
  • Liveness monitoring: The novel Büchi monitor outputs quantitative satisfaction estimates that converge to 1 when the property holds and to 0 otherwise under mild frequency assumptions.The construction uses local monitors for individual assumptions and a global monitor for their union.
  • Liveness monitoring: The liveness monitor resets its score on visits to an assumption state, decays it otherwise, and reduces the decay rate after repeated visits.If the assumption is visited only finitely often, the score converges to 0; under suitable regularity, soundness is established.
  • Randomized policy mixing: The adaptive strategy samples static policies according to a time-varying distribution, yielding a probabilistic strategy whose weights identify the fulfilled assumption subset.For the relevant subset, its weight diverges while other subset weights remain comparatively suppressed.
  • Theoretical guarantees: Under Assumption 1, the randomized strategy is terminally gracefully robust almost surely, and it converges to the optimal library strategy for the assumptions fulfilled by Adam.When all assumptions hold, the limiting mixture fulfills all guarantees; violated assumptions make the GR(1) implication true automatically.

6 Experiments

The experiments evaluate Grace against the Bloem et al. baseline and measure how quickly its adaptive strategy identifies fulfilled assumptions. Grace scales better on larger benchmarks and converges within a few hundred steps.

  • RQ1: Comparison with Bloem et al.: Grace completes every benchmark within the time and memory limits, while the baseline times out on Scheduler(3, 3).The comparison uses the same front end and back end, with synthesis capped at one hour and 5 GB of memory.
  • RQ1: Comparison with Bloem et al.: Grace is faster on 8 of 12 benchmarks overall and overtakes the baseline as benchmark size grows.Its richer encoding creates overhead on small instances, but better asymptotic scaling dominates at larger sizes.
  • RQ2: Convergence: The adaptive strategy converges within a few hundred steps across all benchmarks.Convergence is measured as the first time the probability of selecting StrLib(Ainf) exceeds 0.99 and remains above that threshold, averaged over 100 runs.
  • RQ2: Convergence: 97 →198 steps on Lift(2, 2) →(3, 3), as convergence time roughly doubles when the number of assumptions increases.The adaptive strategy must rule out more candidate subsets before probability mass concentrates on Ainf.
  • RQ2: Convergence: The correct strategy is deployed almost always despite clipping monitor probabilities away from exact 0 and 1.The clipping keeps incorrect strategies rarely samplable under finite precision.
  • Overall findings: The results show that the theoretical advantages of the framework manifest concretely rather than only asymptotically.The authors characterize the experiments as establishing that the framework is not vacuous, while identifying the theory as the main contribution.

7 Conclusion

The paper introduces gracefully robust GR(1) strategies with a two-phase synthesis and adaptation framework. Future work targets larger specifications, faster convergence, and broader online adaptation under uncertainty.

  • Conclusion: Gracefully robust strategies address active assumption violation and guarantee abandonment under partial violations.The approach is designed for GR(1) games where not all environment assumptions are met.
  • Conclusion: Because graceful robustness is doubly exponential to compute, the paper uses terminal graceful robustness and an exponential strategy library.The adaptive phase mixes library strategies at runtime and provably converges to the optimal response.
  • Future work: Future work includes optimizing Grace for larger specifications and accelerating convergence with decay schedules or informed priors.The paper also identifies online learning and controller adaptation under uncertain specifications or environment models as broader directions.

Appendix

The appendix collects deferred proofs, a generalization of the liveness-monitor construction, probability background, and benchmark descriptions.

  • Appendix contents: The appendix contains deferred proofs for complexity and robustness claims concerning gracefully robust strategies.It includes Theorem 3.6, Corollary 3.7, and the implication from global graceful robustness to terminal graceful robustness.
  • Appendix contents: It also provides a generalized liveness-monitor construction, probability background, and benchmark descriptions used in the evaluation.These materials support the technical sections and experimental setup.

A Proofs of Claims in Section 3

The appendix establishes complexity bounds for robust and gracefully robust strategies and proves that graceful robustness implies terminal graceful robustness. It derives the bounds by reducing requirements to Streett games.

  • Complexity bounds: The robust-strategy synthesis bound is doubly exponential in the numbers of assumptions m and guarantees n.Theorem 3.6 gives the time and memory bounds using Y = 2^O(m2^m) and Z = 2^O(n2^n).
  • Proof strategy: Each requirement becomes a generalized reactivity game with Y and Z generalized-Büchi conjuncts and rank l ≤ k.The resulting game is solved through a Streett-game reduction whose state and edge sizes scale with Y^l Z^l.
  • Proof strategy: The obliging-game reduction yields a regular Streett game with l + m Streett pairs.The Streett-game solver contributes the stated time and memory costs, and multiplying across requirements gives the overall bound.
  • Robustness implication: Every gracefully robust strategy is terminally gracefully robust.The proof constructs a dominating strategy on the limit subgame, using tail invariance because finite prefixes do not affect infinitely recurring vertices.
  • Robustness implication: The constructed strategy preserves or improves the original strategy against every Adam strategy, contradicting graceful robustness if terminal graceful robustness failed.The comparison is established by combining the original strategy before entering the limit subgame with a dominating obliging-game strategy afterward.

B Proofs of Claims in Section 4

Section 4 proves that the strategy library contains optimal strategies for every fulfilled-assumption subset and establishes the algorithm's complexity bounds. The proof uses nested assumption–guarantee cases, trap regions, and rank-based induction.

  • For every assumption subset A*, StrLib(A*) is optimal from every vertex in the graceful winning region.
  • Obliging-game winning regions are monotone: enlarging assumptions or reducing guarantees can only enlarge the winning region.
  • The induction constructs strategies across rank regions by using an obliging-game strategy until entering a lower-rank region, then resetting and switching strategies.The lower-rank region is a trap for Adam, and finite prefixes become irrelevant after entry.
  • Each Solve_Obliging_Game instance reduces to a Streett game with m+1 pairs, O(|V|·m·n) vertices, and O(|E|·m·n) edges.
  • Algorithm 1 performs 2^(m+n) nested-loop iterations, each invoking Solve_Obliging_Game and updating Γ over assumption supersets.
  • The library stores at most 2^(m+n) sub-strategies, each of size at most (m+1)!, yielding the stated memory bound.

C Proofs of Claims in Section 5

Section 5 establishes asymptotic correctness of the liveness monitor and the randomized adaptive strategy. Under the stated recurrence assumption, monitor scores distinguish recurring assumptions from assumptions eventually abandoned, while strategy selection converges almost surely to an optimal library strategy.

  • Algorithm 2 is an asymptotic liveness monitor: recurring assumptions with constant hitting time receive scores converging to 1, while nonrecurring assumptions receive scores converging to 0.The exact hitting-time bound need not be known to the monitor.
  • The monitor resets an assumption's score on visits and otherwise discounts it by the current decay rate, whose rate is itself attenuated after visits.
  • Within sufficiently long windows, a static strategy is selected for N consecutive steps with a positive lower bound on probability.
  • The adaptive scheduler assigns probabilities to static strategies using their current weights and a normalizing sum over assumption subsets.
  • Because such blocks occur infinitely often almost surely and only 2^m static strategies exist, at least one strategy is repeatedly activated for arbitrarily long blocks.
  • The randomized strategy is terminally gracefully robust almost surely and converges to StrLib(Ainf), which is optimal for the assumptions fulfilled infinitely often.

D Generalization of Asymptotic Liveness Monitors to Recurring Events with Sub-Exponential Hitting Times

Section D extends the liveness-monitoring result from constant to sub-exponential hitting times. Exponential decay of the monitor's attenuation factor dominates sub-exponential gaps between recurring visits, preserving asymptotic detection.

  • The sub-exponential condition is sufficient but not necessary for infinitely frequent visits: exponential inter-visit gaps still satisfy Büchi recurrence while violating the condition.
  • The generalized monitor is sound for paths where each recurring event has sub-exponential hitting time, without requiring the exact hitting-time function.
  • After the k-th visit, the discount factor becomes λ^kα0, while the estimate remains bounded below by (1−λ^kα0)^(2^o(k)).
  • Because λ^k dominates the sub-exponential gap, (1−λ^kα0)^(2^o(k)) tends to 1 as recurring visits continue.
  • After the final visit, the estimate decays constantly, preserving the monitor's separation of recurring and nonrecurring events.

E Known results in probability theory

Section E recalls the Borel–Cantelli lemmas and Lévy's extension, which characterize when infinitely many events occur almost surely from unconditional or conditional probability sums.

  • If the sum of event probabilities is finite, the probability that infinitely many events occur is zero.
  • For independent events with divergent total probability, infinitely many events occur almost surely.
  • Lévy's extension replaces independence with a divergent sum of conditional probabilities relative to a filtration.

F Experiment Benchmarks Description

The experiments use GR(1) benchmarks covering concurrency, resource sharing, service scheduling, routing, buffering, and process allocation, with explicit liveness assumptions and guarantees.

  • Dining Philosophers: Dining Philosophers models philosophers alternating between thinking and eating while requiring access to two neighboring forks.The benchmark includes instances with n=2 and n=3, using 2 and 3 assumptions and guarantees, respectively.
  • Dining Philosophers: Dining Philosophers guarantees eventual eating for each philosopher and prevents adjacent philosophers from eating simultaneously.The stated instance has 54 states and 114 edges.
  • Lift Controller: The lift controller serves recurring floor requests by moving one floor up, down, or remaining stationary until requests are cleared.For n=2, the benchmark has 16 states and 34 edges; for n=3, it has 48 states and 66 edges.
  • Network Routing Arena: Network Routing Arena captures packet arrivals and authentication events alongside liveness objectives for routing decisions and memory updates.Its arena includes exploration, authentication, routing, memory updates, recovery, and idle regions.
  • Generalized Buffer: Generalized Buffer models independent single-slot producer-consumer channels, requiring every buffer to be emptied infinitely often after recurring production.For n=2, the instance has 12 states and 29 edges; for n=3, it has 16 states and 54 edges.
  • Bus Arbiter: The bus arbiter grants access to at most one requesting process at a time while guaranteeing infinitely-often service for every process.The n=2 instance has 16 vertices, 61 edges, 2 assumptions, and 2 guarantees.
Loading 2608.28391v1…