Abstract model checking and refinement of temporal logic in αSPIN | Publicación