in small font next to the state  For example  rover F can only take action F deliver from its DELIVERING state The transition conditions i e the logical expressions labeling the edges in an FSA plan describe the set of actions that enable a state to state transition to occur The operator means   AND "
means OR " and " means NOT " The condition else" will be defined shortly The transition conditions of one agent can refer to the actions of one or more other agents This is because each agent is assumed to be reactive to what it has observed other agents doing If not visible agents communicate their action choice Once an agent s action repertoire and its allowable actions from each state have been defined else" can be defined  The transition condition  else" labeling an outgoing edge from a state is an abbreviation denoting the set of all remaining actions that may be taken from the state that are not already covered by other transition conditions  For example in Figure L s three transition conditions from state TRANSMITTING are  I receive L transmit I receive L pause and else " L can only take L transmit or L pause from this state However rover I could take I deliver instead of I receive Therefore in this case else" is equivalent to   I deliver    L transmit I deliver   L pause An FSA plan represents a set of allowable action sequences  In particular  a plan is the set of all action sequences that begin in an initial state and obey the transition conditions An example action sequence allowed by F s plan is   F collect    I deliver F collect I receive I receive where F takes its actions and observes I s actions at F deliver ech step in the sequence At run time these FSA plans are interpreted in the following manner At every discrete time step  every agent  F  I  L  is at one of the states in its plan  and it selects the next action to take Agents choose their actions independently They do not need to synchronize on action choice The choice of action might be based  for example  on sensory inputs from the environment Although a complete plan would include the basis for action choice as mentioned above  here we leave it unspecified in the FSA plans  Our rationale for doing this is that that the focus of this paper is on the verification of properties about correct action sequences The basis for action choice is irrelevant to these properties Once each agent has chosen an action  all agents are assumed to observe the actions of the other agents that are mentioned in its FSA transition conditions  For example  F s transition conditions mention I s actions  so F needs to observe what I did  Based on its own action and those of the other relevant agent s an agent knows the next state to which it will transition There is only one possible next state because the FSAs are assumed to be deterministic  For example  if F is in its COLLECTING state  and it chooses action F collect and it observes I taking action I deliver then it will stay in its COLLECTING
The process of being in a state choosing an action observing the actions of other state agents then moving to a next state is repeated indefinitely So far  we have been assuming multplans where each agent has its own individual lan then each agent uses the same multiagent plan to decide its plan   If we assume actions A multiagent plan is formed by taking a  product"  defined in Subsection of the plans for F  I  and L  This product models the synchronous behavior of the agents where synchronous" means that at each time step every agent takes an action observes actions of other agents  and then transitions to a next state  The product plan is formed essentially  by taking the Cartesian product of the individual automaton states and the in