r
i
⊃
♦
g
i
;
(5)
g
i
⊃
♦
¬
r
i
;
(6)
¬
r
i
⊃
♦
¬
g
i
.
(7)
Четыре первых утверждения характеризуют поведение программы
в соседние моменты времени или состояния. В более глобальном сти-
ле свойства предусмотренной реакции можно выразить следующими
выражениями:
r
i
⊃
[
r
i
U
(
g
i
∧
r
i
)];
(
а
)
g
i
⊃
[
g
i
U
(
¬
r
i
∧
g
i
)];
(
b
)
¬
r
i
⊃
[
r
i
U
(
¬
g
i
∧ ¬
r
i
)];
(
c
)
g
i
⊃
(
r
i
P
g
i
)
.
(
d
)
Эти выражения заменяют все остальные. Утверждение (
a
)
говорит
о том, что ес ли
r
i
истинно, то оно должно оставаться истинным до
тех пор, пока
g
i
истинно. Утверждение (
b
)
говорит о том, что если
ресурс предоставлен, то он остается предоставленным до тех пор,
пока от него не откажутся. Утверждение (
c
)
говорит о том, что если
от ресурса отказались, то он не может быть затребован до тех пор,
пока отказ от него не будет признан. Утверждение (
d
)
говорит о том,
что если
g
i
в данный такт не назначено, то его следующему значению
должен предшествовать запрос.
Справедливая реакция
(
φ
1
P
φ
2
)
⊃
(
ϕ
1
P
ϕ
2
);
φ
1
⊃
♦
ϕ
1
;
φ
2
⊃
♦
ϕ
2
.
Пример
. Распределение ресурсов. Рассмотрим снова обслужива-
емые диспетчером процессы. Наложим на них требование условного
предшествования:
(
r
i
P
r
ϕ
)
⊃
(
g
i
P
g
ϕ
)
, которое означает, что ес ли
процесс
P
i
поместил свой запрос раньше процесса
P
ϕ
, то он раньше
и будет обслужен. Однако здесь необходимо быть осторожным, ставя
жесткие условия. Например, если
g
i
истинно, в то время, как оба
r
i
и
r
ϕ
ложны, то может иметь место ситуация, когда нельзя обещать, что
g
i
будет предшествовать
g
ϕ
. Для исключения такой ситуации необходимо
исходить из ложности
g
ϕ
. Тогда выражение условного предшествова-
ния будет выглядеть следующим образом:
(
¬
g
ϕ
)
⊃
[(
r
i
P
r
ϕ
)
⊃
(
g
i
P
g
ϕ
)]
.
Пример формулировки свойств правильного поведения аген-
тов.
Имеется
k
агентов. Агент
A
1
является отправителем кадров, аген-
ты
A
2
,
A
3
, . . . , A
k
— передатчиками кадров. Агент
A
1
помещает кадры
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2005. № 4 73
