Power Plant Control Room reference
baxter Baxter
787 Cockpit reference
Predator Drone Control Room reference
State flow in WiSAR

AAAI 2014 Symposium Overview

The goal of the workshop is to bring together the fields of formal verification, cognitive modeling, and task analysis to study the design and verification of real fieldable human-machine systems. Recent papers in each of these communities discuss modeling challenges and the application of basic formal verification in human-machine interaction; however, there is little communication between researchers in these different areas and there are many open questions that require cross-disciplinary collaboration. The workshop is to bring together experts from many communities in an environment where it is possible to explore key research areas, common solutions, near-term research problems, and advantages in combining the best of the different communities.

Research Challenges

  • What model classes, methodologies, and constructs are appropriate for modeling human and
        machine activities in a way that is amenable to formal verification? Examples include

    • Programming languages

    • State Machines

    • Activity models (e.g. Brahams)

    • Cognitive models (SOAR, ACT-R, DIARC, etd.)

    • Task analyses-based models (GDTA, CWA, etc.)

    • Probabilistic models

    • Behavioral game theory

  • What levels of abstraction are appropriate for such modeling, and what information is lost in using
        abstraction?

  • What is the role for formal verification in an evaluation space that also includes simulation as well
        as human in the loop experimentation?

  • What are the contexts, if any, for which the trade offs between authority between humans, autonomy,
        and model-based reasoning can be specified?

  • What is the impact on design for including explicit (meta-) reasoning models in the human-machine
        interaction loop?

  • What types of formal verification tools are appropriate, and what other lessons from formal verification
        apply to human-machine systems?

  • What are the ethical considerations of using verified models to allocate responsibility and authority
        between humans and machines?

  • What organizational structures are appropriate for human-machine collaborative work?

    • Master-slave

    • Teammates

    • Principal-agent

  • How can dynamic models evolve in the presence of learning agents, both human and machine, and
        in the presence of inaccurate mental models.

    • Format

    The symposium will consist of presentations of relevant current work and position papers. We will have invited talks from leaders in the field, working groups, and a panel to foster a general discussion of issues. The symposium is intended to serve as a springboard for the emerging research direction on this very important and useful problem.