Partial Order Reduction for Model Checking of Timed Automata

Abstract. The paper presents a partial order reduction method applicable to networks of timed automata. The advantage of the method is that it reduces both the number of explored control states and the number of generated time zones. The approach is based on a local-time semantics for networks of timed automata defined by Bengtsson et al. [1998], and used originally for local reachability analysis. In this semantics, each component automaton executes asynchronously, in its own local time scale, which is tracked by an auxiliary reference clock. On communication transitions, the automata synchronize their time scales. We show how this model can be used to perform model checking for an extension of linear temporal logic, which can express timing relations between events. We also show how for a class of timed automata, the local-time model can be implemented using difference bound matrices without any space penalty, despite the need to represent local time. Furthermore, we analyze the de...

• Type: Conference
• Year: 1999
• Where: CONCUR
• Authors: Marius Minea
• Keywords: CONCUR 1999, Distributed And Parallel Computing, Local Time, Time Scales, Timed Automata