Formal verification of human-robot teamwork

ABSTRACT

We here address the modelling and analysis of human-agent teamwork, specifically in the context of proposed astronaut-robot collaboration in future space missions. We are particularly interested in modelling such systems at a level that allows formal verification techniques to be applied, and hence carry out sophisticated analysis of the reliability and effectiveness of the teams before the system is deployed in real scenarios. In this paper we describe our ongoing research in this area.

REFERENCES

• 1: R. H. Bordini, L. A. Dennis, B. Farwer, and M. Fisher. Automated Verification of Multi-Agent Programs. In Proc. 23rd IEEE/ACM Int. Conf. Automated Software Engineering (ASE), 2008.
• 2: Rafael H. Bordini , Michael Fisher , Willem Visser , Michael Wooldridge, Model Checking Rational Agents, IEEE Intelligent Systems, v.19 n.5, p.46-52, September 2004 [doi>10.1109/MIS.2004.47]
• 3: Rafael H. Bordini , Michael Fisher , Willem Visser , Michael Wooldridge, Verifying Multi-agent Programs by Model Checking, Autonomous Agents and Multi-Agent Systems, v.12 n.2, p.239-256, March 2006 [doi>10.1007/s10458-006-5955-7]
• 4: Rafael H. Bordini , Michael Wooldridge , Jomi Fred Hübner, Programming Multi-Agent Systems in AgentSpeak using Jason (Wiley Series in Agent Technology), John Wiley & Sons, 2007
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: Anand S. Rao, AgentSpeak(L): BDI agents speak out in a logical computable language, Proceedings of the 7th European workshop on Modelling autonomous agents in a multi-agent world : agents breaking away: agents breaking away, p.42-55, February 1996, Einhoven, The Netherlands
• 7: M. Sierhuis. Modeling and Simulating Work Practice. BRAHMS: a multiagent modeling and simulation language for work system analysis and design. PhD thesis, Social Science and Informatics (SWI), University of Amsterdam, The Netherlands, 2001.
• 8: M. Sierhuis. Multiagent Modeling and Simulation in Human-Robot Mission Operations, 2006. See http://ic.arc.nasa.gov/ic/publications.
• 9: M. Sierhuis, J. M. Bradshaw, A. Acquisti, R. V. Hoof, R. Jeffers, and A. Uszok. Human-Agent Teamwork and Adjustable Autonomy in Practice. In Proc. 7th Int. Symp. Artificial Intelligence, Robotics and Automation in Space (i-SAIRAS), 2003.
• 10: Michael Woolridge , Michael J. Wooldridge, Introduction to Multiagent Systems, John Wiley & Sons, Inc., New York, NY, 2001
• 11: M. Wooldridge and A. Rao, editors. Foundations of Rational Agency. Kluwer, 1999.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Verification

Keywords:
agent-based modelling, teamwork, verification