A Formal Framework for Design and Validation of Multimodal Interactive Systems in Transport Domain - Human-Computer Interactions in Transport - page 105

This formula means that in the transition of the HCI (all the execution traces), if
stateI is identified as being the initial state of task T , then all the states that follow
it are reached by m 1 modality until reaching the stateF , which identifies the end of
task T , or they are reached by m 2 modality until they reaching stateF identifying the
end of task T .

4.4.3.4. Redundancy

To express the property of redundancy in the LTL temporal logic, we must
enumerate all possible combinations between the modalities in each state. We have
not been able to represent this properly in a generic expression of LTL logic. It
requires a richer logic, enabling us to express the parallel operator.

4.4.4. Case study

To illustrate the approach previously described, we have chosen MATIS
( Multimodal Airline Travel Information System ), the multimodal application
described in [MAC 98, NIG 94]. It enables a user to extract information regarding
the times of flights using voice, direct handling with the keyboard and the mouse, or
a combination of these modalities, by basing itself on the individual or synergistic
use of numerous input modalities. For each request, a window is created following
an order from the user. It contains fields filled in with values corresponding to the
parameters of the request, such as the names of the flight departure and arrival towns.
The user can fill in these fields by saying town names that are recognized by the
system or by clicking on the fields before selecting a town from among the suggested
list.

4.4.4.1. Modeling of the input interaction

For reasons of simplification, we will model an multimodal HCI that will enable
the user to formulate a single request. We will consider two modalities: speech and
direct handling with the mouse. A speech and A handle are the set of actions of the system
generated, respectively, by the speech and direct handling modalities using the mouse:

A speech = { 'show me flights' , 'from' , 'this' , 'City' , 'To' , 'Boston' , 'Oslo' }

A handle = { ClicBoston , ClicOslo , ClicFrom , ClicTo , ClicNrequest }

With the following basic actions made using the mouse:
- ClicBoston , ClicOslo : click the mouse on the town of Boston and the town of
Oslo, respectively, from a list of towns;
- ClicFrom , ClicTo : click the mouse on the text field, respectively From and To of
the form for request input;