$\omega$-Regular Energy Problems

TL;DR

This paper presents efficient algorithms for solving combined energy and acceptance conditions in weighted automata and timed automata, using modified Bellman-Ford and reduction techniques, with implementations available in open-source tools.

Contribution

It introduces a novel approach to solve energy and acceptance problems in weighted automata, including witness extraction, using modified Bellman-Ford and reduction methods.

Findings

Algorithms are efficient and implementable.

Solutions are provided for both automata and timed automata.

Tools are freely available for practical use.

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.