AP->P(s) atomic propositions to the set of states where these are true.
Block contains set of equations e, variables Xi

monotonic function defined on a lattice (set of ordered states)-> lpf, gfp
Block graph is acyclic digraph mapping dependencies among blocks B1,...,Bm via edges

now the model checking is LTS L=,s0) and CS=logic B w/ var X to see s0 belongs [[X]][[B]]
CS Cleaveland-Steffen model checking algorithm:
uses a "product graph" not computed explicitly:
L=,s)> and mu-calc formula B is digrpah of V= ,
E= {if Xi=xj V xk or xi=xj^xk then -> and ->
if s->s' and xi = xj or xi=[a]xj, then -> }
or-node: used op V or to define xi
and-node: other
maintain bool vars for xi , keep track of immediate successors, predecessors counted

finds min, max (non-incremental) for lfp, gfp. No change to blocks after

MCI
modify CS to be incremental
given a previous computed value of variable,
when changes occur (delete/insert transition), compute new valuation using all as "starting point"
init phase: effects of change found, then iterate topological order of block graph using MAX/MIN modified
now the lattice ordered maybe changed up or down in a block Bj, so we have upj and downj (two lists) and counter
during init phase change product graph and var assignments
simply remove/add edges to product graph then update counters and-node, or-nodes
edge updates according to and/or-node and added to lists up or down
However, a fp at this point isn't necessarily desired one.
Look at SCCs as well