We show how to efficiently solve energy B\"uchi problems in finite weighted automata and in one-clock weighted timed automata. Solving the former problem is our main contribution and is handled by a modified version of Bellman-Ford interleaved with Couvreur's algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source platforms TChecker and Spot.
翻译:我们展示了如何有效解决有限加权自动自动数据和1小时加权定时自动数据中的能量B\“uchi”问题。解决前一个问题是我们的主要贡献,它由修改版的Bellman-Ford与Couvreur的算法互连处理。后一个问题通过减少前一个依赖角点抽象处理。我们的所有算法都可以免费获得,并用基于开放源平台Tchecker和Spot的工具实施。