It is assumed here that machine learning operators are applied one at a time per agent rrather than in batch and  if multans the agents co evolve plans by taking turns learning Beyond these assumptions this paper does not focus on the learning opera Potter tors per se  other than to define them    It focuses instead on the outcome resulting from the application of a learning operator In particular we address the reverification issue The next section gives useful background definitions needed for understanding reverification

## 3. Preliminary Definitions

This section provides definitions of FSAs  properties  verification  and  machine learning operators  For a clear  unambiguous understanding of the results in this paper  many of these definitions are formal

## 3.1  Automata For Agents' Plans

FSAs have at least four advantages over classical plans  Nilsson Wellman Dean For one  unlike classical plans  the type of finite state automaton plans used here allows potentially infinite  indeterminate  length action sequences 6  This provides a good model of embedded agents that are continually responsive to their environment without any artificial termination to their behavior  Execution and learning may be interleaved in a natural manner  Another advantage is that FSA plans have states  and the plan designer can use these states to represent subtasks of the overall task This subdivides the plan into smaller units  thereby potentially increasing the comprehensibility of the plans  States also enable different action choices at different times  even if the sensory inputs are the same A third advantage of FSA plans is that they are particularly well suited to modeling the concurrent behavior of multiple agents An arbitrary number of single agent plans can be developed independently and then composed into a synchronous multiagent plan  for which global properties may be tested  in a straightforward manner  Finally FSA plans can be verified using the very popular and effective automata-theoretic model checking methods eg see Kurshan A disadvantage of FSA plans as opposed to classical plans is that there is a great deal of research that has been done on automatically forming classical plans e g   see Dean and Wellman It is unclear how much of this might be applicable to FSAs   On the other hand  evolutionary algorithms can be used to evolve FSA plans  Fogel disadvantage of FSA plans as opposed to plans composed of rule sets is that the latter may express a plan more succinctly  Nevertheless for plans that require formal verification  FSAs are preferable because the complex interactions that can occur between rules make them very hard to verify  Formal verification for FSAs is quite sophisticated and widely used in safety critical industrial applications This subsection  which is based on Kurshan briefly summarizes the basics of the FSAs used to model agent plans  Figures   and   illustrate the definitions  This paper focuses on FSAs that model agents with a potentially infinite lifetime  represented as an infinite length string" ie a sequence of actions