Modelagem e Verificação de Propriedades Epistêmicas em Sistemas Multi-agentes
Autores
4059 |
273,573
|
|
4060 |
273,573
|
Informações:
Publicações do PESC
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.
Our aim is to develop models, languages and algorithms to formally verify knowledge properties of concurrent Multi-Agents Systems. Three models are proposed and their adequacy is discussed with respect to representation and verification of knowledge properties. First, we address the issue of model checking knowledge in non-probabilistic concurrent systems. The work benefits from many recent results on model checking and combined logics for time and knowledge, and focus on the way knowledge relations can be captured from automata-based system specifications. In order to extend the results to probabilistic systems, we use Markov process models involving probability and non-determinism. The corresponding approaches to construct the knowledge relations take into account the temporal, probabilistic and non-deterministic nature of the systems, and we discuss for each case how these aspects influence the semantics for knowledge. For each model we present a language able to express specifications on the knowledge level and the corresponding model checking algorithms.