Model Updating CTL Systems
Minimal change is a fundamental principle for modelling system dynamics. In this paper, we study the issue of minimal change for Computational Tree Logic (CTL) model update. We first consider five primitive updates which capture the basic update operations in the CTL model. Based on these primitive updates, we then define the minimal change criteria for CTL model update and develop formal algorithms that embed the underlying minimal change principle. We also present the well known microwave oven scenario to demonstrate our update algorithms. Our work presented in this paper can be viewed as the first formalization towards an integration of model checking and model updating for system modification.
KeywordsModel Check Microwave Oven Minimal Change Atomic Proposition Kripke Model
Unable to display preview. Download preview PDF.
- 3.Clarke Jr., E., et al.: Model Checking. The MIT press, Cambridge (1999)Google Scholar
- 6.Gammie, P., van der Meyden, R.: MCK-Model checking the logic of knowledge. In: The Proceeding of the 16th International Conference on Computer Aided Verification, pp. 479–483 (2004)Google Scholar
- 7.Harris, H., Ryan, M.: Theoretical foundations of updating systems. In: The Prodeeding of the 18th IEEE International Conference on Automated Software Engineering, pp. 291–298 (2003)Google Scholar
- 8.Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)Google Scholar
- 10.McMillan, K., Amla, N.: Automatic abstraction without counterexamples. Cadence Berkeley Labs, Cadence Design Systems (2002)Google Scholar