Finding Minimum and Maximum Termination Time of Timed Automata Models with Cyclic Behaviour

TL;DR

This paper introduces a new algorithm for accurately computing the minimum and maximum termination times of timed automata with cyclic behavior, addressing limitations of existing tools and handling infinite cycles.

Contribution

It presents the first comprehensive model checking algorithm for BCET/WCET in cyclic timed automata, capable of detecting infinite cycles and ensuring soundness.

Findings

The algorithm can handle arbitrary diagonal-free timed automata with cycles.

It can determine whether cycles lead to infinite WCET.

The proposed method outperforms UPPAAL in cases with infinite cycles.

Abstract

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.