Operator precedence temporal logic and model checking