An Efficient Inverse Image Computation Algorithm for Sequential Machine Verification Using Temporal Logics