Foundations of tree-like local model updates

Model update is an approach to enhance model checking functions by providing computer aided modifications in system development [2, 9]. It has been observed that one major obstacle restricting the application of this approach, e.g. CTL model update [15], is that the update has to take the entire system model into account, and that is usually not feasible for large scale domains. In this paper, we develop a tree-like local model update approach under the framework of ACTL - a widely used fragment of CTL in property specification. We define a bisimulation based minimal change principle on tree-like local model update, reveal its relationship to traditional belief update and provide essential semantic characterizations. We also investigate primary semantic and computational properties in relation to tree-like local model update. Finally we briefly describe the update system prototype that we have implemented and summarize our experimental results.