We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a B\"uchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm 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.

翻译：本文展示了如何在有限加权自动机与单时钟加权时间自动机中，高效求解涉及定量度量（本文称为能量）以及由Büchi或奇偶目标表达的定性接受条件的问题。求解前一类问题并提取相应证据是我们的主要贡献，该问题通过贝尔曼-福特算法的改进版本与库夫勒算法交错处理实现。后一类问题则通过基于角点抽象归约至前一类问题进行处理。我们所有算法均已开源实现，并集成于基于TChecker与Spot开源平台的工具中。