Synthesizing Update Schedules with Game-Based Extension of Bounded Model Checking

1 Introduction

• Update steps must avoid components that are active, while system functionality must remain guaranteed, creating a conflict between update execution and availability.The schedule must identify times when each update step can be carried out safely.Source: §1 · p. 1
• Variable system behavior makes a single chosen update time insufficient; a robust schedule must work in worst-case conditions.The paper models the conflict as a game between the update process and the system and its environment.Source: §1 · pp. 1–2
• The paper extends bounded model checking with a game-based approach to synthesize a robust update plan for a system operating during updates.It builds on the game-theoretic update-scheduling approach of Kröger and Fränzle.Source: §1 · p. 2
• The method synthesizes global time points for update actions, reducing mode-specific scheduling to reaching update completion while avoiding updates to an active mode.The resulting plan is robust against arbitrary system behavior.Source: §1 · p. 2

2 Timed Games

• Timed games extend game graphs with real-valued clocks, and each player is represented by an individual timed automaton.The game combines the automata in parallel, with update transitions controllable and system transitions uncontrollable.Source: §2 · p. 2

2.1 Timed Automaton

• A timed automaton represents runs as alternating delays and discrete transitions subject to clock guards, resets, and location invariants.A never-reset global clock records total elapsed run time.Source: §2.1 · p. 3

2.2 Parallel Composition

• Parallel composition combines the system and update automata, with separate clock sets and stutter transitions when a player chooses no action.The composed game lets the two players' transitions be analyzed together.Source: §2.2 · p. 3

2.3 Games, Winning Conditions and Strategies

• A robust plan is a fixed sequence of update times that wins for every system behavior by reaching a target while never visiting bad locations.The update automaton is assumed linear and deterministic, so fixing its time points uniquely determines its behavior.Source: §2.3 · p. 4

2.4 Bounded Model Checking:

• Bounded model checking unrolls a transition system to a finite step bound and encodes executions and properties as a satisfiability problem.It can be extended for synthesis with decision variables and constraints, but bounded exploration is inherently incomplete for unbounded reasoning.Source: §2.4 · pp. 4–5

3 Example System: Trajectory Planner

• The example focuses on the mode-dependent behavior and mode-transition conditions of a trajectory planner used in a highway pilot.The planner generates feasible vehicle trajectories for autonomous driving under normal conditions and through construction zones.Source: §3 · p. 5
• The planner has four modes: Off, Normal, Construction Zone, and Emergency.Emergency is a safety mode for faulty, incomplete, or unavailable input data.Source: §3 · p. 5
• Mode changes depend on external requests and system conditions, including lane and object detection inputs.Faulty or unavailable detection inputs can trigger Emergency from active modes; leaving Emergency requires a request that switches to Off.Source: §3 · p. 5
• Transitions take 5–15ms, and the planner makes mode decisions every 30ms based on periodic inputs.External requests can trigger certain mode changes at any time.Source: §3 · p. 5
• The illustrative update targets Construction Zone mode, takes 10ms, and is performed in a single step.Source: §3 · p. 5

4.1 Modeling of the Player

• The game assigns the autonomous system and environment to uncontrollable player S and the update to controllable player U, with update completion required while avoiding the mode being updated.The target is the update automaton’s final location; the bad location pairs the Update phase with the mode being updated.Source: §4 · p. 6, §4.1 · p. 7

4 Bounded Model Checking for Safe Updates with Game Based Extension

• Rather than synthesize a fully reactive strategy, the method seeks a robust update plan that succeeds for every possible system behavior.The plan identifies global times at which update-automaton transitions must occur, making completion independent of system behavior.Source: §4 · p. 6

4.2 Synthesis of Robust Plan via Bounded Model Checking

• The game-based BMC extension unrolls the automata for a bounded number of steps and encodes their behavior in an SMT formula with quantifier alternation.The encoding uses Boolean location variables, real-valued clocks, and variables for the game representation.Source: §4.2 · p. 7

4.2.1 Global Time

• The global clock starts at zero and evolves strictly monotonically, providing the absolute-time reference used to synthesize update-transition times.The encoding introduces k + 1 real-valued variables for global time across the bounded run.Source: §4.2.1 · pp. 7–8

4.2.2 Encoding of System and Update Runs

• The bounded run encoding constrains update transitions to their synthesized global times and adds z-based transitions to account conservatively for system paths beyond the step bound.Without the z-based transition, a path requiring more discrete steps but less real time could reach the mode being updated before the schedule’s assumed path; the added transition directs exhausted-budget runs to a bad location.Source: §4.2.2 · pp. 9–10, §4.2.3 · p. 12

4.2.3 Game Semantics Encoding

• The quantified formula existentially selects update times and universally considers valid system and global-clock behaviors, so satisfiability yields a schedule that reaches the update’s end without visiting a bad location within k steps.This soundness guarantee applies to valid system executions within the bound that satisfy the global-time constraints; unsatisfiability for a chosen bound does not rule out a plan in the unbounded game.Source: §4.2.3 · pp. 11–12

4.2.4 Result of the Example System

• At k = 6, Z3 synthesized tg1 = 5 and tg2 = 15, guaranteeing the example update can start and finish regardless of intervening system behavior.For every k < 6, the solver reported “unsat for k steps”; each time the planner enters Off before the update starts, it can begin 5ms later.Source: §4.2.4 · pp. 12–13

4.3 Limitations and Discussion

• The example has no synthesized robust plan for updates longer than 35ms, because planner nondeterminism prevents reliably determining its mode or guaranteeing a later updatable mode.The paper suggests combining a robust plan for earlier transitions with a reactive strategy for subsequent ones; absolute-time points decouple update decisions from nondeterministic environment timing, unlike relative delays.Source: §4.3 · p. 13
• The approach reduces quantifier nesting to depth two, versus approximately 2k for a naive bounded encoding of a full reactive strategy, and is therefore intuitively expected to scale better.The authors describe this as an intuitive assessment, not a measured scalability comparison.Source: §4.3 · p. 13
• The method synthesizes fixed global-time schedules rather than state-dependent strategies, and the authors do not claim UPPAAL TIGA implements the same alternating-quantifier structure.They characterize UPPAAL TIGA as based on symbolic, zone-based game theory and note simpler integration of SMT theories as a conceptual benefit.Source: §4.3 · p. 13
• Direct runtime evaluation and optimizing the game-based BMC extension for scalability comparable to UPPAAL’s reactive-strategy synthesis remain future work.The passage poses both runtime evaluation and further scalability optimization as open topics.Source: §4.3 · p. 13

• Prior work divides broadly between methods for safe updates under specifications and techniques for synthesizing strategies using timed games or SMT-based bounded model checking.Source: §5 · p. 13
• Holthusen et al. [14] use contract-based configuration refinement, Finkbeiner and Schewe synthesize bounded discrete systems, and Göttmann et al. optimize strategies under stochastic behavior.The paper contrasts these approaches with timed global-time schedules that provide qualitative guarantees across executions.Source: §5 · p. 14
• UPPAAL TIGA supports timed-game reachability and safety strategies, while UPPAAL Stratego targets stochastic and priced-game optimization.The passage notes limits in combining complex objectives and reasoning over universally quantified adversarial behavior.Source: §5 · p. 14
• SMT-based BMC tools vary in quantifier support: ISAT3 is restricted to existential reasoning, while cvc5 and MathSAT5 support quantified formulas but can struggle with nesting.Source: §5 · p. 14
• The paper adapts SMT-based synthesis to alternating quantifiers from the game formulation, timing constraints, and robustness requirements.Source: §5 · p. 14

• Game semantics combined with bounded model checking synthesizes robust update schedules as global time points independent of system behavior.The update and system are modeled as a timed game; unlike reactive strategies, the plan is fixed rather than state-dependent.Source: §6 · p. 14
• A trajectory-planner example uses Z3 to synthesize a robust update plan, supporting the authors’ conclusion that such plans are promising for safe, predictable updates.Source: §6 · p. 14
• A detailed scalability analysis and comparison with reactive-strategy synthesis are left for future work.Source: §6 · p. 14