To combat the well-known state-space explosion problem in Propositional Linear Temporal Logic (PLTL) model checking,a novel algorithm capable of translating PLTL formulas into Nondeterministic Automata (NA) in an efficient way is proposed.The algorithm firstly transforms PLTL formulas into their non-free forms,then it further translates the non-free formulas into their Normal Forms (NFs),next constructs Normal Form Graphs (NFGs) for NF formulas,and it finally transforms NFGs into the NA which accepts both finmite words and infinite words.The experimental data show that the new algorithm reduces the average number of nodes of target NA for a benchmark formula set and selected formulas in the literature,respectively.These results indicate that the PLTL model checking technique employing the new algorithm generates a smaller state space in verification of concurrent systems.