and internal conditions  To ensure the usefulness of these learning operators the learner needs to check that it has not generated a useless plan ie Although not addressed in this paper  we are currently developing efficient methods for making this check using the knowledge of the learning that was done The particular choice of learning operators presented here was motivated by four factors First these operators translate into easy to implement perturbations of entries in a table which is the representation of FSAs used in our implementation  see Section Second these operators were inspired by the literature  For example  generalization and special ization operators are considered fundamental for inductive inference  Michalski and to deleting adding FSA edges are effective for evolving FSAs  Fogel Third these oper ators made practical sense in the context of applications that were considered  Fourth  the particular taxonomies presented here facilitate powerful theoretical and empirical results for reducing the time complexity of reverification  as shown in the remainder of this paper

## 4. A Priori Results About The Safety Of Machine Learning Operators

Subsection defined several useful learning operator schemas to modify automaton edges to and the transition conditions along edges

-
The K
K
results in this section establish which of these operator schemas are a priori guaranteed to preserve two property classes of interest  Invariance and Response   This section assumes to that all learning operators are applied to a single FSA plan ie lagent Or lplan Section addresses the translation of the operators applied to a single plan into their effect on a product plan  for      multans   and how this affects the results  We begin by formally defining what we mean by  safe machine learning operator "

## 4.1 "Safe" Online Machine Learning

Our objective is to lower the time complexity of reverification  The ideal solution is to iden tify safe machine learning methods  SMLs   which are machine learning operators that are a priori guaranteed to preserve properties  also called  correctness preserving mappings" and require no run time reverification  For a plan   and property    suppose verification has succeeded prior to learning ie   x  x implies x Then a i e machine learning operator         is an SML if and only if verification is guaranteed to succeed after learning  In other words  if   '
t hen implies Subsection provides results about the a priori safety of machine learning operators Some of the results in Subsection     are negative  Nevertheless  although we do not have an a priori guarantee for these learning operators  Section   shows that we can perform reverification more efficiently than total reverification from scratch

## 4.2 Theoretical Results

Let us begin by considering the primitive operators The results for all primitive operators are corollaries of two fundamental theorems  Theorems   and    which may not be imme diately intuitive  For example it seems reasonable to suspect that if an edge is deleted somewhere along the path from a trigger to a response  then this could cause failure of a Response property to hold because the response is no longer accessible  In fact  this is not