O tráfego em grandes cidades e rodovias tem sua operação impactada pelos congestionamentos com grande gasto de tempo, consumo de combustível e erros humanos na condução de veículos. neste trabalho, aborda-se o uso de um gerenciamento de interseção cooperativa que coordene um ambiente composto de veículos automatizados e que atenda a requisitos como eficiência e segurança. nesse sistema de tomada de decisão, a troca de informações entre veículos é usada para realizar movimentos que não necessariamente seguem os caminhos convencionados pelas leis de trânsito atuais, por meio de um modelo de exploração flexível em uma área discretizada da interseção. desta forma, estabeleceu-se uma coordenação capaz de organizar veículos que precisam cruzar o mesmo local em instantes de tempo relativamente próximos. assim, construiu-se abstrações de um espaço de estados, com ferramentas de verificação formal, usando sistemas de transição para executar as especificações de manobras dos veículos automatizados e a lista de prioridades de passagem a ser seguida. para analisar a alcançabilidade de estados, optou-se pela implementação de técnicas de tratamento de grafos, a fim de identificar os menores caminhos seguros possíveis que um conjunto de veículos leva para sair do setor de recursos compartilhados. os testes iniciais do processo de tomada de decisão passaram por reduções no modelo, a fim de as limitações em termos de processamento de dados e de memória. posteriormente, analisa-se a evolução dos modelos finais para variadas condições iniciais e explora-se visualmente os comportamentos de uso da área de interseção. ao final, a exploração exaustiva e automática dos estados atingíveis gerou de uma gama de alternativas de caminhos em diversos cenários, com a possibilidade de escalar o modelo para outras condições iniciais. estes resultados devem contribuir para a adoção de uma nova perspectiva em relação às pesquisas de coordenação de interseções.