Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

$ω$-Regular Energy Problems

Sven Dziadek, Uli Fahrenberg, Philipp Schlehuber-Caissier

TL;DR

The paper tackles the problem of deciding and witnessing energy-feasible infinite runs under ω-regular (Büchi and Parity) acceptance in both finite weighted automata and one-clock weighted timed automata. It combines a modified Bellman-Ford algorithm with Couvreur's SCC-based approach to handle energy constraints, and leverages the corner-point abstraction to reduce one-clock weighted timed automata to finite weighted automata. It provides a thorough treatment of degeneralization, lasso-based solutions, and trace extraction, and extends the framework to Parity conditions by iterative Büchi reductions. An implementation built on TChecker and Spot demonstrates practical feasibility and scalability, including a dedicated trace-extraction pipeline and a discussion of limitations and potential extensions. This work advances efficient verification of energy-constrained liveness properties in resource-bounded systems and offers a concrete, available tool for practitioners.

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ü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.

$ω$-Regular Energy Problems

TL;DR

The paper tackles the problem of deciding and witnessing energy-feasible infinite runs under ω-regular (Büchi and Parity) acceptance in both finite weighted automata and one-clock weighted timed automata. It combines a modified Bellman-Ford algorithm with Couvreur's SCC-based approach to handle energy constraints, and leverages the corner-point abstraction to reduce one-clock weighted timed automata to finite weighted automata. It provides a thorough treatment of degeneralization, lasso-based solutions, and trace extraction, and extends the framework to Parity conditions by iterative Büchi reductions. An implementation built on TChecker and Spot demonstrates practical feasibility and scalability, including a dedicated trace-extraction pipeline and a discussion of limitations and potential extensions. This work advances efficient verification of energy-constrained liveness properties in resource-bounded systems and offers a concrete, available tool for practitioners.

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ü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.
Paper Structure (8 sections, 11 theorems, 11 equations, 15 figures, 6 algorithms)

This paper contains 8 sections, 11 theorems, 11 equations, 15 figures, 6 algorithms.

Table of Contents

  1. Introduction
  2. Energy Büchi Problems in Finite Weighted Automata
  3. Energy Büchi Problems for Weighted Timed Automata
  4. Implementation
  5. Benchmarks
  6. Trace extraction
  7. Parity Condition
  8. Conclusion

Key Result

lemma 1

For any finite run $\rho$ and $c_1, c_2, b\in \mathbbm{N}$ with $c_1\le c_2$, $\textup{lastweight}_{c_1}(\rho)\le \textup{lastweight}_{c_2}(\rho)\le \textup{lastweight}_{c_1}(\rho)+c_2-c_1$.

Figures (15)

  • Figure 1: Satellite example: two representations of the base circuit. We mark the acceptance condition of the automaton above its depiction. Here both automata are in fact looping automata, as all infinite runs are accepted.
  • Figure 2: Weighted timed Büchi automaton $A_{T1}$ for satellite with work module. Only infinite runs containing infinitely many transitions marked by $\color{blue}{\bullet}$ are accepted.
  • Figure 3: Satellite example. (a) work module $W$; (b) product $B_1=A\mathbin{\|} W$
  • Figure 4: Corner-point abstraction of base module of Figure \ref{['fig:ex.1']}.
  • Figure 5: Left: WBA (also used in Example \ref{['ex:double_checking']}); right: degeneralization of one SCC (states named original state, level).
  • ...and 10 more figures

Theorems & Definitions (16)

  • definition 1: WBA
  • lemma 1
  • definition 2
  • definition 3
  • lemma 2
  • lemma 3
  • theorem 1
  • definition 4: WTBA
  • definition 5
  • lemma 4
  • ...and 6 more