2013 | OriginalPaper | Buchkapitel
Toward the Revision of CTL Models through Kripke Modal Transition Systems
verfasst von : Paulo T. Guerra, Aline Andrade, Renata Wassermann
Erschienen in: Formal Methods: Foundations and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.