Certified Temporal Equilibrium Synthesis With Reusable Deviation Evidence

Temporal equilibrium synthesis seeks joint policies that satisfy a system requirement over infinite executions and admit no profitable unilateral deviation. During policy search, repeated certification can rediscover the same profitable behaviors after controller updates. We propose Certified Temporal Equilibrium Synthesis (CTES) for known finite deterministic games with Boolean linear temporal logic goals. CTES combines certification of constructed candidates with preference-guided finite-memory policy search and retains the best certified policy found. Its cross-profile deviation bank stores profitable infinite behaviors as finite prefixes and repeating loops. Replay checks whether the current opponents reproduce a stored behavior, including their memory updates through loop closure, and whether it strictly improves the deviator's current Boolean payoff. A successful replay lets the same witness reject another profile; otherwise, a complete verifier searches for new deviations. We prove sound rejection and sufficient transfer conditions against arbitrary legal pure history-dependent deviations. On contention games with up to twelve players, CTES improves the lexicographic policy score over certified initialization in 22 of 120 runs. Across matched resource-allocation streams, deviation reuse reduces total exact certification time by 15.95% with complete coverage. Under fixed search budgets, reuse improves certification throughput in contention and resource allocation.