A formal semantics for Brahms

Research output: Chapter in Book/Conference proceedingChapterpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationComputational Logic in Multi-Agent Systems
Subtitle of host publication12th International Workshop, CLIMA XII, Barcelona, Spain, July 17-18, 2011. Proceedings
PublisherSpringer Nature
Pages259-273
Number of pages15
ISBN (Electronic)978-3-642-22359-4
ISBN (Print)978-3-642-22358-7
DOIs
Publication statusPublished - 2011
EventCLIMA: International Workshop on Computational Logic in Multi-Agent Systems - Barcelona, Spain
Duration: 17 Jul 201118 Jul 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6814
NameLecture Notes in Artificial Intelligence
PublisherSpringer
Volume6814

Conference

ConferenceCLIMA: International Workshop on Computational Logic in Multi-Agent Systems
Abbreviated title12th International Workshop, CLIMA XII
Country/TerritorySpain
CityBarcelona
Period17/07/1118/07/11

Fingerprint

Dive into the research topics of 'A formal semantics for Brahms'. Together they form a unique fingerprint.

Cite this