A study of the model explosion problem in CTL model update

Computation Tree Logic (CTL) model update is an approach for software verification and modification, where minimal change is employed to generate admissible models that represent the corrected software design. In this paper, we first apply CTL model update to a model based on the well known Andrew File System protocol, and demonstrate the process of discovering an admissible model explosion problem. We then propose a new update principle named minimal change with maximal reachable states to solve this problem. Our experimental results show that in the case of updating the Andrew File System protocol model, the new CTL update approach significantly narrows down the admissible models to fewer committed models. We provide a thorough study on the semantics and complexity properties on optimizing CTL model update.