Another is that our verification method is expressed using the formal foundations in the model checking literature As mentioned in the introduction of this paper  FSAs have been shown to be effective The representations of reactive agent plans strategies  Burkhard Kabanza Carmel Markovitch FSA plans have been used both for multiagent competi Fogel tion of co evolving FSA agents for competitive game playing were mentioned above A similarity with our work is that Fogel assumes agents  plans are expressed as    automata  Nevertheless  Fogel never discusses verification ol of these plans  Goldman and Rosenschein present a method for multiagent coordi ntion that assumes FSA plans  Multiple agents cooperate by taking actions to favorably ater their environment  The cooperation strategy is implemented by a plan developer who manually edits the FSAs  The relationship to the work here is that they present FSA
transformations that ensure multiagent coordination  Likewise in our research  a learn ing operator that is a priori guaranteed  safe" for some multiagent coordination property transforms the FSA while ensuring coordination Although both their method and ours guarantee this coordination their solution is manual whereas ours is entirely automated Some of the more recent research on agent coordination applies formal verification meth ol of the content of the content to the content of the model their agents  semantics with a formalism similar to Petri nets  rather than FSAs   They verify synchronization  Invariance  proper ties  which prevent deadlock  using model checking  Furthermore  Lee and Durfee suggest recovery from failed verification using two methods  concept learning  and a method analo g the good of the Burkhard and Kabanza assume agent plans are represented as automata and they address issues of model check ing temporal logic properties of the joint  multiagent  plans  Thus there is a growing precedent for addressing multiagent coordination by expressing plans as   automata and verifying them with model checking  Our work builds on this precedent  and also extends it  because none of this previous research addresses efficient    verification for agents that learn Finally there are alternative methods for constraining the behavior of agents  which are complementary to reverification and self repair  For example  Shoham and Tennenholtz design agents that obey social laws e g safety conventions by restricting the agents actions Nevertheless the plan designer may not be able to anticipate and engineer all laws into the agents beforehand  especially if the agents have to adapt   One solution is to use laws that allow maximum flexibility  Fitoussi    Tennenholtz However this solution does not allow for certain changes in the plan  such as the addition or deletion of actions An appealing alternative would be to couple initial engineering of social laws with efficient reverification after learning A method for ensuring physically bounded behavior of agents is  artificial physics" With artificial physics multiagent behavior is restricted by Gordon Spears artificial forces between the agents Nevertheless when encountering severe unanticipated circumstances artificial physics needs to be complemented with reverification and steering" for self repair   Gordon et al