From model checking to a temporal proof for partial models