Expressiveness Results for Timed Modal Mu-Calculi

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_{\nu ,\mu }^{rel}$, 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.

References in corpus (2)

• The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix)
• Extensible Proof Systems for Infinite-State Systems