Temporal Logic and Model Checking for Operator Precedence Languages