A Formal Semantics for Brahms

  • Richard Stocker
  • Maarten Sierhuis
  • Louise Dennis
  • Clare Dixon
  • Michael Fisher
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6814)


The formal analysis of computational processes is by now a well-established field. However, in practical scenarios, the problem of how we can formally verify interactions with humans still remains. In this paper we are concerned with addressing this problem. Our overall goal is to provide formal verification techniques for human-agent teamwork, particularly astronaut-robot teamwork on future space missions and human-robot interactions in health-care scenarios. However, in order to carry out our formal verification, we must first have some formal basis for this activity. In this paper we provide this by detailing a formal operational semantics for Brahms, a modelling/simulation framework for human-agent teamwork that has been developed and extensively used within NASA. This provides a first, but important, step towards our overall goal by establishing a formal basis for describing human-agent teamwork, which can then lead on to verification techniques.


Rational Agent Model Check Multiagent System International Space Station Operational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bordini, R.H., Dennis, L.A., Farwer, B., Fisher, M.: Automated Verification of Multi-Agent Programs. In: Proc. 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 69–78 (2008)Google Scholar
  2. 2.
    Bordini, R.H., Fisher, M., Sierhuis, M.: Formal Verification of Human-Robot Teamwork. In: Proc. 4th ACM/IEEE International Conference on Human Robot Interaction (HRI), pp. 267–268. ACM Press, New York (2009)CrossRefGoogle Scholar
  3. 3.
    Clancey, W., Sierhuis, M., Kaskiris, C., van Hoof, R.: Advantages of Brahms for Specifying and Implementing a Multiagent Human-Robotic Exploration System. In: Proc. 16th Florida Artificial Intelligence Research Society (FLAIRS), pp. 7–11. AAAI Press, Menlo Park (2003)Google Scholar
  4. 4.
    Clancey, W.J., Sierhuis, M., Seah, C., Buckley, C., Reynolds, F., Hall, T., Scott, M.: Multi-agent Simulation to Implementation: A Practical Engineering Methodology for Designing Space Flight Operations. In: Artikis, A., O’Hare, G.M.P., Stathis, K., Vouros, G.A. (eds.) ESAW 2007. LNCS (LNAI), vol. 4995, pp. 108–123. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  5. 5.
    Dennis, L.A., Fisher, M., Lisitsa, A., Lincoln, N., Veres, S.M.: Satellite Control Using Rational Agent Programming. IEEE Intelligent Systems 25(3), 92–97 (2010)CrossRefGoogle Scholar
  6. 6.
    Holzmann, G.J.: Software model checking with SPIN. Advances in Computers (2005)Google Scholar
  7. 7.
    Rao, A.S., Georgeff, M.: BDI Agents: From Theory to Practice. In: Proc. 1st International Conference on Multi-Agent Systems (ICMAS), San Francisco, USA, pp. 312–319 (1995)Google Scholar
  8. 8.
    Rao, A.S., Georgeff, M.P.: Modeling Agents within a BDI-Architecture. In: Proc. Conference on Knowledge Representation & Reasoning (KR). Morgan Kaufmann, San Francisco (1991)Google Scholar
  9. 9.
    Sierhuis, M.: 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)Google Scholar
  10. 10.
    Sierhuis, M.: Multiagent Modeling and Simulation in Human-Robot Mission Operations (2006),
  11. 11.
  12. 12.
    Sierhuis, M., Bradshaw, J.M., Acquisti, A., Hoof, R.V., Jeffers, R., Uszok, A.: Human-Agent Teamwork and Adjustable Autonomy in Practice. In: Proc. 7th International Symposium on Artificial Intelligence, Robotics and Automation in Space, i-SAIRAS (2003)Google Scholar
  13. 13.
    Sierhuis, M., Clancey, W.J.: Modeling and Simulating Work Practice: A Human-Centered Method for Work Systems Design. IEEE Intelligent Systems 17(5) (2002)Google Scholar
  14. 14.
    Sierhuis, M., Clancey, W.J., van Hoof, R.J., Seah, C.H., Scott, M.S., Nado, R.A., Blumenberg, S.F., Shafto, M.G., Anderson, B.L., Bruins, A.C., Buckley, C.B., Diegelman, T.E., Hall, T.A., Hood, D., Reynolds, F.F., Toschlog, J.R., Tucker, T.: NASA’s OCA Mirroring System: An application of multiagent systems in Mission Control (2009)Google Scholar
  15. 15.
    Plotkin, G.D.: A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Computer Science Department. Aarhus University, Denmark (1981)Google Scholar
  16. 16.
    Stocker, R., Sierhuis, M., Dennis, L., Dixon, C., Fisher, M.: A Formal Semantics for the Brahms Language (2011),
  17. 17.
    van Hoof, R.: Brahms website (2000),
  18. 18.
    Wooldridge, M.: An Introduction to Multiagent Systems. John Wiley & Sons, Chichester (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Richard Stocker
    • 1
  • Maarten Sierhuis
    • 2
    • 3
  • Louise Dennis
    • 1
  • Clare Dixon
    • 1
  • Michael Fisher
    • 1
  1. 1.Department of Computer ScienceUniversity of LiverpoolUK
  2. 2.PARCPalo AltoUSA
  3. 3.Man-Machine InteractionDelft University of TechnologyDelftThe Netherlands

Personalised recommendations