Compatibility Between Shared Variable Valuations in Timed Automaton Network Model-Checking

Many real-time systems are modelled as timed automaton networks, which are parallel compositions of timed automata. Those timed automata interact with each other through shared variables and/or communication channels. In the literate, symbolic states with different shared variable valuations are treated as distinct ones. This paper presents a compatibility relation between shared variable valuations. Using this relation, the reachability analysis algorithm can avoid exploring all the states with different shared variable valuations. An algorithm is presented in this paper to detect compatible shared variable valuations. A compact data structure is also proposed to record the shared variable valuation sets found by this algorithm. Based on these results, an optimized reachability analysis algorithm is presented. Case studies show that our technique improves the space-efficiency of reachability analysis significantly.