A proof lattice-based technique for analyzing liveness of resource controllers