Свойство обязательной реакции
Пользователь обращается к ИЧМИ, используя различные модальности. Будем полагать для простоты здесь и далее до конца статьи, что это обращение происходит в дискретном времени. И какое бы количество модальностей не использовалось в каждый момент времени t набор значений использованных модальностей преобразуется в последовательность входных макросостояний x(t). Это входное макросостояние можно рассматривать как символ некоторого языка. Последовательность таких символов является предложением языка. Если для обращения используется только текстовый язык (например, DISL, GIML, ISML [Guerrero-Garcia et al., 2009]), то входное состояние может соответствовать как отдельному символу этого языка, так и его словам или предложениям. В данном случае для нас это непринципиально. Если для обращения используются сенсоры [Shinjo, 2005], речь, жесты или графика [Maybury, 2002], то и в этом случае мы полагаем, что в результате при обращении к ИЧМИ формируется последовательность входных макросостояний. В ответ на эту последовательность входных макросостояний ИЧМИ формирует ответную реакцию. Эта реакция может быть на том же или другом языке, с использованием тех же или других модальностей, и является последовательностью выходных макросостояний, являющейся ответом на обращение пользователя.
Таким образом, свойство обязательной реакции на языке временной модальной логики выглядит следующим образом.
(x) (входное(x)? внутреннее(bi) ?(внутреннее(bj, bj=f(x, bi)) ?выходное (yj, yj?=?(bj))?
Это свойство читается следующим образом: «Когда на входе ИЧМИ в некоторый момент времени появилось входное макросостояние x, то ИЧМИ, находящийся во внутреннем макросостоянии bi, в следующий момент времени перейдет в состояние bj и на его выходе появится выходное состояние yj». И это правило справедливо для всех x. Поэтому можно проверить реакцию ИЧМИ на любое входное макросостояние.
