Abstract
Timed Automata are established specification models for real-time systems. One of their main advantages is composability, allowing the modular specification of different aspects of a system via communicating timed automata. Composed together, these automata specify the behavior of a whole component or system. In previous work, we developed a technique to determinize a single timed automaton, by unfolding it and bounding ourselves to an observable depth k. Within this paper we expand our approach, enabling the efficient bounded determinization of networks of timed automata. We realize an on-the-fly algorithm that performs at each level of unfolding the following tasks: building the product, hiding the communication, removing silent transitions, and determinizing. In contrast to the previous work, this on-the-fly algorithm only needs to traverse the state-space exactly once. We implemented the algorithm in the model-based testing tool MoMuT::TA and demonstrate and evaluate our implementation on a case study.