Abstract
Model checking is one of the most robust techniques in automated system verification. But, although this technique can handle complex verifications, model checking tools usually do not give any information on how to repair inconsistent system models. In this paper, we show that approaches developed for CTL model update cannot deal with all kinds of model changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context. We relate our proposal to classical works in belief revision and give an algorithm sketch.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 8(2), 244–263 (1986)
Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L.: An analysis of SAT-based model checking techniques in an industrial environment. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 254–268. Springer, Heidelberg (2005)
Chauhan, P., Clarke, E.M., Kukula, J.H., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 33–51. Springer, Heidelberg (2002)
Cimatti, A., Clarke, E.M., 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)
Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artificial Intelligence 112(1-2), 57–104 (1999)
Zhang, Y., Ding, Y.: CTL model update for system modifications. Journal of Artificial Intelligence Research 31(1), 113–155 (2008)
Herzig, A., Rifi, O.: Propositional belief base update and minimal change. Artificial Intelligence 115(1), 107–138 (1999)
Winslett, M.: Reasoning about action using a possible models approach. In: Proc. of AAAI, pp. 89–93. Morgan Kaufmann, San Francisco (1988)
Katsuno, H., Mendelzon, A.O.: On the difference between updating a knowledge base and revising it. In: Proc. of KR, pp. 387–395. Morgan Kaufmann, San Francisco (1991)
Alchourron, C.E., Gärdenfors, P., Makinson, D.: On the logic of theory change: Partial meet contraction and revision functions. J. Symb. Logic 50(2), 510–530 (1985)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. Springer, Heidelberg (1999)
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, Cambridge (2004)
Katsuno, H., Mendelzon, A.O.: A unified view of propositional knowledge base updates. In: Proc. of IJCAI 1989, pp. 1413–1419. Morgan Kaufmann, San Francisco (1989)
Herzig, A.: Logics for belief base updating. In: Dubois, D., Prade, H. (eds.) Handbook of Defeasible Reasoning and Uncertainty Management. Vol. Belief Change, pp. 189–231. Kluwer Academic, Dordrecht (1998)
Winslett, M.: Updating logical databases. Cambridge University Press, Cambridge (1990)
Sousa, T.C.: Revisão de modelos formais de sistemas de estados finitos. Master’s thesis, Universidade de São Paulo (2007)
Sousa, T.C., Wassermann, R.: Handling inconsistencies in CTL model-checking using belief revision. In: Proc. of the Brazilian Symposium on Formal Methods (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Guerra, P.T., Wassermann, R. (2010). Revision of CTL Models. In: Kuri-Morales, A., Simari, G.R. (eds) Advances in Artificial Intelligence – IBERAMIA 2010. IBERAMIA 2010. Lecture Notes in Computer Science(), vol 6433. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16952-6_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-16952-6_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16951-9
Online ISBN: 978-3-642-16952-6
eBook Packages: Computer ScienceComputer Science (R0)