Кадровое взаимное исключение.
Каждый кадр — это набор
y
(
t
) =
= (
y
1
(
t
)
, . . . , y
m
(
t
))
значений функций выхода различных автома-
тов
M
1
, M
2
, . . . , M
m
, определенный на внутреннем макросостоянии
b
(
t
)
, т.е.
y
(
t
) =
ϕ
(
b
(
t
))
. Поток кадров является последовательно-
стью кадров. Назовем последовательности макросостояний
DK
l
=
= (
b
l
(
t
1
)
, . . . , b
l
(
t
1
+
r
))
и
DK
k
= (
b
k
(
t
2
)
, . . . , b
k
(
t
2
+
s
))
, где
{
(
t
1
+
r
)
−
t
1
}∩{
(
t
2
+
s
)
−
t
2
}
=
∅
, взаимно исключающими, если какие-
либо условия не должны выполняться, когда автоматы находятся во
внутренних макросостояниях этих последовательностей. Обозначим
π
(
DK
j
)
условие, которое истинно, если автоматы
M
1
, M
2
, . . . , M
m
на-
ходятся в одном из макросостояний последовательности
DK
j
. Тогда
свойство кадрового взаимного исключения может быть представлено
следующим образом:
s
(
b
(
t
0
))
⊃ ¬
[
π
(
b
l
(
t
1
)
, . . . , b
l
(
t
1
+
r
))
∧
π
(
b
k
(
t
2
)
, . . .
. . . , b
k
(
t
2
+
s
))]
∧
(
t
1
+
r < t
2
)
.
Свойства осуществимости.
Эта категория свойств выражается
общей формулой
w
1
⊃
♦
w
2
,
означающей, что если формула
w
1
для некоторого потока сигналов или
кадров в какой-то момент времени станет истинной, то
w
2
должна, в
конце концов, также стать истинной. В отличие от свойств инвариант-
ности, которые описывают только сохранение определенных свойств,
свойства осуществимости говорят о том, что некоторые события, в
конце концов, должны осуществиться. Эта формула в определенном
смысле задает цель
w
2
, которая обязательно должна быть достигнута
после истечения некоторого, в общем случае, неизвестного времени.
Абсолютная корректность.
Это свойство похоже на свойство кор-
ректного завершения и имеет смысл только для терминальных авто-
матов. Абсолютная корректность выражается следующим образом:
[
s
(
b
(
t
0
))
∧
ϕ
(
x
(
t
0
)
, y
(
t
0
))]
⊃
♦
[
s
(
b
(
t
e
))
⊃
ϕ
(
x
(
t
e
)
, y
(
t
e
))]
,
Это означает, что если имеется поток, для которого в момент вре-
мени
t
0
имеет место истинность
s
(
b
(
t
0
))
∧
ϕ
(
x
(
t
0
)
, y
(
t
0
))
, то позднее
обязательно наступит время
t
e
, когда все автоматы окажутся в тер-
минальных состояниях и будет иметь место отношение
ϕ
(
x
(
t
e
)
, y
(
t
e
))
(будет истинна формула
ϕ
(
x
(
t
e
)
, y
(
t
e
))
).
Например, если в момент времени
t
0
среднее значение всех функ-
ций выхода (отсчетов), входящих в
y
(
t
0
)
, не более определенной ве-
личины, то в конце концов в момент времени
t
e
оно станет равным
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2005. № 4 65
