A Nivat Theorem for Weighted Timed Automata and Weighted Relative Distance Logic

TL;DR

This paper establishes a Nivat theorem for weighted timed automata, showing their expressive equivalence with a weighted relative distance logic, enabling constructive translations and decidability results for quantitative real-time system modeling.

Contribution

It introduces a Nivat theorem for WTA and a weighted relative distance logic, connecting automata and logic for quantitative timed languages.

Findings

Recognizable weighted timed languages can be constructed from boolean timed languages.

Weighted relative distance logic and WTA are expressively equivalent.

Constructive translation enables decidability of the logic.

Abstract

Weighted timed automata (WTA) model quantitative aspects of real-time systems like continuous consumption of memory, power or financial resources. They accept quantitative timed languages where every timed word is mapped to a value, e.g., a real number. In this paper, we prove a Nivat theorem for WTA which states that recognizable quantitative timed languages are exactly those which can be obtained from recognizable boolean timed languages with the help of several simple operations. We also introduce a weighted extension of relative distance logic developed by Wilke, and we show that our weighted relative distance logic and WTA are equally expressive. The proof of this result can be derived from our Nivat theorem and Wilke's theorem for relative distance logic. Since the proof of our Nivat theorem is constructive, the translation process from logic to automata and vice versa is also constructive. This leads to decidability results for weighted relative distance logic.