Expressiveness Results for Timed Modal Mu-Calculi

TL;DR

This paper compares the expressiveness of various timed modal mu-calculi over timed automata, showing that one logic is strictly more expressive than others and TCTL, highlighting differences in their expressive power.

Contribution

It establishes relative expressiveness results for several timed modal mu-calculi and introduces a logic, $L^{rel}_{ u,}$, that surpasses others and TCTL in expressiveness.

Findings

$L^{rel}_{ u,}$ is strictly more expressive than other mu-calculi.

$L^{rel}_{ u,}$ is more expressive than TCTL.

Other mu-calculi are incomparable with TCTL.

Abstract

This paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (real) time with a general framework for defining formulas recursively; several variants have been proposed in the literature. We show that one logic, which we call $L^{rel}_{\nu,\mu}$, is strictly more expressive than the other mu-calculi considered. It is also more expressive than the temporal logic TCTL, while the other mu-calculi are incomparable with TCTL in the setting of general timed automata.