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