Characteristic formulae for timed automata

This paper offers characteristic formula constructions in the real-time log ic L-nu for several behavioural relations between (states of) timed automat a. The behavioural relations studied in this work are timed (bi)similarity, timed ready simulation, faster-than bisimilarity and timed trace inclusion . The characteristic formulae delivered by our constructions have size whic h is linear in that of the timed automaton they logically describe. This al so applies to the characteristic formula for timed bisimulation equivalence , for which an exponential space construction was previously offered by Lar oussinie, Larsen and Weise.