$\omega$-Regular Energy Problems
Logic in Computer Science
2024-07-22 v4
Abstract
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.
Keywords
Cite
@article{arxiv.2205.04392,
title = {$\omega$-Regular Energy Problems},
author = {Sven Dziadek and Uli Fahrenberg and Philipp Schlehuber-Caissier},
journal= {arXiv preprint arXiv:2205.04392},
year = {2024}
}