A Local Approach for Temporal Model Checking of Java Bytecode