Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semantics naturally capture the synchronous interactions characteristic of many cyber-physical systems (CPS), their adoption in CPS design remains limited. Building on the concept of permissive strategy templates (PeSTels) for turn-based games, we introduce concurrent (permissive) strategy templates (ConSTels) -- a novel representation for sets of randomized winning strategies in concurrent games with Safety, Büchi, and Co-Büchi objectives. ConSTels compactly encode infinite families of strategies, thereby supporting both offline and online adaptation. Offline, we exploit compositionality to enable incremental synthesis: combining ConSTels for simpler objectives into non-conflicting templates for more complex combined objectives. Online, we demonstrate how ConSTels facilitate runtime adaptation, adjusting action probabilities in response to observed opponent behavior to optimize performance while preserving correctness. We implemented ConSTel synthesis and adaptation in a prototype tool and experimentally show its potential.
翻译:有限图上的双人博弈为建模反应式系统与其环境之间的策略交互提供了严格的理论基础。虽然并发博弈语义自然地捕捉了许多信息物理系统(CPS)所特有的同步交互特征,但其在CPS设计中的应用仍较为有限。基于回合制博弈中许可策略模板(PeSTels)的概念,我们引入了并发(许可)策略模板(ConSTels)——一种用于表示具有安全性、Büchi和Co-Büchi目标的并发博弈中随机化获胜策略集合的新型表达方式。ConSTels能够紧凑地编码无限策略族,从而支持离线和在线自适应。在离线场景中,我们利用可组合性实现增量式综合:将针对简单目标的ConSTels组合成适用于更复杂组合目标的非冲突模板。在在线场景中,我们展示了ConSTels如何促进运行时自适应,通过根据观测到的对手行为调整动作概率来优化性能,同时保证正确性。我们在原型工具中实现了ConSTel综合与自适应功能,并通过实验验证了其潜力。