Before beginning our discussion of automata  we briefly digress to define Boolean al gebra Examples throughout this paper have automaton transition conditions expressed in Boolean algebra  because Boolean algebra succinctly summarizes these transition condi tions  Boolean algebra is also useful for succinctly expressing the properties  Furthermore it is easier for us to describe two of the incremental reverification algorithms if we use Boolean algebra notation  Therefore  we briefly summarize the basics of Boolean algebra A Boolean algebra    is a set of elements with distinguished elements   and    closed under the Boolean            and    operations  and satisfying the standard properties   Sikorski For elements  and  of is called the meet of   and is called the join of   and    and     is called the complement of    For those readers who are unfamiliar with Boolean algebras and who want some intuition for these operations  it may help to imagine that each element of is itself a set eg a set of actions Meet join and complement would then be set intersection  union  and complement  respectively   Elements and in this case  would be the empty set     and the set of all elements in the universe respectively The Boolean algebras are assumed to be finite  There is a partial order among the which is defined as if and only if It may help to think of elements analogous to    for sets  The elements   and   are defined as and The analogous to single element sets  of         are the nonzero elements of   minimal with respect to    In the rovers example  agents F  I  and L each have their own Boolean algebra with its atoms  The atoms of F s Boolean algebra are its actions F collect and F deliver  the atoms of I s algebra are I receive and I deliver  the atoms of L s algebra are L transmit  L pause  and L receive  The element  F collect    F deliver  of F s Boolean algebra describes the set of actions   F collect  F deliver A Boolean algebra of if is a nonempty subset of that is closed and and also has the distinguished elements and under the operations 1 is the product algebra of subalgebras the atoms of the subalgebras For example  if 1 respectively then  1 n is an atom of Π n =1   i The Boolean algebra       for agent F s actions is the smallest one containing the atoms of F s algebra  It contains all Boolean elements formed from F s atoms using the Boolean and    including   and     These same definitions hold for I and L s operators algebras       and in the multiagent plan ie  the product of the F  I  and L FSAs   One atom of the product algebra taken simultaneously by the three agents  Algebras product algebra Let us return now to automata Formally an FSA of the type considered here is a is the set of vertices states of three tuple where is the Boolean algebra corresponding to is the matrix of transition conditions which are elements of      and are the initial states 7 Also is the set of directed edges connecting pairs of K
vertices of which is an abbreviation for κ is the transition condition of K