 The line concerning ℘fin(a) ×  ℘(AtProp) is the closest to  the Kripke semantics of modal logic.   One might hope that the final coalgebra would turn out to be the canonical model of the modal logic  K, but this is not quite right.    One needs to cut down to those maximal consistent sets which are realized by some point in some finitely branching model.  