IJPAM: Volume 52, No. 3 (2009)

A METHOD FOR CTL MODEL UPDATE, REPRESENTING
KRIPKE STRUCTURES AS ``TABLE SYSTEMS''

Miguel Carrillo$^1$, David A. Rosenblueth$^2$
$^{1,2}$Institute for Research in Applied Mathematics and Systems
National Autonomous University of Mexico
Apdo. 20-726, México D.F., 01000, MEXICO
$^1$e-mail: mcarrillob@uxmcc2.iimas.unam.mx
$^2$e-mail: drosenbl@servidor.unam.mx


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
ISSN: 1311-8080
Year: 2009
Volume: 52
Issue: 3