Algorithms for CTL system modification

Model updating, as a new concept to be employed as a standard and universal method for system modification, has been started in and further developed in this paper. This paper introduces algorithms for Computation Tree Logic (CTL) model update. The algorithms correct errors in a CTL Kripke model to make this model satisfy its various required properties. These update algorithms are designed through pseudo-code, which details the logic of the algorithms. The microwave oven example in has been correctly treated by the pseudo-code, which demonstrates the feasibility of these algorithms. The algorithms and their pseudo-code are the foundations for later implementation of a CTL model updater and integration of a CTL model checker and this updater