Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2505.14691 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908372725399552 |
|---|---|
| author | Lemke, Caroline Bisping, Benjamin |
| author_facet | Lemke, Caroline Bisping, Benjamin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_14691 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems Lemke, Caroline Bisping, Benjamin Logic in Computer Science Computational Complexity 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. |
| title | Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems |
| topic | Logic in Computer Science Computational Complexity |
| url | https://arxiv.org/abs/2505.14691 |