Исходя из того, что ИЧМИ должна самостоятельно принимать решения о выборе в зависимости от ситуации стратегии «безбарьерного» интерфейса, наиболее подходящей архитектурой для создания ИЧМИ является мультиагентная архитектура. Для удобства формулировки последующих свойств будем полагать, что мультиагентная архитектура ИЧМИ является реактивной [Brooks, 1999]. Моделью каждого из агентов этой архитектуры будет являться конечный автомат, и таким образом, моделью ИЧМИ является совокупность M1, M2,…, Mm параллельно функционирующих и взаимодействующих автоматов. Пусть b(t)={b1(t),…, bm(t)} - множество внутренних состояний соответственно автоматов {M1, M2,…, Mm} в момент времени t, называемое внутренним макросостоянием; yj(t) =??(bj(t)) — функция выходов автомата Mj, bj(t+1)=fj(xj(t), bj(t)) функция переходов автомата Mj, где bj(t), bj(t+1) — внутренние состояния автомата Mj; y(t)={y1(t),…, ym(t)} - внутреннее макросостояние; внутреннее(b(t)) — предикат, принимающий истинное значение, когда автоматы находятся в макросостоянии b(t), входное(x(t)) — предикат, принимающий истинное значение, когда на входы автоматов поступает входное макросостояние x(t); выходное(y(t)) — предикат, принимающий истинное значение, когда на выходе автоматов появляется выходное макросостояние у(t); y(t)=?(b(t)) — макрофункция выходов, b(t+1)=f(x(t),b(t)) макрофункция переходов автоматов Используя введенные обозначения, сформулируем свойства ИЧМИ в виде формул временной модальной логики. Для этого будем использовать модальные операторы, сведенные в таблицу.
|
Обозначение оператора. | Значение оператора. | |
| будет истинной в следующий момент времени. | |
| была истинной в предыдущий момент времени. | |
| станет истинной в некоторый следующий момент времени. | |
| всегда истинна в следующие моменты времени. | |
| была истинной в некоторый предыдущий момент времени. | |
| была всегда истинной в предыдущие моменты времени. | |
u. | будет истинной до тех пор, пока истинна. | |
s. | станет истинной, как только станет истинной. | |
w. | истинна тогда, когда истинна. | |
|
В соответствии с идеологией временной модальной логики символы времени в формулах не употребляются. А согласно теореме Габбэя [Gabbay, 1977] любая формула временной модальной логики может быть переписана в логически эквивалентную форму с использованием правил вида прошлое будущее.
Среда, с которой имеет дело агентная ИЧМИ состоит из пользователей. С этими пользователями агенты общаются с помощью использования предикатов двух типов: посылаемых и получаемых предикатов. Посылаемые предикаты находятся в левой части правила, а получаемые — в правой.
