14 / 18
В.С. Буренков, С.Р. Иванов
62
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1
Защита
g
имеет вид
1
2
,
g A A
где
1
1
,
;
AP
A Cond V C
2
1
,
.
AP
A Cond V C
В
1
A
может входить условие
.
nempty c
В
2
A
не входят условия относительно
каналов. В соответствии с
1
,
Transs
если
1
v
в исходной системе было отправлено
процессом
1
PG
или
2
,
PG
то это же справедливо и в абстрактной системе. В таком
случае условие
nempty c
выполняется. Доказательство выполнимости условий
относительно переменных аналогично случаю 1.
Случай б.
Правило исходной системы
i
rrc
, правила абстрактной системы
,
1
, 1
.
t j
raa
j S
Доказательство выполнимости посылки правила абстрактной
системы такое же, как и в случае 1.
Следовательно, в абстрактной системе из состояния
m
f s
существует
множество переходов, в которых всегда найдется переход
1
,
m
m
f s
f s
соответствующий переходу
1
,
m m
s
s
такой, что
1
1
.
abs
m
m
L f s
L s
Случай 2.2:
2
.
c C
Элемент множества правил исходной системы
2
{ |1
}
concrete
i
Rulesr
rrc
i n
имеет вид (5), элемент множества правил абстракт-
ной системы
2
|1
2
abstract
i
Rulesr
rra i
— вид
2,
:
?
2,
2,
1
0
3
0
3
,
|
( ( ))
0
( )
...
,
, , , , ,
,
, , , , ,
,
abs i
g c x
i
i
abs abs
abs
abs
i
abs
i
k
i
i
abs
abs
i
abs
abs
l
l
g
len c
k
c
v v
rra
l
l
l
l
l
l
где
1
:
abs
abs
x v
и
2,
2
.
:
abs
abs
i
k
c
v v
Из выполнимости условия
0
len c
k
в посылке правила
2
,
i
concrete
rrc Rulesr
следует выполнимость
2,
0
abs
i
len
c
k
в посылке пра-
вила
2
.
i
abstract
rra Rulesr
Покажем это рассмотрением фрагмента вычисления
0 1 1 2
m m
s s
s
системы
TS
и соответствующего фрагмента вычисления
0
1
1
2
( )Α ( )Α Α ( )
m m
f s
f s
f s
системы
.
abs
TS
Для случая отправки со-
общения по каналу
2
c C
множество правил исходной системы
2
concrete
Ruless
0
,
rsc
2
2,1
2,
{ , ...,
} :
n
c C c
c
: !
0
0
1
0
0
0
, |
( ( ))
( ) ( ) ...
,
, , , , , ,
, , , , , ,
g c v
k
i
n
i
n
l
l
g len c k cap c
c v v
rsc
l
l
l
l
l
l
где
1 2
:
.
k
c v v v v
Множество правил абстрактной системы
2
0
abstract
Ruless
rsc
,
2,1 2,2
,
:
c c c
: !
0
0
1
0
0
3
0
3
,
|
( ( ))
( )
( )
... ,
, , , , ,
,
, , , , ,
,
abs
g c v
abs abs
abs
abs
abs
k
i
abs
abs
i
abs abs
l
l
g
len c k cap c
c v v
rsa
l
l
l
l
l
l
где
1 2
:
.
abs
abs
k
c v v v v