We present construction of characteristic formulas for event-recording automata in terms of the ERLv logic, a real-time extension of the Hennessy-Milner Logic with greatest fixpoints. By combining the construction of characteristic formulas with the model checking algorithm for ERLv, we obtain a decision procedure for timed bisimilarity and timed similarity for event-recording automata. Furthermore, we present decidability results for the fixpoint free fragment of ERLv, denoted by ERL. We show that the model checking problem for event-recording automata and ERL is PSPACE-complete, and that the satisfiability problem for ERL is decidable. 'We present a tableau-based decision procedure that allows the decision of whether or not a given ERL formula is valid. We introduce a set of reduction rules for constructing tableaux for ERL formulas, and show that these rules form a sound and complete tableau system.

• csl-01-06.ps