An Expressive Timed Modal Mu-Calculus for Timed Automata

This paper presents a modal mu-calculus, \(L^{\textit{rel}}_{\mu ,\nu }\) , for encoding properties of systems modeled as timed automata. Our logic includes arbitrary fixpoints and an until-like modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mu-calculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional region-graph construction for timed automata. We additionally establish that, in contrast to the other mu-calculi, \(L^{\textit{rel}}_{\mu ,\nu }\) is strictly more expressive than Timed Computation Tree Logic (TCTL) in the setting of general timed automata, meaning that model checkers for \(L^{\textit{rel}}_{\mu ,\nu }\) are immediately usable as model checkers for TCTL for general timed automata.