Model checking has been successfully applied to system verification. However, there are no standard and universal tools to
date being applied for system modification. This paper introduces a formal approach called the Linear Temporal Logic (LTL)
model update for system modification. In contrast to previous error repairing methods, which were usually simple program debugging
and specialized technical methods, our LTL model update modifies the existing LTL model of an abstracted system to correct
automatically the errors occurring within this model. We introduce three single operations to represent, update, and simplify
the updating problem. The minimal change rules are then defined based on such update operations. We show how our approach
can eventually be applied in system modifications by illustrating an example of program corrections and characterizing some
frequently used properties in the LTL Kripke model.
Keywords Logic for Artificial Intelligence - belief revision and update - temporal reasoning - model update - model checking