во время
t
поток находился в состоянии
b
(
t
)
и формула
φ
была ис-
тинна. Состояние
b
(
t
)
при этом не обязательно достигается в первый
раз.
В отличие от свойства гарантированного осуществления свойство
безопасности
[
s
(
b
(
t
))
∧
φ
(
x
(
t
)
, y
(
t
))]
⊃
[(
¬
s
(
b
(
t
))
U
[
s
(
b
(
t
))
∧
φ y
(
t
)
, x
(
t
)])]
означает следующее: если поток находится в состоянии
b
(
t
)
и форму-
ла
φ
(
x
(
t
))
истинна, то через некоторое время поток должен достичь
состояния
b
(
t
)
и при первом же приходе в это состояние формула
φ
должна стать истинной.
Предусмотренная реакция.
Свойства, выражаемые формулой
w
1
⊃
♦
w
2
, относятся к числу свойств, которые гарантируют, что в
случае истинности формулы
w
1
, истинной станет формула
w
2
. Час то
желательно дополнить это свойство требованием, чтобы формула
w
2
никогда не становилась истинной, если этому не предшествует истин-
ность формулы
w
1
. Это свойство в общем случае выразимо с помощью
оператора предшествования, но требует в каждом конкретном случае
тщательного выбора времени наблюдения. Хорошим примером вы-
ражения, задающего свойство предусмотренной реакции, является
следующее:
[
s
(
b
(
t
0
))
⊃
w
1
P
w
2
]
∧
[(
w
2
∧
N
¬
w
2
)
⊃
N
(
w
1
P
w
2
)]
.
Этот пример иллюстрирует тщательный выбор времени наблю-
дения, когда предшествование
w
1
по отношению к
w
2
может быть
наблюдаемым либо из начального состояния, либо во время, когда
w
2
истинна и изменяет свое значение на ложное в следующий момент
времени (здесь
N
означает “в следующий момент времени”). В боль-
шинстве практических случаев имеется дополнительная информация
о формулах
w
1
и
w
2
, которая помогает сформулировать требования в
более простой форме.
Справедливая реакция.
Во многих ситуациях предшествование
двух событий
ϕ
1
и
ϕ
2
связано с более ранними событиями
φ
1
и
φ
2
,
такими, что
φ
1
предшествует событию
φ
2
. Такую ситуацию будем
называть условным предшествованием. Она представляется выраже-
нием
(
φ
1
P
φ
2
)
⊃
(
ϕ
1
P
ϕ
2
)
.
Оно означает, что если
φ
1
предшествует
φ
2
, то
ϕ
1
предшествует
ϕ
2
. Вместе с выражениями
φ
1
⊃
♦
ϕ
1
,
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2005. № 4 67
