  Population protocols (Angluin et al., PODC, 2004) are a formal model of
sensor networks consisting of identical mobile devices. Two devices can
interact and thereby change their states. Computations are infinite sequences
of interactions satisfying a strong fairness constraint.
  A population protocol is well-specified if for every initial configuration
$C$ of devices, and every computation starting at $C$, all devices eventually
agree on a consensus value depending only on $C$. If a protocol is
well-specified, then it is said to compute the predicate that assigns to each
initial configuration its consensus value.
  In a previous paper we have shown that the problem whether a given protocol
is well-specified and the problem whether it computes a given predicate are
decidable. However, in the same paper we prove that both problems are at least
as hard as the reachability problem for Petri nets. Since all known algorithms
for Petri net reachability have non-primitive recursive complexity, in this
paper we restrict attention to immediate observation (IO) population protocols,
a class introduced and studied in (Angluin et al., PODC, 2006). We show that
both problems are solvable in exponential space for IO protocols. This is the
first syntactically defined, interesting class of protocols for which an
algorithm not requiring Petri net reachability is found.
