human or allow a human to come to harm  The main contribution of Weld and Etzioni is call to arms   before we release autonomous agents into real world environments  we a need some credible and computationally tractable means of making them obey Asimov s First Law  how do we stop our artifacts from causing us harm in the process of obeying our orders "  Of course  this law is too general for direct implementation and needs to be operationalized into specific properties testable on a system  such as   Never delete a user s file " This paper addresses Weld and Etzioni s call to arms in the context of adaptive agents To respond to the call to arms we are working toward Asimovian" adaptive agents which we define to be adaptive agents that can verify  in a reasonably efficient manner  whether user defined properties are preserved after adaptation 2  Such agents will either constrain their adaptation methods  or repair themselves in su a way as to preserve these properties The verification method assumed here model checking consists of building a finite model of a system and checking whether the desired property holds in that model  In the context of this paper  model checking determines whether for plan    and property ie whether plan models" satisfies  property     The output is either  yes" or  no" and if  no " one or more counterexamples are provided  Model checking has proven to be very effective for safety critical applications eg a model checker uncovered a potentially disastrous error in a system designed to make buildings more earthquake resistant  This error would have unleashed a structural force to worsen earthquake vibrations  rather than dampen them  Elseaidy et al Essentially model checking is brute force search through the set of all reachable states of the plan to check if the property holds If the plan has a finite number of states this process terminates   Model checking global properties of a multiagent plan has time complexity that is exponential in the number of agents 3 With a large number of agents this is could be a serious problem In fact even model checking a single agent plan with a huge number of states can be computationally prohibitive  A great deal of research in the verification community is currently focused on reduction techniques for handling very large state spaces Clarke Wing One of the largest systems model checked to date using these reduction techniques had 120 states  Burch et al Nevertheless the applicability of many of these reduction techniques is restricted and few are completely automated Furthermore  none of them are tailored for efficient    verification after learning has altered the system Some methods in the literature are designed for software that changes One that emphasizes efficiency as ours does is Sokolsky and Smolka s However none of them  including Sokolsky and Smolka s method  are applicable to multiagent systems in which a single agent could adapt  thereby altering the global behavior of the overall system In contrast  our approach addresses the timeliness of adaptive multiagent systems Consider how reverification fits into our overall adaptive agents framework In this framework  see Figure     there are one or more agents with  anytime" plans  Grefenstette ie  plans that are continually executed in response to internal and Ramsey external environmental conditions  Each agent s plan is assumed to be in the form of a finite state automaton  FSA  FSAs have been shown to be effective representations of