Abstract: Compared with propositional interval temporal logic (PITL), extended propositional interval temporal logic (EPITL) is equipped with infinite models and the chop-star operator additionally. However, there is no algorithm available for model checking EPITL. To this end, we propose an algorithm for EPITL satisfiability checking. The first step is to translate EPITL formulae with or without chop-star operators into their normal forms (NFs). The second step is to construct normal form graphs (NFGs) from the NF formulae. The last step is to check the satisfiability of the EPITL formulae by using the NFGs. Accordingly, we can translate the NFGs into buchi automata. So, the EPITL model checking problem is solved. As shown in the simulation results, our approach is superior to the existing ones based on other logics in terms of specification and verification of some properties of loop structures.