一句话：提出子值映射与dGL归纳刻画，合成最宽松的混合博弈控制包络。
嵌入式系统（如汽车、火车）的控制问题可建模为双人混合博弈，控制包络是一族保证玩家不败的非确定性策略。本文研究如何合成尽可能宽松的控制包络。作者提出 subvalue maps，一种可沿博弈结构进行验证与合成的组合式策略表示；并在微分博弈逻辑 dGL 中给出归纳逻辑刻画，用于判定子值映射是否诱导可靠控制包络，保证无论对手如何行动玩家都不失败。论文证明存在允许最多动作选项且仍获胜的最大子值映射，并满足该逻辑刻画，由此得到归纳式合成框架。评估利用 dGL 的表达力对多种控制挑战建模并求解。
Control problems for embedded systems like cars and trains can be modeled by two-player hybrid games. Control envelopes, which are families of safe control solutions, correspond to nondeterministic policies that ensure a player following them will not lose. Each deterministic, finite specialization of the nondeterministic policy is a control solution. This paper synthesizes control envelopes for hybrid games that are as permissive as possible. It introduces subvalue maps , a compositional representation of such policies that enables verification and synthesis along the structure of the game. An inductive logical characterization in differential game logic (dGL) checks whether a subvalue map induces a sound control envelope which ensures that the player never loses, no matter what actions the opponent plays. The maximal subvalue map, which allows the most action options while still winning, is shown to exist and satisfy a logical characterization. An inductive subvalue map synthesis framework is obtained from the soundness characterization. An evaluation of the framework uses the significant expressivity of dGL to model and solve a broad range of control challenges.
@article{paperbot3804,
title = {Hybrid Game Control Envelope Synthesis},
author = {Aditi Kabra and Jonathan Laurent and Stefan Mitsch and André Platzer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798230}
}