Modelagem e Verificação de Propriedades Epistêmicas em Sistemas Multi-agentes

O objetivo deste trabalho é desenvolver modelos, estratégias e algoritmos para verificar formalmente propriedades epistêmicas em sistemas Multi-Agentes. Três tipos de modelos são abordados e sua adequação e aplicabilidade discutidas. Primeiro, discutimos verificação de propriedades epistêmicas em modelos não probabilísticos para sistemas multi-agentes. O trabalho se beneficia dos vários resultados recentes na área de verificação de modelos e de lógicas modais combinando operadores de conhecimento e tempo, e resulta numa proposta para construir as relações de conhecimento diretamente a partir de especificações de sistemas baseadas em autômatos. Estendendo a discussão para sistemas probabilísticos baseados em modelos de processos de Markov, consideramos modelos envolvendo probabilidade e não determinismo. As respectivas propostas para construção das relações de conhecimento levam em conta a natureza temporal, probabilística e não determinística dos sistemas, considerando a influência destes aspectos na semântica para conhecimento. Apresentamos para cada modelo uma linguagem para construir especificações envolvendo conhecimento e os correspondentes algoritmos para verificação automática de propriedades.