Toward the revision of CTL models through Kripke modal transition systems

Abstract

In this paper we consider the problem of automatic repair of models in the context of system partial specification. This problem is a challenge involving theoretical and practical issues and the theory of belief revision is an alternative to give theoretical support to its solution. A Kripke structure is widely used to model systems, but it does not express partial information explicitly and a set of these structures might be required to represent several possibilities of behavior. A more general structure is the Kripke Modal Transition System (KMTS) which can specify systems with partial information and can be interpreted as a set of Kripke models. In this paper, we propose a framework for the repair of KMTS based on belief revision combined with model checking as an approach to revise sets of Kripke structures. We demonstrate the advantages of our approach, even with the existing restrictions in representing general sets of CTL models over the KMTS formalism. © 2013 Springer-Verlag.