Bounded Model Search in Linear Temporal Logic and Its Application to Planning