 communication graphs and witness graphs, on which a bounded and nested depth-first search procedure is employed to run black-box testing over the unspecified component. Our algorithms are both sound and complete. Though we do not have an exact complexity analysis result, our preliminary studies show that, in the liveness testing algorithm for LTL, the maximal length of test-cases 