伽罗瓦能量博弈：解决各种定量可达性问题

我们提供了一个用于能量博弈的通用决策程序，其中包含能量受限攻击者和可达性目标，超越了向量值能量和向量加法更新。我们仅要求能量形成良好且有界的下确界半格，能量更新具有上闭域且可以通过伽罗瓦连接函数“撤销”。我们将这些伽罗瓦能量博弈实例化为常见能量博弈、能量受限博弈、多权重可达性博弈、向量加法系统带状态的可达性问题以及最短路径问题。这些实例均得到 Isabelle 形式化化和两个实现器的支持。对于这些实例，我们的简单算法相对于游戏图大小为多项式，相对于维度为指数级。