@article{Aceto_Ingólfsdóttir_Pedersen_Poulsen_2000, title={Characteristic Formulae for Timed Automata}, volume={7}, url={https://tidsskrift.dk/brics/article/view/20150}, DOI={10.7146/brics.v7i23.20150}, abstractNote={This paper offers characteristic formula constructions in the real-<br />time logic L for several behavioural relations between (states of)<br />timed automata. The behavioural relations studied in this work are<br />timed (bi)similarity, timed ready simulation, faster-than bisimilarity<br />and timed trace inclusion. The characteristic formulae delivered by<br />our constructions have size which is linear in that of the timed <br />automaton they logically describe. This also applies to the characteristic<br />formula for timed bisimulation equivalence, for which an exponential<br />space construction was previously offered by Laroussinie, Larsen and<br />Weise.}, number={23}, journal={BRICS Report Series}, author={Aceto, Luca and Ingólfsdóttir, Anna and Pedersen, Mikkel Lykke and Poulsen, Jan}, year={2000}, month={Jan.} }