标题： 伽罗瓦能量博弈：解决各种定量可达性问题 显示英文标题

标题： Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems

摘要： 我们提供了一种针对能量受限攻击者和可达性目标的能量游戏的通用决策过程，超越了向量值能量和向量加法更新。 我们只需要能量形成良基有界并半格，且能量更新具有向上闭合的域，并可以通过伽罗瓦连接函数“撤销”。 我们将这些伽罗瓦能量游戏实例化为常见的能量游戏、下降能量游戏、多权重可达性游戏、带状态的向量加法系统的可覆盖性和最短路径问题，由Isabelle形式化和两个实现支持。 对于这些实例，我们的简单算法相对于游戏图大小是多项式的，相对于维度是指数级的。 显示英文摘要

摘要： We provide a generic decision procedure for energy games with energy-bounded attacker and reachability objective, moving beyond vector-valued energies and vector-addition updates. All we demand is that energies form well-founded bounded join-semilattices, and that energy updates have an upward-closed domain and can be "undone" through a Galois-connected function. We instantiate these Galois energy games to common energy games, declining energy games, multi-weighted reachability games, coverability on vector addition systems with states and shortest path problems, supported by an Isabelle-formalization and two implementations. For these instantiations, our simple algorithm is polynomial w.r.t. game graph size and exponential w.r.t. dimension.