Коалгебраическое исследование бисимуляционных паралельных процессов
The aim of this paper is to extend of coalgebra semantic and categorical methods to noninterleaving models, in particular, transition systems
 with independence and labelled event structure.
Збережено в:
| Дата: | 2004 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут програмних систем НАН України
2004
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/2318 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Коалгебраическое исследование бисимуляционных паралельных процессов/М.Ф. Антонцева // Проблеми програмування. — 2004. — N 2,3. — С. 47-51. — Бiбліогр.:5 назв. - рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859998626213789696 |
|---|---|
| author | Антонцева, М.Ф. |
| author_facet | Антонцева, М.Ф. |
| citation_txt | Коалгебраическое исследование бисимуляционных паралельных процессов/М.Ф. Антонцева // Проблеми програмування. — 2004. — N 2,3. — С. 47-51. — Бiбліогр.:5 назв. - рос. |
| collection | DSpace DC |
| description | The aim of this paper is to extend of coalgebra semantic and categorical methods to noninterleaving models, in particular, transition systems
with independence and labelled event structure.
|
| first_indexed | 2025-12-07T16:34:50Z |
| format | Article |
| fulltext |
1
КОАЛГЕБРАИЧЕСКОЕ ИССЛЕДОВАНИЕ БИСИМУЛЯЦИОННЫХ
ПАРАЛЛЕЛЬНЫХ ПРОЦЕССОВ
Антонцева Марина Федоровна
Институт Систем Информатики им. А.П.Ерщова СО РАН
630090 г. Новосибирск, проспект Лаврентьева 6
тел.: (3832) 34-36-52
факс: (3832) 32-34-94
e-mail: iis@iis.nsk.su
The aim of this paper is to extend of coalgebra semantic and categorical methods to noninterleaving models, in particular, transition systems
with independence and labelled event structure.
Введение
Теория категорий в последнее время стала активно использоваться в теории параллелизма для описания
и изучения параллельных систем и процессов. Использование методов теории категорий позволило исследовать
взаимосвязи между различными моделями [3]. Одним из наиболее широко применяемых понятий этой теории
является понятие открытого морфизма.
В теории параллельного программирования существует множество различных поведенческих
эквивалентностей, но самыми известными являются бисимуляционные эквивалентности. Две системы
называются бисимуляционно эквивалентными, если наблюдатель не может найти различий в их поведении. В
рамках теории категорий было предложено абстрактное понятие бисимуляции для различных параллельных
моделей, определенное через конструкцию открытых морфизмов. В дальнейшем этот подход стал
использоваться и для определения других видов эквивалентностей.
В [4] дан коалгебраический подход для описания поведенческой бисимуляции интерливинговых моделей
– систем переходов. Коалгебра является двойственной к алгебре. Двойственность алгебраической и
коалгебраической семантик показана в [5].
Цель моей работы – расширить эти два подхода (категориальный и
коалгебраический) на модели истинного параллелизма, представленные системами
переходов с независимостью и помеченными структурами событий.
1. Модели
1.1. Системы переходов
Определение 1.1.
1. Т-система – это структура ( )SAiS →,,, , где
S – множество состояний с начальным состоянием i,
A – множество меток,
SASS ××⊆→ – отношение перехода. Пишем ss S
a ′→ , если Ssas ∈→′),,( .
2. TI-система – это структура ( )SS IAiS ,,,, → , где ( )SSS IAiS ,,,, → – T-система и SI – иррефлексивное,
симметричное отношение, такое что
1) sssassas ′′=′�′′≈′ ),,(),,( ,
2) ,),,(),,(.),,(),,( ubsIsasusbsIsas SS ′′∃�′′′ ),,(),,( uasIsbs S ′′′′ ,
3) �′′ ),,(),,( ubsIsas S ),,(),,(. sbsIsass S ′′′′′∃ ,
4) ),,(),,(),,(),,(),,( wbwIsaswbwIuassas SS ′′�′′′≈′ ,
где ≈ – это наименьшее отношение эквивалентности, включающее отношение между переходами � , которое
определяется так:
).,,(),,(),,,(),,(),,,(),,(.),,(),,( uasIsbsubsIsassbsIsasbuassas SSS ′′′′′′′′′′∃⇔′′′ �
Отношение SI называется отношением независимости. Если ),,(),,( wbwIsas S ′′ , то говорят, что
переходы ss S
a ′→ и ww S
b ′→ независимы.
3. OTI-система – это TI-система ( )SS IAiS ,,,, → , которая является достижимой, ацикличной и такая, что
если usus S
b
S
a →′′→′ , и эти переходы не совпадают, то
).,,(),,(),,,(),,(),,,(),,(. ubsIsasuasIsbssasIsbsSs SSS ′′′′′′′′′′∈∃
Т.е. в OTI-системе любой квадрат независимости – невырожденный, другими словами, состоит из
четырех различных состояний.
2
Определение 1.2. Пусть S ( )SSSS IAiS ,,,, →= и T ( )TTTT IAiT ,,,, →= – две OTI-системы. Морфизм
f:S → T между ними – это пара ),( λσ=f , где TS AATS →→ :,: λσ , такие что выполнено:
1) TS ii =)(σ ;
2) если ss S
a ′→ и )(aλ определено, то )()( )( ss T
a ′ → σσ λ ;
если ss S
a ′→ и )(aλ не определено, то )()( ss ′= σσ ,
3) если uuIss S
b
SS
a ′→′→ и )(),( ba λλ определено,
то )()()()( )()( uuIss T
b
TT
a ′ →′ → σσσσ λλ .
OTI-системы вместе с морфизмами формируют категорию, которую обозначают . Пишем А для
обозначения категории ОTI-систем с множеством меток А.
1.2. Помеченные структуры событий
Определение 1.3. Помеченная структура событий – это структура ,,( ≤E #, )l , где
Е – множество событий,
AEl →: – помечающая функция (А – алфавит),
EE ×⊆≤ – отношение причинной зависимости,
# EE ×⊆ – отношение конфликта (иррефлексивное, симметричное отношение), которое удовлетворяет:
1) { }edEdEe ≤∈∈∀ |. – конечно (т.н. принцип «конечности причин»);
2) 1321 .,, eEeee ∈∀ # 3132 eeee #�≤ – (т.н. принцип «наследования конфликта»).
Два события Eee ∈2,1 – параллельны, пишут 21coee , если ( )∉#≤¬≤¬ },{),(),( 211221 eeeeee .
Определение 1.4. Пусть E = ,,( ≤E #, )l – помеченная структура событий. C – конфигурация, если
выполнено:
1) CdedCeEde ∈�∧∈∈∀ �., , ;\id=≤�
2) )(., eeEee ′#¬∈′∀ .
Множество конфигураций структуры событий обозначается C(E).
Определение 1.5. Пусть E = ,,( ≤E #, )l , E` = ),,,( lE ′#′≤′′ – две помеченные структуры событий над
алфавитами A и A′ соответственно. Морфизм между ними – это EEf ′→= :),( λη , где –
AAEE ′→′→ :,: λη частичные функции такие, что выполнено:
1) ;ll �� λη =′
2) если c – конфигурация E, то cη – конфигурация E ′ , и если cee ∈∀ 21 , и их образы определены и
)()( 21 ee ηη = , то 21 ee = .
– категория помеченных структур событий с морфизмами.
2. Открытые морфизмы
Определим категорию мультимножеств A относительно множества меток A как полную
подкатегорию A (категория помеченных структур событий с морфизмами над множеством меток А), чьи
объекты – это конечные мультимножества, т.е. частично упорядоченные помеченные события.
Тогда вычисление в структуре событий E можно представить как морфизм в A: ∈→ PEPp ,: A .
Так как структуры событий (и также мультимножества) вкладываются в TI-системы [2,3], то вычисление
в T∈ A представляется морфизмом TPp →: в A, где P – образ объекта A под действием вложения.
Пусть – категория моделей, ➥ – подкатегория . Oпределим вычисление в ∈X как
морфизм XPp →: в , где P∈ . Тогда любой морфизм в YXf →: переводит такое вычисление p в X в
вычисление YPpf →:� в Y.
Определение 2.1. Пусть ∈QP, , ∈YX , Пусть YXf →: – морфизм в , QPm →: – морфизм в
, XPp →: – вычисление в Х, YQq →: – вычисление в Y.
Тогда YXf →: называют -открытым морфизмом, когда f удовлетворяет условию:
если pfmq �� = , то существует морфизм XQp →′ : , такой что pmp =′� и qpf =′� .
Определение 2.2. Пусть – категория моделей, ➥ – подкатегория . Пусть ∈21, XX .
Говорят, что 21 , XX – -бисимулятивны с бисимуляцией X, если существует «хорда» -открытых морфизмов
2211 :,: XXfXXf →→ .
Предложение 2.3 [2]. A-открытые морфизмы в A – это морфизмы 21:)1,( TTA →σ , где A1 –
тождественное отображение на множестве А, такие что:
1) если ts T
a ′→ 2)(σ , то ssSs T
a ′→∈′∃ 1. и ts ′=′)(σ ;
3
2) если ssss T
b
T
a ′′→′→ 11 , и )()()()( 222 ssIss T
b
TT
a ′′→′′→ σσσσ , то ssIss T
b
TT
a ′′→′′→ 111 .
3. F– коалгебры
Определение 3.1. Пусть SetSetF →: – функтор. Тогда F-коалгебра – это пара ( )SS α, , состоящая из
множества S и функтора ( )SFSS →:α .
Определение 3.2. Пусть ( )SS α, и ( )TT α, – две F-коалгебры. Гомоморфизм F-коалгебр (или F-
гомоморфизм) – это функция TSf →: , удовлетворяющая равенству ( ) ffF TS �� αα = .
Композиция двух F-гомоморфизмов тоже F-гомоморфизм, и тождественное отображение F-коалгебр –
F-гомоморфизм. Следовательно, набор всех F-коалгебр с F-гомоморфизмами образуют категорию, которая
обозначается F.
Определение 3.3. Пусть ( )SS α, и ( )TT α, – две F-коалгебры. F-бисимуляция между ними – это
отношение TSR ×⊆ , такое что существует функтор )(: RFRR →α (т.е. ),( RR α F-коалгебра),
удовлетворяющий условию: проекции SR →:1π и TR →:2π являются F-гомоморфизмами.
Теорема 3.4 [4]. Пусть ( )SS α, и ( )TT α, – две F-коалгебры. Функция TSf →: является F-
гомоморфизмом тогда и только тогда, когда ее граф G(f) – это F-бисимуляция между данными F-
коалгебрами.
4. Связь коалгебр и моделей
4.1. ОTI-системы и IF –коалгебры
Рассмотрим помеченную TI-систему ( )SSS IAiS ,,,, → .
Определим →SI
S :α P ))(( SASSA ×××× следующим образом: { }ssIsasSs S
a
as ′→>′<∈∀ |,,� ,
где { }uuIssubuI S
b
SS
a
as ′→′→>′<= |,, .
Построим SetXSXXF I
S
I ∈∀∩= )()( α . Тогда SetSetF I →: – функтор (это легко показать), и
),( I
SS α – коалгебра. Таким образом, любая TI-система ( )SSS IAiS ,,,, → соответствует IF -коалгебре. И
наоборот, любая IF -коалгебра соответствует TI-системе ( )SSS IAiS ,,,, → :
).(,,х независимы ним с переходов, нет и
);(,,,,
ssass
subusauuIss
I
SS
a
I
SS
b
SS
a
α
α
>∈∅′<⇔′→•
>∈′′<⇔′→′→•
Т. е. класс TI-систем совпадает с классом IF -коалгебр. Далее будем рассматривать подкласс TI-систем –
OTI-системы.
Утверждение 4.1. Пусть ( )SSS IAiS ,,,, → и ( )STT IAiT ,,,, → – две OTI-системы, ),( I
SS α и ),( I
ST α –
соответствующие им IF -коалгебры. Тогда IF -гомоморфизм между ними – это морфизм TSf A →:)1,( в
A, который удовлетворяет:
1. ;)(.,)( tsfиsssтоtsfесли S
a
T
a ′=′′→′∃′→
2.
.
),()()()(,,
uuIssто
ufufIsfsfuussесли
S
b
SS
a
T
b
TT
a
S
b
S
a
′→′→
′→′→′→′→
Доказательство.
Пусть TSf →: – IF -гомоморфизм между S и T, т.е. удовлетворяет равенству ( ) ffF I
TS
II
�� αα = .
Надо доказать, что для f выполняется:
1) если ss S
a ′ → , то )()( sfsf T
a ′→ ;
2) если uuIss S
b
SS
a ′→′→ , то )()()()( ufufIsfsf T
b
TT
a ′→′→ ;
3) если tsf T
a ′→)( , то ssSs S
a ′→∈′∃ . и tsf ′=′)( ;
4) если ss S
a ′→ , uu S
b ′→ и )()()()( ufufIsfsf T
b
TT
a ′→′→ , то uuIss S
b
SS
a ′→′→ .
Пусть ss S
a ′→ , и нет переходов, с ним независимых. Это равносильно тому, что )(,, ssa I
Sα>∈∅′< .
Тогда >∅′<=>∅′< ),(,,, sfasaF I по построению IF . Так как ( ) SssfsfF I
T
I
S
I ∈∀= )()( �� αα , то
))((),(, sfsfa I
Tα>∈∅′< , что равносильно )()( sfsf T
a ′→ .
4
Пусть uuIss S
b
SS
a ′→′→ . Тогда )(,,,, subusa I
Sα>∈′′< и )()()(,),(),(, sfFufbufsfa I
S
I α�>∈′′< .
Так как f – IF -гомоморфизм, то ))(()(,),(),(, sfufbufsfa I
Tα>∈′′< и, следовательно,
)()()()( ufufIsfsf T
b
TT
a ′→′→ .
Пусть tsf T
a ′→)( , т.е. ))((,, sfta I
Tα>∈∅′< . Так как ( ) SssfsfF I
T
I
S
I ∈∀= )()( �� αα , то
)()(,, sfFta I
S
I α�>∈∅′< . Отсюда следует, что существует Ss ∈ , такое что ss S
a ′→ и
>∅′>=<∅′<>=∅′< ),(,,,)(,, sfasafFta I . Поэтому )(sft ′= .
Пусть ss S
a ′→ , uu S
b ′→ и )()()()( ufufIsfsf T
b
TT
a ′→′→ . Т. е.
))(()(,),(),(, sfufbufsfa I
Tα>∈′′< . Так как ( ) SssfsfF I
T
I
S
I ∈∀= )()( �� αα , то
)()()(,),(),(, sfFufbufsfa I
S
I α�>∈′′< , т.е. uuIss S
b
SS
a ′→′→ .
Таким образом, мы показали, что если TSf →: – IF -гомоморфизм между S и T, то он является
морфизмом, который удовлетворяет пунктам 1 – 2 утверждения.
Обратное очевидно.
Утверждение 4.1 доказано.
Теорема 4.2. Пусть ( )SSS IAiS ,,,, → и ( )STT IAiT ,,,, → – две OTI-системы, ),( I
SS α и ),( I
ST α –
соответствующие им IF -коалгебры. Тогда IF -бисимуляция между ними – это отношение TSR ×⊆ такое,
что Rts >∈<∀ , выполнено:
1) ;,., RtsиttTtтоssеслиSs T
a
S
a >∈′′<′→∈′∃′→∈′∀
2) ;,., RtsиssSsтоttеслиTt S
a
T
a >∈′′<′→∈′∃′→∈′∀
3)
;,,,,,
.,,,,,
Rwuwutsи
wwIttTwwtтоuuIssеслиSuus T
b
TT
a
S
b
SS
a
>∈′′<><>′′<
′→′→∈′′∃′→′→∈′′∀
4.
;,,,,,
.,,,,,
Rwuwutsи
uuIssSuusтоwwIttеслиTwwt S
b
SS
a
T
b
TT
a
>∈′′<><>′′<
′→′→∈′∃′→′→∈′′∀
Доказательство.
Пусть TSR ×⊆ – IF -бисимуляция между ( )SSS IAiS ,,,, → и ( )STT IAiT ,,,, → . Тогда по определению
3.3 существует функтор )(: RFRI
R →α такой, что ),( I
RR α – IF -коалгебра. Тогда I
Rα индуцирует отношение
перехода RARR ××⊆→ .
Пусть Rts >∈< , , ss S
a ′→ и sts >=< ,1π . Из этого следует, что sts S
a ′→>< ,1π , и так как 1π –
IF -гомоморфизм, то по определению 3.3 существует Rts >∈′′′< , такое, что >′′′<→>< tsts R
a ,, и
sts ′>=′′′< ,1π . Следовательно, Rts >∈′′< , . Так как 2π – IF -гомоморфизм, то tt T
a ′→ .
Таким образом мы доказали, что для любого
;,и.то,если, RtsttTtssSs T
a
S
a >∈′′<′→∈′∃′→∈′ . Доказательство 2–4 – аналогично.
Т. е. мы доказали, что если отношение TSR ×⊆ – IF -бисимуляция, то R удовлетворяет 1–4.
Обратно: пусть TSR ×⊆ удовлетворяет 1–4.
Определим )(: RFRI
R →α для Rts >∈< , следующим образом:
{ }
.
,,,,,
,|,,,,где
,,,|,,,,
,,
,
��
�
�
�
��
�
�
�
>∈′′<><>′′<
′→′→′→′→>>′′<><<=
>∈′′<′→′→>>′′<<>=<
><
><
Rwuwutsи
wwIttuuIsswubwuI
RtsиttssItsats
T
b
TT
a
S
b
SS
a
tsa
T
a
S
a
tsa
I
Rα
Тогда легко показать, что ),( I
RR α – IF -коалгебра и проекции из R в S и в T – это IF -гомоморфизмы.
Следовательно, отношение TSR ×⊆ – IF -бисимуляция между ( )SSS IAiS ,,,, → и ( )STT IAiT ,,,, → .
Теорема 4.2 доказана.
Теорема 4.3. Для OTI-систем над алфавитом А A–открытые морфизмы совпадают с IF -
гомоморфизмами соответствующих им IF -коалгебр.
Доказательство.
Следствие утверждения 4.1 и предложения 2.3.
5
Теорема 4.4. Для OTI-систем над алфавитом А A–бисимуляция совпадает с IF -бисимуляцией
соответствующих им IF -коалгебр.
Доказательство.
Пусть ( )SSS IAiS ,,,, → и ( )STT IAiT ,,,, → – две OTI-системы, ),( I
SS α и ),( I
ST α – соответствующие им
IF -коалгебры. Пусть TSR ×⊆ – IF -бисимуляция между ними. Так как по теореме 4.3 IF -гомоморфизмы
совпадают с A–открытыми морфизмами, то по определению 2.2 R – A–бисимуляция между
( )SSS IAiS ,,,, → и ( )STT IAiT ,,,, → .
Обратно: пусть R – A–бисимуляция между ( )SSS IAiS ,,,, → и ( )STT IAiT ,,,, → . По определению 2.2
существуют A–открытые морфизмы TRfSRf →→ :,: 21 , которые по теореме 4.3 являются IF -
гомоморфизмами. В качестве 1f и 2f возьмем проекции из R в S и в T . Строим )(: RFR II
R →α , как в
доказательстве теоремы 4.2. Тогда ),( I
RR α – IF -коалгебра и проекции из R в S и в T – это IF -
гомоморфизмы. Т. е. отношение TSR ×⊆ – IF -бисимуляция между ),( I
SS α и ),( I
ST α .
Теорема 4.4 доказана.
Теорема 4.5. Пусть ( )SSS IAiS ,,,, → и ( )STT IAiT ,,,, → – две OTI-системы. Функция TSf →:
является A–открытым морфизмом тогда и только тогда, когда ее граф )( fG – это IF -бисимуляция
соответствующих им IF -коалгебр.
Доказательство.
Следствие теоремы 3.4, теоремы 4.3 и теоремы 4.4
4.2. Помеченные структуры событий и коалгебры
Рассмотрим помеченную структуру событий ,,( ≤E #, )l . Определим ее «развертку» )(. Eotsiles как TI-
систему ),,,,()(. SSS IAiSEotsiles →= [3], где
S – множество конечных конфигураций структуры событий, Si =∅;
A=l(E);
).\()\(
;,)(},{\
cccoccccIcc
Eeaelecccc
S
b
SS
a
S
a
′′⇔′→′→
∈=′=⇔′→
Утверждение 4. 6 [3]. )(. Eotsiles – OTI-система.
Следующая теорема является следствием теоремы 4.4.
Теорема 4.7. Две помеченные структуры событий – A–бисимулятивны тогда и только тогда, когда
IF –коалгебры, соответствующие их «разверткам» в OTI–системы, – IF -бисимулятивны.
Заключение
Статья посвящена исследованию распределенных систем, таких как системы переходов с
независимостью и помеченные структуры событий. Для исследования применялись два подхода, которые стали
активно использоваться в теории параллелизма сравнительно недавно для спецификации и верификации
параллельных процессов. Это коалгебраический и категориальный подходы. В ходе работы стало ясно, что
некоторые определенные свойства интерливинговых моделей можно распространить на модели с “истинным”
параллелизмом, такие как OTI-системы. Однако для TI-систем эти свойства не выполняются.
В дальнейшем планируется, используя коалгебраические методы, изучить взаимосвязи между
различными временными сетевыми моделями, а также исследовать новые поведенческие эквивалентности,
учитывая также временные аспекты поведения систем.
Список литературы.
1. И.Б.Вирбицкайте. Семантические модели в теории параллелизма. Новосибирск: ИСИ СОРАН, 2000. – 190с.;
2. Andre Joyal, Mogens Nilsen and Glynn Winskel. Bisimulation From Open Maps. Information And Computation 127, pp. 164-185, 1996;
3. Mogens Nilsen, Vladimiro Sassone and Glinn Winskel. Relationships Between Models of Concurrency. Theoretical Computer Science, 803,
pp. 425-476, 1994;
4. J.J.Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249, pp. 3-80, 2000;
5. J.J.Rutten, D.Turi. Initial Algebra and Final Coalgebra Semantics for Concurrency. EATS №62, pp. 530-559.
|
| id | nasplib_isofts_kiev_ua-123456789-2318 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Russian |
| last_indexed | 2025-12-07T16:34:50Z |
| publishDate | 2004 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Антонцева, М.Ф. 2008-09-17T13:58:23Z 2008-09-17T13:58:23Z 2004 Коалгебраическое исследование бисимуляционных паралельных процессов/М.Ф. Антонцева // Проблеми програмування. — 2004. — N 2,3. — С. 47-51. — Бiбліогр.:5 назв. - рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2318 681.3 The aim of this paper is to extend of coalgebra semantic and categorical methods to noninterleaving models, in particular, transition systems
 with independence and labelled event structure. ru Інститут програмних систем НАН України Теоретические и методологические основы программирования Коалгебраическое исследование бисимуляционных паралельных процессов Article published earlier |
| spellingShingle | Коалгебраическое исследование бисимуляционных паралельных процессов Антонцева, М.Ф. Теоретические и методологические основы программирования |
| title | Коалгебраическое исследование бисимуляционных паралельных процессов |
| title_full | Коалгебраическое исследование бисимуляционных паралельных процессов |
| title_fullStr | Коалгебраическое исследование бисимуляционных паралельных процессов |
| title_full_unstemmed | Коалгебраическое исследование бисимуляционных паралельных процессов |
| title_short | Коалгебраическое исследование бисимуляционных паралельных процессов |
| title_sort | коалгебраическое исследование бисимуляционных паралельных процессов |
| topic | Теоретические и методологические основы программирования |
| topic_facet | Теоретические и методологические основы программирования |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/2318 |
| work_keys_str_mv | AT antoncevamf koalgebraičeskoeissledovaniebisimulâcionnyhparalelʹnyhprocessov |