This　paper　gives　a　symbolic　model　checking　algorithm　for　the　temporal　logic　CTL*.　The　algorithm　determines　whether　a　finite　state　system　satisfies　a　formula　in　CTL*　using　the　method　of　symbolic　tableau　construction.　According　to　our　algorithm,　we　had　implemented　a　new　CTL*　symbolic　model　checker　(MCTK)　by　means　of　OBDD　and　obtained　some　experimental　results.　Up　to　now,　the　well-known　symbolic　model　checking　tools　(SMV,　NuSMV　etc.)　have　been　implemented　only　for　the　sublogics　of　CTL*,　such　as　CTL　and　LTL.　The　results　that　we　have　obtained　in　this　paper　are　quite　surprising　and　show　that　efficient　CTL*　model　checking　is　possible　when　the　specifications　are　not　excessively　complicated.