IJPAM: Volume 52, No. 3 (2009)
KRIPKE STRUCTURES AS ``TABLE SYSTEMS''
Institute for Research in Applied Mathematics and Systems
National Autonomous University of Mexico
Apdo. 20-726, México D.F., 01000, MEXICO
Abstract.A model checker determines whether or not a Kripke structure satisfies a given temporal-logic formula. A model updater, by contrast, modifies a Kripke structure in such a way that a given temporal-logic formula holds, if possible. An important component of a model checker (such as NuSMV or SPIN) is a language allowing the concise specification of large Kripke structures. This suggests that any practical method for model update should employ such languages as well. We study a computation-tree logic (CTL) model updater employing ``table systems,'' a fragment of the structure-specification language of NuSMV. Such a fragment allows our model-updater to produce structures having a similar specification to that of the structure given by the user. Our updater extends an existing, state-by-state method for CTL model update by adding/removing additional transitions than those prescribed by the original method.
Received: March 20, 2009
AMS Subject Classification: 68T27, 68T05, 68Q60
Key Words and Phrases: model checking, computation-tree logic (CTL), model update, knowledge revision/update
Source: International Journal of Pure and Applied Mathematics