178
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
(
)
{ } { } { } .
a
b
t
P P P P P P
=
… ′
′
′
Процесс
,
P
′′′
состоящий из процессов
,
, ,
a b
t
P P P
…
,
которые выполняются параллельно, обозначим как
(
)
.
a b
t
P P P P
… ′′′
&
&
Описание свойств процессов проекта ИМИ.
Моделью каждого
проекта ИМИ является некоторый процесс. Частный случай описания
процессов — описание их на языке графов переходов в виде сово-
купности параллельно функционирующих и взаимодействующих ав-
томатов. С помощью такого описания требуемые свойства ИМИ мо-
гут быть сформулированы на языке модальной логики [11]. Для этого
используются различные модальные операторы, например:
c
ξ
—
формула
ξ
будет истинной в ближайшем будущем;
◊ξ
—
формула
ξ
станет истинной когда-нибудь в будущем;

ξ
—
формула
ξ
была ис-
тинной когда-то в прошлом.
В соответствии с идеологией временной модальной логики
символы времени в формулах не применяются. Согласно теореме
Габбэя, любая формула временной модальной логики может быть
переписана в логически эквивалентную форму с учетом правил вида:
прошлое
⊃
будущее
[12].
Описание требуемых свойств ИМИ на языке модальной логики лег-
ко применимо к случаю, когда проект ИМИ представляется в виде про-
цессных выражений. Так, свойство обязательной реакции в терминах
процессных понятий на естественном языке формулируется в виде вы-
сказывания: если в прошлом процесс
P
выполнял последовательность
действий
0 1 2
2
. . ....
. .
m m
a a a a a
−
,
то в будущем он должен обязательно вы-
полнить последовательность действий
0 1 2
2
. . ....
. .
n n
b b b b b
−
[11].
На языке модальной логики приведенному выше высказыванию
удовлетворяют, например, следующие, но не единственные формулы:
0 1 2
2
( . . ....
. .)
m m
f a a a a a
−
⊃
c
0 1 2
2
( . . ....
. .).
n n
b b b b b
ϕ
−
,

0 1 2
2
( . . ....
. .)
m m
f a a a a a
−
⊃
◊
0 1 2
2
( . . ....
. .).
n n
b b b b b
ϕ
−
Здесь
0 1 2
2
( . . ....
. .)
m m
f a a a a a
−
и
0 1 2
2
( . . ....
. .)
n n
b b b b b
ϕ
−
—
предикаты, ис-
тинные на последовательностях
0 1 2
2
. .
. .
m m
a a a a a
−
…
и
0 1 2
2
. .
. .
n n
b b b b b
−
…
соответственно.
Пример описания альтернативных процессов.
Рассмотрим
введенные понятия на примере процесса ИМИ телевизора. Процесс
ИМИ предполагает наличие у каждого пользователя нескольких мо-
дальностей, с помощью которых он управляет работой телевизора
(
выключить или не выключить):
m
1 —
статические жесты;
m
2 —
кнопочный пульт;
m
3 —
мимика лица;
m
4 —
голосовые команды;
m
5 —
динамические жесты. Вокруг телевизора выделим три зоны, в
которых могут быть распознаны перечисленные модальности:
m
1,