LTL on finite and process traces: Complexity results and a practical reasoner