Model-checking, an automatic verification methodology, has been applied to verify multi-agent systems. Alternating-time temporal logic (ATL), a property specification language for multi-agent systems was also investigated. According to whether agents are able to observe the whole information of the system and whether agents are able to record the history information, agents' strategies are divided into four types. These strategy abilities are defined in semantic level of ATL, as well as other logics. However, under perfect information and perfect recall setting, all agents have the same strategy ability. Under imperfect information and/or imperfect recall setting, only agents appeared in coalition modalities <<A>>φ and [[A]]φ have imperfect information and/or imperfect recall strategies, while other agents not in A still have perfect information and perfect recall strategies. When coalition modalities are nested, same agents may have different strategy abilities to fulfill different sub formulas, which results in inconsistency. On the other hand, in practice, agents' strategy abilities are usually decided by the multi-agent systems rather than the specifications, and different agents may own different strategy abilities. This kind of multi-agent systems is called heterogeneous mutli-agent systems. To overcome these problems, this paper proposes a new formal model, called typed interpreted systems which are able to define agent's strategy abilities at syntax level. Typed interpreted systems extend interpreted systems by associating each agent with a strategy type denoting the agent's strategy ability, therefore are able to model heterogeneous mutli-agent systems. The paper investigates the semantics of ATL on this new model and proposes an EXPTIME model-checking algorithm. The model-checking algorithm is implemented in a prototype tool ShTMC.