论文标题
$ω$ - 常规能源问题
$ω$-Regular Energy Problems
论文作者
论文摘要
我们展示了如何有效地解决涉及定量措施的问题，此处称为能量以及定性的接受条件，以有限的加权自动机和单盘加权定时自动机表示为büchi或奇偶校目标。解决了以前的问题并提取相应的证人是我们的主要贡献，并通过与Couvreur的算法交织的Bellman-Ford算法的修改版本来处理。后一个问题是通过依靠转角抽象的减少到前者来处理的。我们所有的算法都是免费提供的，并在基于开源平台Tchecker和〜Spot的工具中实现。
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üchi 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.
