Теоретико-категорная характеризация развертки временных сетей Петри
The intention of the paper is to study a category-theoretic characterization of a semantic representation of the behaviour of time Petri nets, which are a time extension of heavily used model for concurrency – Petri nets. First, we introduce a notion of unfolding of a time Petri net and then provi...
Saved in:
| Date: | 2004 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут програмних систем НАН України
2004
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/2323 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Теоретико-категорная характеризация развертки временных сетей Петри/Р.С. Дубцов // Проблеми програмування. — 2004. — N 2,3. — С. 30-36. —Бiбліогр.:11 назв. - рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-2323 |
|---|---|
| record_format |
dspace |
| spelling |
Дубцов, Р.С. 2008-09-17T14:19:42Z 2008-09-17T14:19:42Z 2004 Теоретико-категорная характеризация развертки временных сетей Петри/Р.С. Дубцов // Проблеми програмування. — 2004. — N 2,3. — С. 30-36. —Бiбліогр.:11 назв. - рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2323 681.3 The intention of the paper is to study a category-theoretic characterization of a semantic representation of the behaviour of time Petri nets, which are a time extension of heavily used model for concurrency – Petri nets. First, we introduce a notion of unfolding of a time Petri net and then provide its category-theoretic characterization. ru Інститут програмних систем НАН України Теоретические и методологические основы программирования Теоретико-категорная характеризация развертки временных сетей Петри Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Теоретико-категорная характеризация развертки временных сетей Петри |
| spellingShingle |
Теоретико-категорная характеризация развертки временных сетей Петри Дубцов, Р.С. Теоретические и методологические основы программирования |
| title_short |
Теоретико-категорная характеризация развертки временных сетей Петри |
| title_full |
Теоретико-категорная характеризация развертки временных сетей Петри |
| title_fullStr |
Теоретико-категорная характеризация развертки временных сетей Петри |
| title_full_unstemmed |
Теоретико-категорная характеризация развертки временных сетей Петри |
| title_sort |
теоретико-категорная характеризация развертки временных сетей петри |
| author |
Дубцов, Р.С. |
| author_facet |
Дубцов, Р.С. |
| topic |
Теоретические и методологические основы программирования |
| topic_facet |
Теоретические и методологические основы программирования |
| publishDate |
2004 |
| language |
Russian |
| publisher |
Інститут програмних систем НАН України |
| format |
Article |
| description |
The intention of the paper is to study a category-theoretic characterization of a semantic representation of the behaviour of time Petri nets,
which are a time extension of heavily used model for concurrency – Petri nets. First, we introduce a notion of unfolding of a time Petri net
and then provide its category-theoretic characterization.
|
| issn |
1727-4907 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/2323 |
| citation_txt |
Теоретико-категорная характеризация развертки временных сетей Петри/Р.С. Дубцов // Проблеми програмування. — 2004. — N 2,3. — С. 30-36. —Бiбліогр.:11 назв. - рос. |
| work_keys_str_mv |
AT dubcovrs teoretikokategornaâharakterizaciârazvertkivremennyhseteipetri |
| first_indexed |
2025-11-24T15:56:08Z |
| last_indexed |
2025-11-24T15:56:08Z |
| _version_ |
1850849475165159424 |
| fulltext |
Теоретико-категорная характеризация развертки временных сетей Петри∗∗∗∗
Дубцов Роман Сергеевич
Институт Систем Информатики им А.П. Ершова СО РАН, пр. Академика Лаврентьева, 6, г. Новосибирск,
630090, Россия. Тел.: +7 (383-2) 35-62-59, факс: +7 (383-2) 32-34-94. E-mail: dubtsov@gorodok.net.
The intention of the paper is to study a category-theoretic characterization of a semantic representation of the behaviour of time Petri nets,
which are a time extension of heavily used model for concurrency – Petri nets. First, we introduce a notion of unfolding of a time Petri net
and then provide its category-theoretic characterization.
Введение
Методы теории категорий, получив широкое распространение, в последние десятилетия стали активно
использоваться для описания и изучения параллельных систем и процессов. Объекты категорий представляют
процессы, а морфизмы соответствуют взаимосвязям между поведениями процессов. Теоретико-категорные
методы позволяют классифицировать и унифицировать различные модели параллелизма. Основная идея этого
похода заключается в формальном выражении того факта, что одна модель более выразительна, чем другая, в
терминах вложений (или прообразов).
Сети Петри – одна из популярных моделей параллельных/распределенных систем. Эта модель является
привлекательной, с точки зрения теории, благодаря своей простоте и внутренней параллельной природы, и
часто используется как семантический базис, на котором интерпретируются параллельные языки [6].
В статьях [10, 11] дана теоретико-категорная характеризация поведения сетей Петри, которое
представляется в виде сети-процесса, получаемого посредством развертки сети Петри в ациклическую сеть.
Такой подход дает возможность установить взаимосвязь в виде сопряженных функторов между категориями
сетей Петри и их семантических представлений.
Необходимость в разработке и исследовании параллельных/распределенных систем, функционирующих
в режиме реального времени привела к попыткам ввести понятие времени в формальные модели. В литературе
такие системы часто представляются временными автоматами, содержащими конечное множество счетчиков
[1] и алгебрами временных процессов (см., например, [12]). Однако все эти формализмы базируются на
интерливинговой семантике и не позволяют моделировать параллелизм естественным образом (напрямую). К
временным моделям «истинного параллелизма» относятся временные расширения следующих моделей:
структур событий [7], сетей Петри [3], частично-упорядоченных множеств [5], асинхронных систем переходов
[2] и т.д.
В данной работе рассматриваются временные сети Петри и их семантические представления, а также
дается теоретико-категорная характеризация развертки поведения временной сети Петри в ациклическое
сетевое представление.
Работа состоит из трех частей. В первой части приводятся необходимые сведения из теории категорий.
Вторая часть содержит основные определения, касающиеся сетей Петри и их семантических представлений. В
третьей, основной, части вводятся определения временных сетей Петри и семантики их развертки во временные
сети-процессы, а также дается теоретико-категорная характеризация этой семантики.
1. Элементы теории категорий
В данной части будут приведены основные используемые теоретико-категорные определения (см.,
например [4, 8]).
Определение 1.1. Будем говорить, что задана категория C , если заданы
• класс || C , элементы которого будем называть объектами категории,
• для каждой пары объектов BA, – множество ),( BAC , элементы которого будем называть
морфизмами A в B ,
• для каждой тройки объектов CBA ,, – правило композиции:
композиция пары ),( gf будет обозначаться как gf o
• Для каждого объекта A – морфизм ),(1 AAA C∈ , называемый тождественным,
удовлетворяющие следующим аксиомам:
∗ Работа частично поддержана Российским Фондом Фундаментальных Исследований
(грант №04-01-00789)
).,(),(),(: CACBBA CCC →×o
• Ассоциативность композиции: для любых морфизмов ),( BAf C∈ , ),( CBg C∈ , ),( DCh C∈
выполнено равенство: hgfhgf oooo )()( = ,
• Аксиома тождественности: для любых морфизмов ),( BAf C∈ , ),( CBg C∈ выполнены равенства:
ffB =o1 , gg B =1o .
Определение 1.2. Будем говорить, что задан функтор F из категории A в категорию B , если заданы:
• отображение |||| BA → класса объектов первой категории в класс объектов второй; образ
объекта |A|∈A обозначается как )(AF или просто FA ;
• для каждой пары объектов A∈′AA, отображение ),(), AFFAAA ′→′ BA( ; образ морфизма
),( AAf ′∈A обозначается как )( fF или просто Ff ;
удовлетворяющие следующим аксиомам:
• для каждой пары морфизмов ),( AAf ′∈A , ),( AAg ′′′∈ A верно: )()()( gFfFgfF oo =
• для любого объекта |A|∈A верно: FAAF 1)1( = .
Если нам даны два функтора BA →:F и CB →:G , то поточечная композиция дает нам новый
функтор: CA →:FG o .
Определение 1.3. Пусть даны два функтора BA →:F и BA →:G . Функторным морфизмом
функтора F в функтор G будем называть класс морфизмов ||):( A∈→ AA GAFAα в категории B ,
индексируемый объектами A , такой, что для каждого морфизма Af:A ′→ в категории A выполнено:
AA fGfF αα oo )()( =′ .
Определение 1.4. Обратный конус над функтором CD →:F состоит из
• объекта C∈C ;
• для каждого объекта D∈D – морфизма CFDsD →: в категории C ,
таких, что для каждого морфизма DDd ′→: в категории D верно: Fdss DD o=′ .
Определение 1.5. Обратный предел функтора CD →:F – это обратный конус ))(,( D∈DDsL над F ,
такой, что для любого другого обратного конуса ))(,( D∈DDtM существует единственный изоморфизм
MLm →: такой, что DD smt o= . Для обозначения обратного предела будем использовать следующую
запись: )Colim(F .
Определение 1.6. Пусть BA →:F – функтор и B – объект категории B . Будем говорить, что задано
отражение B относительно F , если задана пара ),( BBR η , где
• BR – объект A и )(: BB RFB →η – морфизм в B ,
• если |A|∈A – объект A и )(: AFBb → – морфизм в B , то существует единственный морфизм
ARa B →: в A такой, что .)( baF B =ηo
Определение 1.7. Будем говорить, что функтор AB: →R является левым сопряженным к функтору
BA: →F , если существует такой функторный морфизм RF o→B1:η , что для каждого объекта |B|∈B
верно, что ),( BRB η – отражение B относительно F .
2. Элементы теории сетей Петри
В данной части приводятся некоторые определения теории сети Петри из статьи [11], которые будут
использованы в дальнейшем. Начнем с некоторых вспомогательных определений.
Множество мультимножеств над S (т.е. множество функций из S в множество натуральных чисел ω )
будем обозначать через ⊕S , а через ∞⊕S – множество мультимножеств с (возможно) бесконечными
вхождениями (т.е. функций из S в расширенное множество натуральных чисел }{∞∪=∞ ωω ). Носитель
мультимножества µ (т.е. множество элементов Ss ∈ ) будем обозначать через ][ µ .
Мы часто будем обозначать мультимножество ⊕∈ Sµ через формальную сумму ssSs ⋅∈⊕ )(µ . Пусть I
– некоторое множество индексов и дан набор }|{ Iini ∈∈ ∞ω , тогда значение суммы ∑ ∈Ii in будет конечно (и
равно обычной сумме) если и только если множество }0|{ >ii nn конечно; иначе значение суммы равно ∞ .
FA Ff
AF ′
GA AG ′Gf
Aα A′α
Теперь мы можем определить линейную комбинацию мультимножеств следующим образом:
∞⊕(_) -гомоморфизмом из ∞⊕
0S в ∞⊕
1S будем называть функцию ∞∞ ⊕⊕ → 10: SSg такую, что
где s⋅1 – формальная сумма, соответствующая функции, принимающей значение 1 на элементе s и 0 – на всех
остальных.
Мы будем рассматривать ⊕S как множество с выделенной точкой – пустым мультимножеством, т.е.
функцией принимающей значение 0 на всех элементах S , которое в дальнейшем будем обозначать как 0.
Также будем обозначать ⊕∈ Sµ через iiIi sn∈⊕ , где ][}|{ µ=∈ Iisi и )( ii sn µ= , т.е. как сумму с ненулевыми
слагаемыми. Кроме того, если SS ⊂′ , то будем писать S ′⊕ вместо sSs ⋅∈⊕ 1 .
Если nXXs ××∈ K1 , то его проекция на компоненту iX будет обозначаться как iXs ↓ . Кроме того,
если }|{ JjsS j ∈= U , то iXS ↓ будет обозначать }|{ JjXs ij ∈↓ , а iXs
⊕
↓ будет обозначать )( ijJj Xs ↓∈⊕ .
Далее перейдем к определению собственно сетей Петри. Заметим, что использование в определении
множеств с выделенной точкой позволяет «моделировать» частичные функции с помощью всюду
определенных.
Определение 2.1. Сеть Петри – это структура ),)0,(:,( 10
NNNNN uSTN ⊕→= δδ , где NT – множество
переходов с выделенной точкой 0, NS – множество мест, 0
Nδ и 1
Nδ – морфизмы множеств с выделенной точкой
и ⊕∈ NN Su – начальная разметка. Кроме того, мы требуем, чтобы выполнялось 00)(0 =⇔= ttNδ .
Морфизм сетей Петри 0N и 1N – это пара функций ),( gf таких, что
1.
10
: NN TTf → – морфизм множеств с выделенной точкой,
2. ∞∞ ⊕⊕ →
10 NN Sg:S – ∞⊕(_) -гомоморфизм,
3. 00
NN gf δδ oo = и 11
NN gf δδ oo = , т.е. f и g сохраняют действие 0
Nδ и 1
Nδ ,
4. I
N
I
N uug
10
)( = ,
5. ][!],[
11
I
N
I
N uaub ∈∃∈∀ , такое, что )]([ agb∈ ,
)]([!))],(([ 11
01
tatfb NN δδ ∈∃∈∀ , такое, что )]([ agb∈ .
Определив композицию покомпонентно, получаем категорию сетей Петри PTNets .
Таким образом, сеть Петри представляется как граф, дуги которого – переходы, а вершины –
мультимножества мест, т.е. разметки.
Сеть Петри N – безопасная, тогда и только тогда, когда выполнено:
где ][NR – множество разметок N , достижимых из начальной. Для безопасных сетей мы будем использовать
следующие обозначения. Входное множество a будем обозначат, как )]}([|{ 1 taTta NN δ∈∈=• . Симметрично
определяется выходное множество: )]}([|{ 0 taTta NN δ∈∈=• . Очевидным образом эти понятия можно
расширить на множество мест. Безопасные сети определяют полную подкатегорию PTNetsSafe ⊂ .
Определение 2.2. Сеть-процесс – это безопасная сеть θ такая, что
1. ∅=⇔∈ •aua N ][ ,
2. 1|| , ≤∈∀ • aSa θ , где |_| обозначает мощность множества,
3. отношение p является иррефлексивным, где p – транзитивное замыкание отношения
кроме того, для всех θTt ∈ множество }|{ ttTt p′∈′ θ конечно,
4. бинарное отношение «конфликта» # определенное на θθ TS ∪ иррефлексивно, по определению,
где p – рефлексивное замыкание p . Сети-процессы образуют полную подкатегорию afecc SO ⊂ .
.)()( )()( ssnssnn
S
SsSs
SS
⋅⋅⋅⋅ ∑⊕=⊕⊕=⊕
∞⊕
∈
∈∈∞⊕
∈∞⊕
∈ µ
µµ
µ
µ
µ
µµµ
),1()()(
0
sgsg
Ss
⋅⋅=
∈
⊕ µµ
,][],[ и )1,0( )()]([, vvNvittTt i
N
i
NN =∈∀==∈∀ ⊕⊕ Rδδ
},,|),{(},|),{(1 atTtSsatatTtSsta •• ∈∈∈∪∈∈∈= θθθθp
,)]([)]([#,, 212
0
1
0
2121 ttttttTtt m ≠∧∅≠∩⇔∈∀ θθθ δδ
,#:,#,, 212121 ytxtttTttyxSTyx mm pp ∧∧∈∃⇔∪∈∀ θθθ
Введем следующие обозначения: пусть [n,m] обозначает интервал ω⊂},,{ mn K , [n] обозначает [1,n],
ik][ обозначает i-й блок длины k множества }0{\ω , т.е. ])1[(\][ kiik − .
Мы будем называть функцию ][][: mnf → блоковой тогда и только тогда, когда n=km и }{)]([ ikf i =
для всех mi ,,1 K= .
Заметим, что компонента g, действующая на местах, в морфизме сетей Петри 10:),( NNgf → может
рассматриваться как мультиотношение (с, возможно, бесконечными множественностями) между
0NS и
1NS ,
т.е. отношение g такое, что nbga тогда и только тогда, когда nbag =))(( . В случае сетей-процессов, g
является отношением, и обратное к нему отношение opg определяется так: bag op тогда и только тогда, когда
agb . Кроме того, в случае сетей-процессов, следующие сужения opg являются (всюду определенными)
функциями: ][][:
01
I
N
I
N
op uug →∅ и )]([))](([: 11
}{ 11
ttfg NN
op
t δδ → для каждого
0NTt ∈ . Эти функции будут
использованы в приведенном ниже определении специальных сетей-процессов, места которых сгруппированы
в семейства, что позволяет удобным образом строить развертку для любых (не только безопасных) сетей Петри.
Определение 2.3. Декорированная сеть-процесс θ – это сеть-процесс такая, что
1. θS имеет вид ][}{ a
Aa
na ×
∈ θ
U , где множество ][}{ ana × называется семейством a, мы будем
использовать обозначение Fa для семейства a, рассматриваемого как мультимножество,
2. yxnayxAa a
•• =×∈∀∈∀ ],[}{,,θ .
Морфизм декорированных сетей-процессов 10:),( θθ →gf – это морфизм сетей-процессов,
действующий с учетом семейств, т.е. для каждого θSa F ⊆][ верно:
1. F
i
Ii
F bag
a∈
⊕=)( для некоторого множества индексов aI ,
2.
ib
op
ia ing ooπ – блоковая функция, где
aπ – проекция ][}{ ana × на ][ an ,
ibin – биекция из ][ an в ][}{ ana × , и
][}{}{}{: abi
op
i nanbg
i
×→× является сужением opg на ][}{
ibi nb × .
Декорированные сети-процессы и их морфизмы образуют категорию DecOcc .
Пусть θ – декорированная сеть-процесс (согласно которой определяются отношения #, p , p ). Далее
введем отношение параллельности:
• для )#( ,, yxxyyxycoxSTyx ∨∨¬⇔∪∈ ppθθ ,
• для ) |},|{(|) ,,()(, ωθθθ ∈∈∃∈∧∈∀⇔∪⊆ xtXxTtycoxXyxXCoTTX p .
3. Временное расширение сетей Петри и их развертки
В данной части вводится ряд понятий, связанных с временными сетями Петри модели Мерлина [7] и ее
семантическими представлениями, а также дается теоретико-категорная характеризация построения семантик.
Пусть R – множество действительных неотрицательных чисел. Введем дополнительное обозначение:
},|],{[ ω∈⊂= babaInterv R – множество интервалов R с целочисленными границами.
Определение 3.1. Временной сетью Петри будем называть пару ),( χNTN = , где N – сеть Петри, а
IntervTN →:χ – функция временных интервалов. При этом будем обозначать ))(min( tχ – нижнюю границу
интервала, – как )(tεχ – самое раннее время срабатывания перехода, и ))(max( tχ как )(tλχ – самое позднее
время срабатывания перехода, т.е. )](),([)( ttt λε χχχ = . Морфизмы временных сетей Петри ),( 000 χNTN = и
),( 111 χNTN = – это морфизмы сетей Петри 10:),( NNgf → , удовлетворяющие следующему условию:
))(()( 100
tftTt N χχ ⊆∈∀ . Определенные выше временные сети Петри и их морфизмы образуют категорию
TPTNets .
Определение 3.2. Временная сеть-процесс – это пара ),( ϕθτθ = такая, что θ – сеть-процесс,
IntervT →θϕ : – функция временных интервалов и для любых переходов θTtt ∈′, выполнено условие:
)()()()( tttttt ′≤∧′≤⇒′ λλεε ϕϕϕϕp .
Аналогичным образом, определим временные декорированные временные сети-процессы.
Определение 3.3. Декорированная временная сеть-процесс – это временная сеть-процесс ),( ϕθτθ =
такая, что θ – декорированная сеть-процесс.
Далее будем рассматривать взаимосвязи между категориями TDecOcc и TPTNets .
Перед этим введем вспомогательное понятие. Глубина некоторого элемента множества θθ ST ∪ , где θ
– либо сеть-процесс, либо декорированная сеть-процесс, определяется по индукции:
• depth(b)=0, если ][ Iub θ∈ ,
• 1}|)(max{)( += tbbdepthtdepth p ,
• depth(b)=depth(t), если bt •=}{ .
Определение 3.4. Пусть ),( ϕθτθ = – временная декорированная сеть-процесс. По определению,
положим ),()( +++ = χθτθ τ , где сеть +θ определяется следующим образом. Пусть
),])[}{()0,(:,( 10 I
a
Aa
unaT θθθθ
θ
δδθ ⊕
∈
×→= U – декорированная сеть-процесс, +(_) – ∞⊕(_) -гомоморфизм из ∞⊕
θS
в ∞⊕
θA такой, что aja =+),( . Тогда определим сеть +θ следующим образом:
))(,)0,(:(_),((_) 10 +⊕+++ →= IuAT θθθθθ δδθ oo . Функция временных интервалов +χ определяется следующим
образом:
Пусть 10:),( τθτθ →gf – морфизм декорированных временных процессов. Тогда
++++ →= 10:)(_),(),( θθτ ingfgf oo , где ⊕⊕ →
00
: θθ SAin – ∞⊕(_) -гомоморфизм из ∞⊕
θS в ∞⊕
θA такой, что
)1,()( aain = .
Нетрудно показать, что определенный выше +
τ(_) является функтором.
Далее определим развертку временной сети Петри в декорированную временную сет-процесс.
Определение 3.5. Пусть ),( χNTN = – временная сеть Петри. Тогда )],[(][ ][TNNTN
τ
ϕτ UUU = . Здесь
][NU – развертка N [11], являющаяся обратным пределом (который существует, согласно теореме 1.10, [11])
последовательности (которая может рассматриваться как функтор из подходящей категории в категорию
TDecOcc ) декорированных сетей-процессов ),)0,(:,(][ 10)(
kkkkk
k uSTN ⊕→= δδU )( ω∈k , определенной
следующим образом. Для 0=k :
• })(|][)},{{(0 nbunbS I
N =×∅= U ,
• }0{0 =T ,
• 00 Su I ⊕= .
Для 0>k :
• )}()(|),{( 0
11 tSBTtBCoSBtBTT NNNkkk δ=↓∧∈∧∧⊆∪=
⊕
−− ,
• }){( ))((|][)}},{({ 0
1
001 nbTtSbTtnbtSS NNkkk =↓∧∈∧∈×∪= − δU ,
• BtBk ⊕=),(0δ и }{ )),)},,(({(),(1
kk SibtBtB ∈= ⊕δ ,
• II
k uu 0= .
Далее, ][TNτ
ϕU – функция временных интервалов, определенная следующим образом:
Нетрудно показать, что определенный таким образом [_]τU является функтором.
Теорема 3.6. Пара функторов [_])ττ U,((_)+ образует сопряжение.
Доказательство (набросок). Для доказательства теоремы построим для каждой временной сети Петри
),( χNTN = следующий сворачивающий морфизм (или свертку) TNTNgfTN →= +
ττεεε ])[(:),( U следующим
образом:
• ttBf =),(ε и 0)0( =εf ,
• iiiii yyxg ⊕=⊕ )),((ε .
Заметим, что он полностью совпадает с сверткой NNgfN →= +][:),( Uεεε из [11].
иначе. }], |)({max)(}, |)({max)([
0,)( если ,)(
),(
][][
][ {
tttttttt
tdeptht
tB
TNTN
TN pp ′′+′′+
=
= λλεε
ττ
τ ϕχϕχ
χ
ϕ
UU
U
иначе. }] |)({max)(}, |)({max)([
0,)( если ,)(
)( {
tttttttt
tdeptht
t
pp ′′−′′−
=
=+
λλεε ϕϕϕϕ
ϕ
χ
Рассмотрим декорированную временную сеть ),( ϕθτθ = и морфизм TNk →+
ττθ )(: в категории
TPTNets . Так как по определению, Nk →+θ: , то по теореме 1.15 [11] имеем: в категории DecOcc
существует единственный морфизм ][: Nh U→θ такой, что += hk N oε . Осталось показасть, что морфизм h
удовлетворяет условиям, накладываемым на морфизмы временных декорированных сетей-процессов, т.е.
действует с учетом временных интервалов и, следовательно, является морфизмом ][: TNh ττθ U→ . Для этого
рассмотрим следующую диаграмму.
Здесь равенство tt ′= следует из того, что += hk TN oε . По определению, имеем: )()()( ttt χχχ θ =′⊆+ и
)()(),(][ tttBTN ′==+ χχχ
τU . Следовательно, ),()( ][ tBt TN
++ ⊆
τ
χχ θ U и ++++ →= ττττ τθ ])[()(:)()( TNhh U – морфизм в
категории TPTNets и, как нетрудно показать, ][: TNh ττθ U→ – морфизм в категории TDecOcc . Таким
образом, мы показали, что для любого морфизма TNk →+
ττθ )(: в категории TPTNets в категории
TDecOcc существует единственный морфизм ][: TNh ττθ U→ , такой, что += τε )(hk TN o . Следовательно (по
теореме 2, [8]), пара функторов [_])ττ U,((_)+ образует сопряжение. Теорема доказана.
Чтобы связать категории TDecOcc и TOcc , определим «забывающий» функтор
TOccTDecOccF →:[_]τ , который «забывает» о семействах мест.
Определение 3.7. Пусть τθ – декорированная сеть-процесс, тогда ][τθτF – это сеть-процесс τθ . Пусть
10:),( τθτθ →gf – морфизм декорированных сетей-процессов, тогда ),()],[( gfgf =τF .
Для того чтобы определить функтор, действующий в обратную сторону, введем некоторые
дополнительные определения.
Пусть Σ – алфавит. Тогда бинарное отношение a на +Σ , языке непустых цепочек над Σ , определяется
следующим образом:
Тогда язык простых строк над Σ определяется следующим образом:
где НОД – наибольший общий делитель.
Рассмотрим некоторую декорированную сеть-процесс θ и переход θTt ∈ . Будем обозначать через }{tΣ
алфавит )]([ 1 tθδ . Аналогично, так как места входной разметки не принадлежат выходному множеству ни одного
перехода, то ∅Σ будет обозначать ][ Iuθ , кроме того, в дальнейшем мы будем обозначать Iuθ как )(1 ∅θδ .
Так как семейство Fb является ничем иным как упорядоченным подмножеством начальной разметки или
выходного множества перехода, то оно соответствует некоторой строке из +Σ x , где ][ Fbx •= , а именно строке
длины |][| Fb , у которой на i-м месте находится символ (b,i). Мы будем обозначать такую строку как Fb̂ .
Теперь определим функтор TDecOccTOccD →:[_]τ , который, как будет показано ниже, совместно с
[_]τF , составляет сопряжение.
Определение 3.8. Пусть ),( ϕθτθ = – временная сеть-процесс. По определению, )],[(][ ϕθτθτ DD = , где
][θD – «декорирование» θ [11], определенное следующим образом. Пусть θ – сеть-процесс из Occ . Тогда
декорированная сеть-процесс ),)0,(:,(][ ][][][
0
][
IuST θθθθθ δδθ DDDDD ⊕→= 1 cтроится по следующим правилам:
• )},}{(||][|}{{][ ∅=∨⊆=∧Σ∈×= xTtxsssS P
x θθ UD
• )]},([|),{( 0
][][ tsSis i θθθ δδ ∈∈= ⊕ DD
0
• },|{ }{
1
][
P
t
F ss Σ∈= ⊕θδ D
• }|{][
PFI ssu ∅Σ∈= ⊕θD .
.,,1,:111
11 kimqnq iiii
m
k
mn
k
n kk KKaK ==∈∃∧≠⇔ + ωσσσσσσ
},1),,НОД(|{\ 1121
21 >∧≠Σ=Σ +
+
kii
n
k
nnP nnk KK σσσσσ
NTt ∈′
θθ tT ∋
),(][ tBT N ∋U
TNε
NTt ∈
+h
k
Теорема 3.9. Пара функторов [_])[_], ττ FD( образует сопряжение.
Доказательство (наборосок). Определим для каждой временной сети-процесса ),( ϕθτθ = морфизм
][: τθτθη τττθ DF→ следующим образом:
• tt =)(τθη ,
• }|),{()( ][ asSisa i =∈⊕= θτθη D .
Заметим, что определенный выше морфизм совпадает с морфизмом ][: θθηθ FD→ из утверждения 2.6 [11].
Пусть ),( ϕθτθ = – временная сеть-процесс, ),( ϕθθτ ′′=′ – декорированная временная сеть-процесс и
][: θττθ τ ′→ Fk – морфизм в категории TOcc . Согласно определения морфизма имеем: ][: θθ ′→ Fk –
морфизм в категории Occ . Следовательно, по теореме 2.9 [11], имеем: в категории DecOcc существует
морфизм θθ ′→][:),( Dgf такой, что θηo)],[( gfk F= . Покажем, что (f, g) действует с учетом временных
интервалов, т.е. является морфизмом в категории TDecOcc . Необходимое условие следует из того факта, что
так как θηo)],[( gfk F= , то )())( tktf =F( , и, следовательно, для любого перехода θTt ∈ верно:
))(())(()( tftkt ϕϕϕ ′=′⊆ , то есть θττθτ ′→][:),( Dgf – морфизм в категории TDecOcc . Таким образом, для
всякого морфизма ][: θττθ τ ′→ Fk в категории TOcc , существует морфизм θττθτ ′→][:),( Dgf в категории
TDecOcc такой, что θτ ηo)],[( gfk F= , следовательно, по теореме 2 [8], пара функторов [_])[_], ττ FD(
образует сопряжение. Теорема доказана.
Литература
1. Alur R., Dill D. The theory of timed Automata. Lecture Notes In Computer Science 600, (1991) 45–73.
2. Aceto L., Murphi D. Timing and causality in process algebra. Acta Informatica. 33(4) (1996) 317–350.
3. Berthomieu B., Diaz M. Modelling and verification of time dependent systems using time Petri nets. IEEE
Transactions on Software Engineering. 17(3) (1991) 259–273.
4. Bourceux F. Handbook of Categorical Algebra. Cambridge: Cambridge University Press (1994)
5. Casley R.F., Crew R.F., Meseguer J., Pratt V.R. Temporal structures. Mathematical Structures in Computer
Science. 1(2) (1991) 79–213.
6. Degano P., De Nicola R., Montanari U. A distributed operational secamtic for CSS based on condition event
system. Acta Informatica. 26 (1988) 59–91.
7. Katoen J.-P. Quatitative and Qualitative Extensions of Event Structures. PhD Thesis, Twente University (1996).
8. MacLane S. Categories for the Working Mathematician. GTM, Springer-Verlag, 1971
9. Merlin P.M., Farber D.J. Recoverability of communication protocols – implications of theoretical study. IEEE
Transactions on Communications, 24(9) (1976) 1036-1043
10. Meseguer J., Montanari U., Sassone V. Process versus unfolding semantics for Place/Transition Petri nets.
Theoretical Computer Science 153, (1996) 171–210.
11. Meseguer J., Montanari U. On the Semantics of Petri Nets. Lecture Notes in Computer Science 630, (1992) 286–
301.
12. Schneider S., Davies J., Jackson D.M., Reed G.M., Reed J.M., Roscoe A.W. Timed CSP: theory and practice.
Lecture Notes in Computer Science 600 (1991) 640–675.
13. Winskel G. Event structures. Lecture Notes in Compiter Science 255, (1987) 325–392
|