Improve Model Checking Efficiency Using Specific Knowledge about the System

In this paper, we present a timed automaton reachability analysis algorithm which can use some other properties to improve the model checking efficiency. If the model checker aborts because of memory or CPU time limitation when checking a property P, the users can still use a set of auxiliary properties P₁, P₂,..., P_n about the system to reduce the space and time requirement. People can verify these auxiliary properties by either model checking or other methods like theorem proving. This algorithm gives the users a way to reduce the space and time requirement of model checking using their knowledge about the system under check.