This paper presents a tableau-based algorithm for constructing an automaton from a linear temporal logic (LTL) formula, designed for efficient on-the-fly model checking. The algorithm constructs the automaton simultaneously with the model, allowing early detection of property violations. It translates an LTL formula into a Generalized Büchi automaton using a depth-first search approach, which can then be transformed into a classical Büchi automaton for emptiness checking. The algorithm is simple to implement and generates small automata, making it suitable for practical use in model checking. The key idea is to build the automaton incrementally during the verification process, avoiding the need to construct the entire automaton upfront. The algorithm is shown to be effective in practice, performing well on typical LTL formulas used in verification. The paper also compares the proposed algorithm with previous approaches, highlighting its advantages in terms of efficiency and on-the-fly construction. The algorithm is proven correct and is demonstrated to be effective in verifying protocols against their specifications.This paper presents a tableau-based algorithm for constructing an automaton from a linear temporal logic (LTL) formula, designed for efficient on-the-fly model checking. The algorithm constructs the automaton simultaneously with the model, allowing early detection of property violations. It translates an LTL formula into a Generalized Büchi automaton using a depth-first search approach, which can then be transformed into a classical Büchi automaton for emptiness checking. The algorithm is simple to implement and generates small automata, making it suitable for practical use in model checking. The key idea is to build the automaton incrementally during the verification process, avoiding the need to construct the entire automaton upfront. The algorithm is shown to be effective in practice, performing well on typical LTL formulas used in verification. The paper also compares the proposed algorithm with previous approaches, highlighting its advantages in terms of efficiency and on-the-fly construction. The algorithm is proven correct and is demonstrated to be effective in verifying protocols against their specifications.