This paper presents a tableau-based algorithm for constructing an automaton from a linear temporal logic (LTL) formula, designed for on-the-fly model checking. The algorithm aims to minimize the size of the automaton and can be used to check the validity of LTL assertions. The general problem is PSPACE-complete, but the algorithm performs well on typical verification problems. The paper discusses the background of LTL and model checking, introduces the concept of generalized Büchi automata, and details the algorithm's construction process. It also includes a correctness proof and experimental results comparing the algorithm with existing methods. The algorithm is shown to produce smaller automata and can be used to detect violations of properties during the construction of the automaton, making it a practical approach for model checking and validity checking.This paper presents a tableau-based algorithm for constructing an automaton from a linear temporal logic (LTL) formula, designed for on-the-fly model checking. The algorithm aims to minimize the size of the automaton and can be used to check the validity of LTL assertions. The general problem is PSPACE-complete, but the algorithm performs well on typical verification problems. The paper discusses the background of LTL and model checking, introduces the concept of generalized Büchi automata, and details the algorithm's construction process. It also includes a correctness proof and experimental results comparing the algorithm with existing methods. The algorithm is shown to produce smaller automata and can be used to detect violations of properties during the construction of the automaton, making it a practical approach for model checking and validity checking.