1. A method for bounded model checking of arbitrary Linear Time Logic temporal properties comprising: translating properties associated with temporal operators F(p), G(p), U(p, q) and X(p) into property checking schemas comprising Boolean satisfiability checks, wherein F represents an eventuality operator, G represents a globally operator, U represents an until operator and X represents a next-time operator; and checking an overall property in a customized manner by repeated invocations of the property checking schemas for F(p), G(p), U(p, q), X(p) operators and standard handling of atomic propositions and Boolean operators.