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.

翻译：本文建立了在时间自动机上解释的几种模态μ演算的相对表达能力结果。这些μ演算将表达真实时间流逝的模态与通过递归定义公式的通用框架相结合；文献中已提出了多种变体。我们证明了一种称为$L^{rel}_{\nu,\mu}$的逻辑严格强于其他所考虑的μ演算。它也比时序逻辑TCTL更具表达能力，而其他μ演算在一般时间自动机环境下与TCTL不可比较。