Abstract
During the process of software development, it is very common that inconsistencies arise between the formal specification and some desired property. Belief Revision deals with the problem of accommodating new information that may be inconsistent with an existing knowledge base.
In this paper, we propose the use of belief revision techniques in order to deal with inconsistencies in formal specifications. The main problem to be solved is that the most well known results for belief revision only hold for logics which are monotonic and compact, while most discrete-time temporal logics used to express system properties – and in particular, CTL — are not compact. We suggest the use of bounded model-checking, transforming the problem from CTL into classical propositional logic and then transforming back the results to suggest revisions to the user.
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
Winter, K.: Model checking for abstract state machines. Journal of Universal Computer Science 3(5), 689–701 (1997)
Büessow, R.: Model Checking Combined Z and Statechart Specifications. PhD thesis, Technical University of Berlin, Faculty of Computer Science (November 2003), http://edocs.tu-berlin.de/diss/2003/buessow_robert.pdf
Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Kolyang, S.T., Wolff, B.: A structure preserving encoding of Z in Isabelle/HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 283–298. Springer, Heidelberg (1996)
Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)
de Sousa, T.C., Wassermann, R.: Handling inconsistencies in CTL model-checking using belief revision. In: Proceedings of the Brazilian Symposium on Formal Methods (SBMF) (2007)
Gärdenfors, P.: Knowledge in Flux: Modeling the Dynamics of Epistemic States. MIT Press, Cambridge (1988)
Hansson, S.O.: A Textbook of Belief Dynamics. Kluwer Academic Publishers, Dordrecht (1997)
Hansson, S.O., Wassermann, R.: Local change. Studia Logica 70(1), 49–76 (2002)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Alchourrón, C., Gärdenfors, P., Makinson, D.: On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic 50(2), 510–530 (1985)
Grove, A.: Two modellings for theory change. Journal of Philosophical Logic 17(2), 157–170 (1988)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2000)
Flouris, G.: On Belief Change and Ontology Evolution. PhD thesis, University of Crete (2006)
Penczek, W., Wozna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTl. Fundamenta Informaticae 51(1), 135–156 (2002)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530–535 (2001)
Goldberg, E., Novikov, Y.: Berkmin: A Fast and Robust SAT Solver. In: Design Automation and Test in Europe (DATE 2002), pp. 142–149 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Finger, M., Wassermann, R. (2008). Revising Specifications with CTL Properties Using Bounded Model Checking. In: Zaverucha, G., da Costa, A.L. (eds) Advances in Artificial Intelligence - SBIA 2008. SBIA 2008. Lecture Notes in Computer Science(), vol 5249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88190-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-88190-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88189-6
Online ISBN: 978-3-540-88190-2
eBook Packages: Computer ScienceComputer Science (R0)