@inproceedings{5046580c09094aee95af46f889a9b22a,
title = "Verifying Brahms human-robot teamwork models",
abstract = "Collaboration between robots and humans is an increasingly important aspect of industrial and scientific settings. In addition, significant effort is being put into the development of robot helpers for more general use in the workplace, at home, and in health-care environments. However, before such robots can be fully utilised, a comprehensive analysis of their safety is necessary. Formal verification techniques are regularly used to exhaustively assess system behaviour. Our aim is to apply such techniques to Brahms, a human-agent-robot modelling language. We show how to translate from Brahms scenarios, using a formal semantics for Brahms, into the input language of a model checker. We illustrate the approach by defining, translating, and verifying a domestic robot helper example.",
author = "R. Stocker and L. Dennis and C. Dixon and M. Fisher",
year = "2012",
doi = "10.1007/978-3-642-33353-8\_30",
language = "English",
isbn = "978-3-642-33352-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature",
pages = "385--397",
booktitle = "Logics in Artificial Intelligence",
address = "United States",
note = "13th European Conference, JELIA 2012 ; Conference date: 26-09-2012 Through 28-09-2012",
}