Чистое поведение.
Свойство чистого поведения обусловливает вы-
полнение определенных условий
ψ
(
x
(
t
i
)
, y
(
t
i
))
, ес ли
i
пробегает мно-
жество значений
i
∈
I
⊆ {
1
,
2
, . . . , T
}
. Используя введенные обозначе-
ния, свойство чистого поведения записывается следующим образом:
(
s
(
b
(
t
0
))
∧
φ
(
x
(
t
0
)))
⊃ ∧
i
∈
I
(
s
(
b
(
t
i
))
⊃
ψ
(
x
(
t
i
)
, y
(
t
i
)))
.
Например, с помощью свойства чистого поведения можно ука-
зать, что значения
y
j
(
t
i
)
не должны превосходить определенный порог,
иметь общий делитель и т.п
Глобальная инвариантность.
Очень часто некоторые инвариант-
ные свойства не зависят от какого-либо конкретного внутреннего со-
стояния или макросостояния. Свойство глобальной инвариантности в
общем виде выглядит следующим образом:
φ
(
x
(
t
))
⊃
ϕ
(
x
(
t
)
, y
(
t
))
.
т.е. всегда, когда имеет место
φ
(
x
(
t
))
, имеет также место и
ϕ
(
x
(
t
)
, y
(
t
))
.
Сигнальное взаимное исключение.
Понятие сигнального взаим-
ного исключения связано с понятием сигнальной критической сек-
ции. Напомним суть этого понятия применительно к предмету на-
шего рассмотрения. Как уже говорилось, каждый отсчет является
значением функции выхода
y
j
(
t
) =
ϕ
(
b
j
(
t
))
автомата
M
j
, каждый
сигнал является последовательностью значений функций выхода
y
j
(
t
) = (
y
j
(
t
0
)
, y
j
(
t
1
)
, . . . , y
j
(
t
e
))
одного и того же автомата
M
j
. Рас -
смотрим любую пару автоматов
{
M
l
, M
k
} ⊆ {
M
1
, M
2
, . . . , M
m
}
. Пус ть
автоматы
M
l
, M
k
достигли одновременно состояний
b
l
(
t
)
, b
k
(
t
)
. На-
зовем последовательности состояний
DS
l
= (
b
l
(
t
)
, . . . , b
l
(
t
+
r
))
и
DS
k
= (
b
k
(
t
)
, . . . , b
k
(
t
+
s
))
взаимно исключающими, если какие-
либо условия не должны выполняться, когда автоматы находятся в
каких-либо состояниях этих последовательностей. Обозначим
π
(
DS
j
)
условие, которое истинно, если автомат
M
j
находится в одном из
состояний последовательности
DS
j
. Тогда свойство сигнального вза-
имного исключения
DS
l
и
DS
k
может быть представлено следующим
образом:
s
(
b
(
t
0
))
⊃ ¬
(
π
(
DS
l
)
∧
π
(
DS
k
))
∧
t t
0
.
Иначе его можно переписать следующим образом:
s
(
b
(
t
0
))
⊃ ¬
[(
s
(
b
l
(
t
))
∨
. . .
∨
s
(
b
l
(
t
+
r
)))
∧
(
s
(
b
k
(
t
))
∨
. . .
. . .
∨
s
(
b
k
(
t
+
r
)))]
∧
t t
0
.
64 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2005. № 4
