Alter definition 6.2 as follows: Require that Fun(A) contains an additional unary relation name Active and that only agents satisfying the relation Active (active agents) can make moves. This is essentially a generalization; the original definition can be seen as a special case where all agents are active.
The new definition may be convenient, for example, when the initial state specifies all agents and their programs, and these agents are activated and deactivated during the evolution.
The same convenience can be achieved without altering the original definition. (This may be useful, for example, if you want to prove something about all distributed ealgebras and wish to restrict attention to the basic definition without losing generality.) Here is one way to do that. In order to indicate the program of a potential agent without making it an actual agent, use an auxiliary unary function name Mod'. Active(t) can be viewed as an abbreviation for Mod(t) = Mod'(t) except if Active is the subject of an update instruction.
Active(t) :=
can be viewed as an abbreviation for
if