Specifying and verifying interaction protocols in a temporal action logic