Ironies of Automation - Ryan

Interesting things I didn't think about:

Solutions?

HRI Survey - Ryan

Obviously, Human-machine interactions has been around as long as machines have.

I agree that HRI is a separate field, but one that requires expertise of many different kinds of people.

Interesting that peer relationships require more autonomy than having the robot just work alone. It makes sense, though, because not only does it need to be able to operate on its own, but it also needs to be able to react in human ways on its own as well, which is much harder.

Information exchange is an important problem with what we are dealing with. We need to make sure the information exchange between the robot and the operator is fast and as complete as possible, so that the operator can react appropriately.

Our problem will require significant UAV automation as well as operator training.

This should have been more obvious to me, but there must be existing models we can use to supplement ours. For example, in terms of how and when to switch between automation and manual control, airplane operators are a good example where we can take information.

Computation Engineering - Ryan

21

Model checking is to verify finite-state model of reactive computing systems for proper behavior.

Computer systems should be reliable, and assurances should be the norm rather than the exception.

Model checking requires

Obviously, we are using a Reactive Computing System

Model checking best used in early conceptual design stages

Desired properties expressed using linear-time temporal logic or automata.

Model checking using over-approximation: assume testable state at all possible origin states

Safety Violations - something bad happens Liveness Violations - stuck in loop that doesn't include desired end state

Liveliness error for Three Philosophers: Why does Phil:1 starve? Doesn't Phil:5 release Fork:6? Page 395

22

Kripke Structures - used to model concurrent systems over time

Computational Tree Logic Syntax

An LTL formula is true of a Kripke structure iff it is true of EVERY infinite path of the Kripke structure considered separately.

How exactly do you use the GFP or LFT algorithms for this? Page 413

Wilderness Research UAV - Ryan

Minimizing time to find person is a balance between quickly covering area and going slow enough that people watching camera feed can detect signs.

In rugged terrain, better to follow contours of terrain than probability

Mosaic camera views significantly better than just showing the camera feed.

Manager wanted to perform efficient search, which makes it incomplete, and the UAV was required to spend lots of time focusing on potential signs, making the search both inefficient and incomplete.

The (sensor) operator is required to direct the camera to make sure that adequate coverage occurs. Would it not be possible to automate the direction of the camera as well as the actual flight, to free the operator from that task?

We may need to have the models be flexible enough that they can change based on what search paradigm is being employed - sequential, remote-led, or base-led.