Expressiveness Results for Timed Modal Mu-Calculi
Logic in Computer Science
2025-08-08 v1
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 , 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.
Keywords
Cite
@article{arxiv.2310.04100,
title = {Expressiveness Results for Timed Modal Mu-Calculi},
author = {Rance Cleaveland and Jeroen J. A. Keiren and Peter Fontana},
journal= {arXiv preprint arXiv:2310.04100},
year = {2025}
}