Alternating projection temporal logic (APTL) has a concise syntax with strong expressive power. It is able to express not only properties specified in classical temporal logic LTL, but also interval related sequential and periodical properties, as well as game related properties of open systems and multi-agent systems. To verify whether a system satisfies an APTL formula, the satisfiability of the APTL formula should be checked. In this paper, based on the method for checking satisfiability of an arbitrary APTL formula provided, a supporting tool APTL2BCG has been developed. The details of implementation are given as follows. Firstly, LNFG of P is constructed according to the normal form of the formula P. Then, the LNFG is transformed to a generalized alternating Büchi automaton over concurrent game structure (GBCG). Finally, the alternating Büchi automaton is developed over concurrent game structure (BCG) from the obtained GBCG, and the BCG is simplified for checking the satisfiability of the formula P.