11 / 23
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. «Приборостроение». 2016. № 3
75
модействию руководителя и некоторого исполнителя состоит в следу-
ющем. На каждую реакцию руководителя, в результате которой в его
выходных каналах, являющихся одновременно входными каналами для
какого-либо исполнителя, окажутся сообщения, предназначенные для
последнего, исполнитель обязательно должен получить эти сообщения и
реагировать на них помещением в свои выходные каналы, являющиеся
одновременно входными для руководителя, ответных сообщений.
На языке модальной логики формулировка этого свойства для
рассматриваемого примера может выглядеть так:
1
1
1
1
1
1
2
1
2
1
1
2
1
1
1
2
2
2
1
1
1
[
(
(1 ,
2
1
)
( ))
(
1-
(
( ))
(
2-
1 (
( ))
(
(
(
)
)
)
,
,
,
,
, (
)
1-
(
( )
,
,
, (
,
,
, (
1 , )
И И
И
И И
И
И И
Р
Р
И
Р
Поместить
x
y
И Получ
РИ РИ
Р ить
x
И Получит Рь
x
И
И
sequent
?s f
!s
sequent
?s
f
!s
sequent
?s
f
!s
sequent
?s
f И Поместить
v И Р !s
2
2
2
2
2
2
2
2
(
)
2-
(
( ))
)
(
,
,
, (
2
,
,
,
1
(
(
( )
( ))
)
, 2
]
,
.
И
Р
И
Р
И
Р
sequent
?s
f
И Р !s
sequent
?s
f
И
И Поместить
w
Получит Р И Р !s
ь
v
w
Здесь каждый предикат
sequent
(
,
?s
i
,
f
(
!a
o
),
!s
o
)) представляет секвент
:
,
i
i
o
o
?a
s
!a
?s !
где
f
(
?a
i
,
!a
o
) — функтор, структура которого может быть
достаточно сложной в зависимости от структуры реакции
!a
o
в конкретном
приложении;
?s
i
,
!s
o
— конфигурации.
Процедура проверки свойств интеллектуального интерфейса.
Формулировка любого свойства интеллектуального интерфейса на
языке модальной логики — утверждение, которое требует определен-
ной процедуры доказательства. В частности, свойство обязательной
реакции предполагает, что в любом макросостоянии, являющемся со-
вокупностью состояний руководителя и исполнителей, это утвержде-
ние должно быть истинным. Следовательно, процедура доказательства
может быть разбита на два этапа: 1) генерация всех возможных макро-
состояний; 2) проверка в каждом макросостоянии истинности свойства
обязательной реакции. Генерация макросостояний может быть осу-
ществлена с помощью правила параллельной композиции, которое для
рассматриваемого примера будет иметь вид
:
, :
, :
.
:
i
i
i
i
o
i
o
i
o
o
o
o
i
i
i
i
i
i
o
o
o
o
o
o
?a
?a
?a
s
s
s
!a
!a
!a
s
s
s
?s
!
?s
!
?s
!
?a ?a ?a
?s ?s ?s
!
!
!
!a !a !a
Это правило позволяет генерировать все макросостояния
,
тре-
буемые для проверки свойства обязательной реакции. В рамках настоя-