An Experiment of Verification of Multi-agent Robotic Soccer Plans with Model Checking
Resumo
In this paper we present an experiment of model checking which consists of the verification of plans of a multi-agent system for simulated robot soccer. This system is of considerable complexity because it is concurrent, nondeterministic and with partial vision of the environment. Some solutions adopted relative to modeling and process of verification to circumvent state space explosion are reported.
Palavras-chave:
Model Checking, Planning, Multi-agent Systems, Autonomous Agents
Referências
A. El Fallah Seghrouchni et al, “Modelling, Control and Validation of Multi-Agent Plans in Dynamic Context”, AAMAS, vol. 1, pp.44-51, Third International Joint Conference on Autonomous Agents and Multiagent Systems - Volume 1 (AAMAS'04), 2004.
F. Marc, “Planification Multi-Agent sous Contraintes dans un Contexte Dynamique: Application Aux Simulations Aériennes”, Thèse (Doctorat en Informati ue), École Doctorale d’Informati ue, Télécommunication et Électronique de Paris, Université Pierre et Marie Curie, 2005.
T. A. Hezinger, “The Theory of Hybrid Automata”, 28p, Electronics Research Laboratory, College of Engineering, University of California: Berkeley, 1996.
L. Khatib et al, “Verification of plan models using UPPAAL”, 1st International Workshop on Formal Approaches to Agent-Based Systems, Maryland, 2000.
L. Khatib et al, “Mapping temporal planning constraints into timed automata”, in: Proceeding of 8th International Syposium on Temporal Representation and Reasoning, 249p, IEEE Computer Society : Cividale Del Friuli, 2001.
G. S. Costa, “Utilização da Verificação de Modelos para o Planejamento de Missões de Veículos Aéreos não-Tripulados”, Dissertação (Mestrado em Engenharia Elétrica) - IME, Rio de Janeiro, 2008.
C. B. Earle et al, “Verifying Robocup Teams”, in: Proceeding of MoChArt 2008, 5th International Workshop on Model Checking and Artificial Intelligence, 189p, Patras, 2008.
O. Santana Jr, C.F.G. Chavez, A. Loureiro da Costa, “MecaTeam Framework: An Infrastructure for the Development of Soccer Agents for Simulated Robots”, IEEE Latin American Robotic Symposium, LARS, p 137-142, ISBN: 978-1-4244-3379-7, 2008.
H. Kitano, "Robocup: The robot world cup initiative”, in Proc. of The First International Conference on Autonomous Agent (Agents-97)) Marina del Ray, The ACM Press, 1997.
G. Behrmann et al, “A Tutorial on Uppaal 4.0”, Department of Computer Science, Aalborg University, 2006.
A. Loureiro da Costa, G. Bittencourt, “From a concurrent architecture to a concurrent autonomous agents architecture”, in: Third International Workshop in RoboCup, Springer Lecture Notes in Artificial Inteligence LNAI, 1856pp, pp.85-90, 1999.
E. M. Clarke, O. Grumberg and D. A. Peled, “Model Checking”. The MIT Press, 1999.
F. Marc, “Planification Multi-Agent sous Contraintes dans un Contexte Dynamique: Application Aux Simulations Aériennes”, Thèse (Doctorat en Informati ue), École Doctorale d’Informati ue, Télécommunication et Électronique de Paris, Université Pierre et Marie Curie, 2005.
T. A. Hezinger, “The Theory of Hybrid Automata”, 28p, Electronics Research Laboratory, College of Engineering, University of California: Berkeley, 1996.
L. Khatib et al, “Verification of plan models using UPPAAL”, 1st International Workshop on Formal Approaches to Agent-Based Systems, Maryland, 2000.
L. Khatib et al, “Mapping temporal planning constraints into timed automata”, in: Proceeding of 8th International Syposium on Temporal Representation and Reasoning, 249p, IEEE Computer Society : Cividale Del Friuli, 2001.
G. S. Costa, “Utilização da Verificação de Modelos para o Planejamento de Missões de Veículos Aéreos não-Tripulados”, Dissertação (Mestrado em Engenharia Elétrica) - IME, Rio de Janeiro, 2008.
C. B. Earle et al, “Verifying Robocup Teams”, in: Proceeding of MoChArt 2008, 5th International Workshop on Model Checking and Artificial Intelligence, 189p, Patras, 2008.
O. Santana Jr, C.F.G. Chavez, A. Loureiro da Costa, “MecaTeam Framework: An Infrastructure for the Development of Soccer Agents for Simulated Robots”, IEEE Latin American Robotic Symposium, LARS, p 137-142, ISBN: 978-1-4244-3379-7, 2008.
H. Kitano, "Robocup: The robot world cup initiative”, in Proc. of The First International Conference on Autonomous Agent (Agents-97)) Marina del Ray, The ACM Press, 1997.
G. Behrmann et al, “A Tutorial on Uppaal 4.0”, Department of Computer Science, Aalborg University, 2006.
A. Loureiro da Costa, G. Bittencourt, “From a concurrent architecture to a concurrent autonomous agents architecture”, in: Third International Workshop in RoboCup, Springer Lecture Notes in Artificial Inteligence LNAI, 1856pp, pp.85-90, 1999.
E. M. Clarke, O. Grumberg and D. A. Peled, “Model Checking”. The MIT Press, 1999.
Publicado
26/05/2013
Como Citar
S., Rui C. Botelho A.; ANDRADE, Aline M. S.; COSTA, Augusto Loureiro da; BARBOZA, Frederico J. R..
An Experiment of Verification of Multi-agent Robotic Soccer Plans with Model Checking. In: WORKSHOP-ESCOLA DE SISTEMAS DE AGENTES, SEUS AMBIENTES E APLICAÇÕES (WESAAC), 7. , 2013, São Paulo/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2013
.
p. 97-102.
ISSN 2326-5434.
