Optimization Technique for Shared Variables in Real-time System Model-Checking
实时系统的模型检验中针对共享变量的优化技术

Real-time systems are often modeled as timed automaton networks, which are parallel compositions of timed automata. Those timed automata interact with each other through shared variables and/or communication chan- nels. In the literate, symbolic states with different shared variable valuations in automaton networks are treated as distinct ones. Therefore, shared variables are also one of the causes of state-space explosion. We present the notion of the compatibility relationship between different shared variable valuations in this paper. Using this compatibility relationship can reduce the amount of states that need exploring in the reachability analysis algorithm of timed au- tomaton networks. In this paper, we describe two algorithms: one that detects compact shared variable valuations and the other more powerful one that detects this compatibility relationship further. These two algorithms result in an enhanced reachability analysis algorithm. The experiment results show that our technioque improves the space-effi- ciency of reachability analysis significantly.