φ
2
⊃
♦
ϕ
2
выражение условного предшествования называется справедливой ре-
акцией. Иначе говоря, если
φ
1
⊃
♦
ϕ
1
и
φ
2
⊃
♦
ϕ
2
интерпре-
тируются, как ответ
ϕ
i
на требование
φ
i
, то справедливая реакция
дополнительно требует: если
φ
1
предшествует
φ
2
, то ответ на
φ
1
, а
именно
ϕ
1
, должен предшествовать ответу на
φ
2
, а именно
ϕ
2
.
Свойства агентов.
Агенты — это интеллектуальные параллельно
работающие процессы. Поэтому проверка свойств поведения агентов
— это, по существу, проверка определенных свойств этих процессов.
Практически все из рассмотренных свойств потоков несколько в иной
интерпретации применимы и для проверки свойств поведения объек-
тов. Чтобы это было более очевидным, будем полагать, что вычисли-
тельной моделью процессов являются конечные автоматы. В отличие
от автомата
M
j
:
, представляющего поток, функции перехода и выхода
агента
A
j
:
имеют следующий вид:
ϕ
(
b
j
(
t
i
)) =
c
j
(
t
i
)
,
f
(
b
j
(
t
i
)
, a
(
t
i
+1
)) =
b
j
(
t
i
+1
)
.
Здесь
c
j
(
t
i
)
является значением функции выхода
ϕ
, а значением
функции выхода в общеупотребительном смысле теории автоматов
а
(
t
i
+1
)
— входное условие при истинном значении которого проис-
ходит переход из состояния
b
j
(
t
i
)
в состояние
b
j
(
t
i
+1
)
, являющеес я
значением функции переходов
f
. Далее те свойства поведения аген-
тов, которые с точностью до обозначений совпадают со свойствами
потоков, только перечислим в новых обозначениях. Большее внима-
ние уделим свойствам поведения агентов, не имеющим аналогов среди
свойств потоков.
Инвариантные свойства.
Корректное завершение
(
s
(
b
(
t
0
))
∧
φ
(
x
(
t
0
)))
⊃
[
s
(
b
(
t
e
))
⊃
ϕ
(
x
(
t
e
)
, c
(
t
e
))]
.
Чистое поведение
(
s
(
b
(
t
0
))
∧
φ
(
x
(
t
0
)))
⊃ ∧
i
∈
I
(
s
(
b
(
t
i
))
⊃
ψ
(
x
(
t
i
)
, c
(
t
i
)))
.
Глобальная инвариантность
(
s
(
b
(
t
))
∧
φ
(
x
(
t
)))
⊃
(
ϕ
(
x
(
t
)
, c
(
t
)))
.
Взаимное исключение критических секций.
Каждый агент
A
j
явля-
ется процессом
P
j
. Если процессы
P
l
,
P
k
, являющиеся автоматами,
68 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2005. № 4
