O termo jogo tem sido utilizado como uma metáfora, em várias áreas do conhecimento, para modelar e analisar situações onde agentes(jogadores) interagem em ambientes compartilhados para a realização de seus objetivos sejam eles individuais ou coletivos. Existem diversos modelos propostos para jogos por diferentes áreas do conhecimento, tais como matemática, ciência da computação, ciência política e social, entre outras. Dentre as diversas formas de modelar jogos examinamos a Teoria dos Jogos e as lógicas para jogos. Neste trabalho apresentamos uma lógica modal de primeira-ordem baseada na lógica CTL, chamada de Game Analysis nalysis Logic, para raciocinar sobre jogos. Relacionamos os principais modelos da Teoria dos Jogos (jogo estratégico, extensivo, e de coalizão) e seus principais conceitos de soluções(equilíbrio de Nash, equilíbrio de subjogo perfeito,e core) aos modelos de GAL e às fórmulas de GAL, respectivamente. Além disso, estudamos as alternativas de quantificação De Re e De Dicto no contexto dos jogos extensivos, caracterizando o conceito de equilíbrio de Nash e equilíbrio de subjogo perfeito de acordo com as alternativas de quantificação. Relacionamos as lógicas Alternating-time lternating-Tempomporal Logic (A ATL) TL) e Coalitional Game Logic (CGL) com a lógica GAL, demonstrando que ambas as lógicas são fragmentos da lógica GAL. Outro resultado deste trabalho é caracterizar uma classe de sistemas multi- agentes,que é baseada na arquitetura de agentes Belief-Desir Desire- Intention(BDI), para a qual existem jogos extensivos e vice-v versa. Como conseqüência, os critérios de racionalidade da Teoria dos Jogos podem ser aplicados diretamente para agentes BDI e vice-versa. Assim, a abordagem deste trabalho pode ser utilizada para analisar sistemas multi-agentes. Do ponto de vista prático, apresentamos um verificador de modelos para a lógica GAL. Diversos estudos de casos são realizados utilizando o verificador de modelos.