  The paper presents a novel algorithm for computing best and worst case
execution times (BCET/WCET) of timed automata models with cyclic behaviour. The
algorithms can work on any arbitrary diagonal-free TA and can handle more cases
than previously existing algorithms for BCET/WCET computations, as it can
handle cycles in TA and decide whether they lead to an infinite WCET. We show
soundness of the proposed algorithm and study its complexity. To our knowledge,
this is the first model checking algorithm that addresses comprehensively the
BCET/WCET problem of systems with cyclic behaviour. Behrmann et al. provide an
algorithm for computing the minimum cost/time of reaching a goal state in
priced timed automata (PTA). The algorithm has been implemented in the
well-known model checking tool UPPAAL to compute the minimum time for
termination of an automaton. However, we show that in certain circumstances,
when infinite cycles exist, the algorithm implemented in UPPAAL may not
terminate, and we provide examples which UPPAAL fails to verify.
