Model Updating CTL Systems

  • Yulin Ding
  • Yan Zhang
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3809)


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.


Model Check Microwave Oven Minimal Change Atomic Proposition Kripke Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baral, C., Zhang, Y.: Knowledge updates: semantics and complexity issues. Artificial Intelligence 164, 209–243 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artificial Intelligence 112, 57–104 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Clarke Jr., E., et al.: Model Checking. The MIT press, Cambridge (1999)Google Scholar
  4. 4.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. 5.
    Ding, Y., Zhang, Y.: A logic approach for LTL system modification. In: Hacid, M.-S., Murray, N.V., Raś, Z.W., Tsumoto, S. (eds.) ISMIS 2005. LNCS (LNAI), vol. 3488, pp. 435–444. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 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. 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. 8.
    Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)Google Scholar
  9. 9.
    Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. University Press, Canbridge (2000)zbMATHGoogle Scholar
  10. 10.
    McMillan, K., Amla, N.: Automatic abstraction without counterexamples. Cadence Berkeley Labs, Cadence Design Systems (2002)Google Scholar
  11. 11.
    Winslett, M.: Updating Logical Databases. Cambridge University Press, Cambridge (1990)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Yulin Ding
    • 1
  • Yan Zhang
    • 1
  1. 1.School of Computing & Information TechnologyUniversity of Western SydneyKingswoodAustralia

Personalised recommendations