A New Approach of Partial Order Reduction Technique for Parallel Timed Automata Model Checking

A new partial order reduction method for timed automaton model checking is presented in this paper. This method avoids exhaustive state-space exploration by enumerating only part of enabled transitions at some symbolic states. This paper gives some sufficient conditions on which partial enumeration does not change the reach ability analysis result. Efficient algorithms are presented to check these conditions. The optimized reach ability analysis algorithm only computes successors w.r.t. part of enabled transitions when it visits a symbolic state the first time. Later, the algorithm revisits generated states to check whether it is necessary to enumerate all transitions. Some experiments shows that the method significantly reduce the number of symbolic states generated during state space exploration.