Update and Abstraction in Model Checking of Knowledge and Branching Time