Abstract:
This paper offers characteristic formula constructions in the
real-time logic 
for several behavioural relations between (states
of) timed automata. 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 which is linear in that of the timed automaton they logically
describe. This also applies to the characteristic formula for timed
bisimulation equivalence, for which an exponential space construction was
previously offered by Laroussinie, Larsen and Weise
for several behavioural relations between (states
of) timed automata. 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 which is linear in that of the timed automaton they logically
describe. This also applies to the characteristic formula for timed
bisimulation equivalence, for which an exponential space construction was
previously offered by Laroussinie, Larsen and WeiseAvailable as PostScript, PDF, DVI.