Об одной геометрической модели временных параллельных процессов
The intention of the paper is to study geometric properties of timed concurrent processes. First, we introduce a notion of timed higher
 dimentional transition sistems and then we provide a category-theoretic characterization of bisimulation equivalence in the context of the
 model u...
Збережено в:
| Дата: | 2004 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут програмних систем НАН України
2004
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/2322 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Об одной геометрической модели временных параллельных процессов / Е.С.Ошевская // Проблеми програмування. — 2004. — N 2,3. — С. 23-29. — Бiбліогр.:10 назв. - рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860139724984811520 |
|---|---|
| author | Ошевская, Е.С, |
| author_facet | Ошевская, Е.С, |
| citation_txt | Об одной геометрической модели временных параллельных процессов / Е.С.Ошевская // Проблеми програмування. — 2004. — N 2,3. — С. 23-29. — Бiбліогр.:10 назв. - рос. |
| collection | DSpace DC |
| description | The intention of the paper is to study geometric properties of timed concurrent processes. First, we introduce a notion of timed higher
dimentional transition sistems and then we provide a category-theoretic characterization of bisimulation equivalence in the context of the
model under consideration.
|
| first_indexed | 2025-12-07T17:48:53Z |
| format | Article |
| fulltext |
Об одной геометрической модели временных параллельных процессов*
Ошевская Елена Сергеевна
Институт математики им С.Л. Соболева СО РАН, пр. Академика Коптюга, 4, г. Новосибирск, 630090,
Россия. Тел.: 33-34-96, факс: 33-25-98. E-mail: eso@iis.nsk.su
The intention of the paper is to study geometric properties of timed concurrent processes. First, we introduce a notion of timed higher
dimentional transition sistems and then we provide a category-theoretic characterization of bisimulation equivalence in the context of the
model under consideration.
Введение
Последние годы активно разрабатываются формальные методы спецификации, анализа и моделирования
параллельных/распределенных систем, имеющих сложную структурную и функциональную организацию. К
таким системам относятся коммуникационные протоколы, системы управления производством,
распределенные операционные системы и т.д. Разработка корректных параллельных/распределенных систем –
нетривиальная задача, требующая для своего успешного решения проведения комплексных фундаментальных
исследований, основанных на различных формальных методах и средствах.
Исследования последнего десятилетия показали, что применение теоретико-категорных методов
позволяет разрабатывать, унифицировать и классифицировать различные параллельные модели [10]. Кроме
того, в рамках теории категорий были предложены абстрактные определения эквивалентностей для различных
параллельных моделей [8]. Оказалось, что эквивалентности, определенные на категориях интерливинговых
моделей, согласуются с интерливинговой бисимуляцией Милнера, тогда как эквивалентности на категориях
моделей с «истинным параллелизмом» требуют более сильной эквивалентности – усиленного варианта
сохраняющей историю бисимуляци Трахтенброта. Альтернативная характеризация временной бисимуляции
для временной интерливинговой модели – временных систем переходов – с использованием теоретоко-
категорных методов была предложена Хунэм и Нильсеном [6].
С другой стороны, в начале 90-х годов прошлого столетия было начато исследование геометрических
свойств параллельных процессов посредством методов комбинаторной алгебраической топологии,
гомологической алгебры, алгебраической геометрии и т.д. В работах сначала Пратта [8], фан Глабика [2], а
затем Губо и Йенсена [3] была предложена и исследована геометрическая модель многомерных автоматов
(Higher Dimensional Automata). Многомерные автоматы – обобщение недетерминированных автоматов для
моделирования семантики «истинного параллелизма». Параллельное выполнение двух событий в
недетерминированных автоматах распознается геометрически как квадрат. В случае параллельного выполнения
трех и более событий в автоматах появляются n-мерные кубы (n=3,4..). Это и привело к понятию многомерных
автоматов. В вышеуказанных работах были изучены некоторые взаимосвязи между различными классами
многомерных автоматов и классическими параллельными моделями, а также теоретико-категорные свойства
этих геометрических моделей. Далее для разработки геометрических моделей параллельных процессов стали
использовать структуры и методы алгебраической топологии (например, цепные бикомплексы (chain
bicomplexes)) [3]. Позже Губо ввел временное расширение многомерных автоматов [5]. Кроме того, в 1996 году
Сассоне и Каттани [9] была предложена модель многомерных систем переходов, которая встраивается в модель
многомерных автоматов, сохраняя и отображая соответствующие понятия гомотопии и бисимуляции. Такое
встраивание является эквивалентностью категорий для некоторого подкласса многомерных автоматных
моделей. При этом было продемонстрировано, что при переходе от многомерных автоматов к многомерным
системам переходов нет никаких потерь в выразительной мощности, и последняя модель адекватно
представляет параллельные процессы.
В данной статье с целью более адекватного анализа поведенческих свойств параллельных систем на
основе методов теории категорий и геометрических структур строится временное расширение модели
многомерных систем переходов и изучаются гомотопические и теоретико-категорные свойства введенной
модели.
Статья состоит из трех частей. В первой части вводится геометрическая модель временных многомерных
систем переходов и строится соответствующая категория. Во второй части с помощью понятия гомотопии
определяется бисимуляционная эквивалентность. В третьей части дается ее альтернативная характеризация в
терминах открытых морфизмов. В заключении перечисляются результаты, полученные в рамках данной
работы, и приводятся некоторые замечания по дальнейшей исследованиям.
* Работа частично поддержана Российским фондом фундаментальных исследований (грант № 04-01-
00789).
1. Временные многомерные системы переходов
Построенная в 1996 году Сассоне и Каттани [9] модель многомерных систем переходов носит теоретико-
множественный характер. Один из недостатков такого подхода – отсутствие наглядности. В 1991 году Пратт
предложил изображать состояния точками, действия – отрезками, а одновременное исполнение n действий – n-
мерными (закрашенными) кубами (n=2,3…). Использование этой идеи сделало построение и исследование
моделей параллельных систем и процессов естественным и интуитивно понятным. К примеру, исполнение
многопроцессорной системой какой-либо последовательности действий теперь можно было изобразить просто
кривой (траекторией). На таком геометрическом представлении и основанно дальнейшее изложение.
Пусть },,...,1,10){(: 1
n nit,t,tQ i
n
n =≤≤∈…= R };{:Q 00 = и пусть nQint обозначает внутренность
множества nQ , причем }.{:Q 0int 0 =
Определим функцию ,n1-n QQ →:k
iδ 0,1,k n},{1,...,i N,n =∈∈ следующим образом
).,,()( 11111 −−− ……=… niin t,k,t,t,t,t,tk
iδ
Пусть Ν∈n – фиксированное.
Определение 1.1. Пусть X – топологическое пространство. Система непрерывных функций
,...,N}{A,nα
n
α{xF 0∈∈}= ( A – счетное) называется кубической, если ,...,N}{nAα 0, ∈∀∈∀ XQx nn
α →: индуцирует
гомеоморфизм nQint на )(int nn
α Qx , и выполняется следующее условие:
если Fxn ∈ , то Fx ∈k
iδo при всех 0,1.k n},{1,...,i =∈
Определим }.)({: nn QxdomFxF =∈=
Введем понятие временной многомерной системы переходов.
Определение 1.2. Тройка ),,( 0iLX называется временной многомерной системой переходов (обозн.
THDTS), если X – хаусдорфово топологическое пространство, L – множество меток, i0 --- начальное состояние,
и выполнены условия:
• для X задана кубическая система функций F такая, что ;)(int
},...,0{,
U
NnFx
n
n
QxX
∈∈
=
• задана функция LFl →1: такая, что
2Fx ∈∀ ,2,1))),((()))((( 11 == iQxlQxl 1
i
0
i δδ
,1, >∈∀ nFx n ,...,n},iQδδxyy{l:xl
)(n
ii 11
1
00 ==⊕=
−
))(()()(
43421
oKo , где ''⊕ обозначает
объединение мультимножеств;
• ,...,N}{n 1∈∀ выполняется следующее условие: если nFxx ∈21 , такие,
что )),(())(()),(())(( 0000 2121 43421
oKo
43421
oKo
43421
oKo
43421
oKo
nnnn
xxxx 1
1
1
1
1
1
1
1
0
1
0
1
0
1
0
1 δδδδδδδδ ==
),()( 21 xlxl = то 21 xx = ;
• X снабжено семейством норм
u
⋅ на касательном пространстве
( ),(int n
uu QxTXT = где nFx ∈ такая, что ))(int nQxu ∈ ) таким, что функция
u
uuuP && =),( непрерывна по u и является нормой.
Интуитивно временную многомерную систему переходов можно представить себе как хаусдорфово
топологическое пространство X , состоящее из соединенных между собой деформированных n-мерных кубов,
причем n=1,.,N. Кубы изогнуты так, что существует покрытие пространства картами XQx nn
α →: , область
значений каждой из которых – соответствующий деформированный n-мерный куб. На касательном
пространстве к X задано семейство непрерывных норм.
Определим понятие морфизма между временными многомерными системами переходов.
Определение 1.3. Пусть ),,(),,,( 00 YX
iLYiLX YX – THDTS, а YX FF , – их кубические системы
соответственно, ,: 1
XXX LFl → ,: 1
YYY LFl → . Тогда отображение α,f (где YX LL →:α – частично
определенное отображение, YXf →: – всюду определенное отображение) – морфизм, если
1. ;)( 00 YX
iif =
2. ,n
XFx ∈∀ },,,1{ Nn K∈
• если nxlX =))((α ,то n
YFy ∈∃ такая, что диаграмма
nQ X
Y
f
x
y
коммутативна, а ))(()( xlyl XY α= ; кроме того, верно, что ))(()))((( 11 −− = nk
i
nk
i QyQxf δδ , для всех
ni K,1= , 1,0=k ,
• если nqxlX <=))((α , то )))((()( qn
jj Qxfxf
q
−= 00
1
δδ oLo , где qjj ,,1 K такие, что
))(())(( 00
1 qjjXX xlxl δδαα oLoo= ;
3. 1≤fdu , Xu ∈ .
Из этого определения следует, что idxfy =− oo1 , а значит, ∞∈Cf .
Таким образом, мы получаем категорию THDTS, чьи объекты даются определением 1.2, а морфизмы –
определением 1.3.
Определение 1.4. Путем в THDTS ),,( 0iLX называется непрерывная функция X→]1,0[:γ такая, что
1. )( 1+=∃ kkk ,aaI , mk ,,0 K= , такие, что nn
k Fx ∈∃ , },,,1{ Nn K∈ такие, что )(int nn
kkI Qx:Iγ
k
→ ,
причем ,δδxaγ
n
n
kk ))(()( 000
43421 oLo= ;δδxaγ
n
n
kk ))(()( 011
1 43421 oLo=+
2.
kIγ – дифференцируемая функция;
3.
kIi
n
k γx o)( – неубывающая функция для всех n,i K1= , но каково бы ни было открытое
множество )(int nn
k QxU ⊂ найдется такое },1{ n,j K∈ , что constx j
n
k ≠)( на )( kIU γI .
Пробегом называется путь, начинающийся в начальном состоянии 0i .
Утверждение 1.5. Морфизмы категории THDTS сохраняют гомотопность путей.
Доказательство этого утверждения очевидно, ведь по определению морфизма при его действии не могут
появляться новые "дырки". А значит, если была гомотопия между путями, то она сохранится.
Определение 1.6. Длиной пути γ называется
∫=
1
0
dt.t
dt
dγ
γlength
γ(t)
)()(
Пусть (u,v)Π обозначает множество всех путей из точки u в точку v в X .
Определение 1.7. Минимальное время между точками u и v в X есть
).(inf),( γγ lengthvut (u,v)
X
i Π∈=
Максимальное время между точками u и v в X есть
).(sup),( γγ lengthvut (u,v)
X
s Π∈=
2. Бисимуляционная эквивалентность
Для T – THDTS полагаем, что TF – ее кубическая система, Ti – начальное состояние. Определим
})({: 00
TT FsQsS ∈= – множество состояний. Определим функции TT SFeb →:, следующим образом: если
n
TFx ∈ , то )),(()( 0Qxxb
n
43421
oKo 0
1
0
1 δδ= )).(()( 0Qxxe
n
43421
oKo 1
1
1
1 δδ=
С каждым путем γ мы ассоциируем натуральное число )(γmm = – число интервалов разбиения
)},({ 1+= kkk aaI из определения 1.4 пути, и сам набор точек .}{ },,0{ mkka K∈ Обозначим ),[ 1 ii aai −
= γγ при всех
1,1 −= m,i K и ],[ 1 mm aam −
= γγ . Тогда путь γ можно представить в виде mγγγ L1= , т.е. γ – это результат
последовательной композиции путей mγγγ ,,1 K= . Причем полагаем, что ),(:)( n
ii xll =γ где n
ix – из
определения 1.4 пути.
Определение 2.1. Пусть 21,TT – THDTS, а
21 TT SSR ×⊆ – отношение на их множествах состояний. Пути
mγγγ L1= , mγγγ ~~~
1L= в ,1T 2T соответственно называются R-соотносимыми, если )(~)( ii aRa γγ и
)~(:)( ii ll γγ = при всех },0{ m,i K∈ .
Определение 2.2. Пути γ и γ~ R-бисимуляционны (обозначается γγ ~
R↔ ), если
• пути γ и γ~ R-соотносимы;
•
− для любого пути β в 1T такого, что γβ ~ , существует γβ ~~
~
в 2T такой, что β и β~
R-соотносимы,
− для любого пути β~ в 2T такого, что γβ ~~
~
, существует γβ ~ в 1T такой, что β и β~
R-соотносимы;
• длины путей γ и γ~ совпадают.
(где ‘~’ обозначает отношение гомотопности в обычном смысле).
Определение 2.3. Бисимуляция между THDTS 1T и 2T – это отношение
21 TT SSR ×⊆ такое, что если γ
и γ~ – пробеги в 1T и 2T соответственно – R-бисимуляционны, sam =)(γ , sam
~)(~ =γ , то
• для любого пути 1ββ = )1)(( =βm такого, что sa =)( 0β , ,)(
1
µβ =Tl существует путь 1
~~ ββ =
( sa ~)(
~
0 =β , µβ =)
~
(
2Tl ) такой, что γβ и βγ ~~ R-бисимуляционны.
• для любого пути 1
~~ ββ = )1)
~
(( =βm такого, что sa ~)(
~
0 =β , µβ =)
~
(
2Tl , существует путь 1ββ =
( sa =)( 0β , ,)(
1
µβ =Tl ) такой, что γβ и βγ ~~ R-бисимуляционны.
THDTS 1T и 2T бисимуляционны ( 21 ~ TT R ), если между ними существует бисимуляция R такая, что
21 TT Rii .
3.Теоретико-категорная характеризация бисимуляционной эквивалентности
Определение 3.1. Наблюдение – это ацикличная THDTS ),,( iLP следующей формы
),()()()( 11
2
1
1
n
k QvQuQuQu K
где 1
21 ,,, Fuuu k ∈K , nFv ∈ , и кроме того, iub =)( 1 , )()( 1+= jj ubue , }1,1{ −∈ k,j K , ).()( vbue k =
Обозначим через Obs подкатегорию наблюдений категории THDTS.Подкатегория Obs является полной.
Чтобы определить понятие Obs-открытости, нужно наделить THDTS следующей структурой: обозначим
через LTHDTS подкатегорию всех тех THDTS с множеством меток L, морфизмы между которыми имеют
тождественную (там, где она определена) компоненту α (определение 1.3). Такие морфизмы будем называть
стрелками. Таким образом, далее говоря об Obs-открытости, мы предполагаем, что рассматриваемые объекты
принадлежат одной подкатегории LTHDTS .
Определение 3.2. Пусть 1T и 2T – THDTS. Стрелка 21 Tφ:T → называется Obs-открытой, если для
любых P, Q из Obs и для любых стрелок p,q,m таких, как на коммутативной диаграмме ниже, существует
стрелка 1TQr →: , удовлетворяющая соотношениям pmr =o и qrφ =o .
Определение 3.3. THDTS 1T и 2T Obs-бисимуляционны, если существуют THDTS T и Obs-открытые
стрелки 21,φφ такие, что 21
21 TTT φφ →← .
Лемма 3.4. Пусть 21 TT , – THDTS, 21 T:Tf,φ →= α – Obs-открытая стрелка. Тогда если n
TFv
1
∈ , то
n
TFvf
2
∈o при всех },,{ Nn K0∈ .
Доказательство. Пусть существует j
TFu
1
∈ )( nj ≤≤1 такая, что 0
2TFtuf ∈=o . Всегда найдутся
1
1 1Tk Fuu ∈,,K такие, что ∈)()()( j
k QuQuQu 11
1 K Obs. Тогда диаграмма
m
P
1T
Q
2T
p
φ
q
rm
P
1T
Q
2T
p
q
φm
( ( ) ( ) ( )j
k QuQuQu
φρm 11
1 K
o= , где )())(())(( 011
12 QtQufQufρ:T kK→ , причем ( )( ) ( )( ) ( ) idρ
QtQufQuf k
=011
1 K
, а p,q –
тождественные вложения) коммутативна. Тогда по определению Obs-открытой стрелки существует стрелка
1
011
1 TQtQufQufr k →)())(())((: K такая, что mrp o= . Но образ )( 0Qt при морфизме r может быть только
точкой, а образ )( jQu при тождественном вложении p имеет размерность 0j > . Получили противоречие.
Значит, n
TFu
1
∈ влечет n
TFuf
2
∈o . Лемма доказана.
Лемма 3.5. Пусть 21 TT , – THDTS, 21 T:Tf,φ →= α – Obs-открытая стрелка. Тогда для любой функции
n
TFu
2
∈ найдется такая функция
1TFx ∈ , что uxf =o при всех },,{ Nn K0∈ .
Доказательство. Допустим, что существует n
TFu
2
∈ такая, что
1TFx ∈∀ uxf ≠o . Можно считать, что
существуют 1
1 2Tk Fvv ∈,,K такие, что [для любого },{ k,i K1∈ существует 1
1Ti Fw ∈ такая, что ii vwf =o ] и
∈)()()( n
k QuQvQv 11
1 K Obs. Тогда диаграмма
( ( ) ( )11
1 QwQw k
φρm
K
o= , где )()()( n
k QuQvQvρ:T 11
12 K→ , причем ( ) ( ) ( ) idρ n
k QuQvQv
=11
1 K
, а p,q – тождественные
вложения) коммутативна. Т.е. по определению Obs-открытой стрелки существует стрелка
1
11
1 TQuQvQr:v n
k →)()()( K такая, что rφq o= . Но q – тождественное вложение. Получили противоречие.
Лемма доказана.
Теорема 3.6. Две THDTS Obs-бисимуляционны тогда и только тогда, когда они бисимуляционны в
соответствии с определением 2.3.
Доказательство. .⇒ Предположим, что существуют THDTS T и 111 α,fφ = , 222 α,fφ = – Obs-
открытые стрелки такие, что 21
21 TTT φφ →← . Положим }Sss,fsf{R T∈= ))()(( 21 . Покажем, что R –
отношение бисимуляции между THDTS 1T и 2T .
Т.к. 21,φφ – морфизмы, то )( Tif1 и )( Tif 2 – начальные состояния 1T и 2T соответственно, т.е.
Rii TT ∈),(
21
.
Из леммы 3.4 и леммы 3.5 следует, что, если Rsfsfss ∈= ))(),((),( 2121 , то для любой функции n
T
n Fx
11 ∈
такой, что 11 sxb n =)( , µxl n =)( 11 , существует функция n
T
n Fx ∈ такая, что )( nn xfx 11 = , sxb n =)( , µxl n =)( , и,
кроме того, )())(( nn xexef 11 = . Аналогично, для любой функции n
T
n Fx ∈ такой, что sxb n =)( , µxl n =)( ,
существует функция n
T
n Fx
22 ∈ такая, что )( nn xfx 22 = , 22 sxb n =)( , µxl n =)( 22 , и, кроме того, )())(( nn xexef 22 = .
Рассмотрим соответствующие ,Fx n
T
n
11 ∈ n
T
n Fx ∈ и .n
T
n Fx
22 ∈ Возьмем путь ),(],[: nn Qx110 →β
),()( nxb 10 =β .xeβ n )()( 11 = Тогда его образ в 2T , по доказанному, есть ),(],[:
~ nn Qx210 →β ),()(
~ nxb 20 =β
).()(
~ nxe 21 =β Покажем, что β~ и β R-бисимуляционны.
)()()( j
k QuQuQu 11
1 K 1T
m
)())(())(( 011
1 QtQufQuf kK
2T
φ
p
q
)()( 11
1 QwQw kK 1T
m
)()()( n
k QuQvQv 11
1 K 2T
φ
p
q
Они, очевидно, R-соотносимы. При действии морфизма длина пути не возрастает, т.к. .1≤fdu
Рассмотрим наблюдения )()()( nn
k QxQuQu 11
1 K и )()()( nn
k QxQvQv 1
11
1 K из T и 1T соответственно,
.)(,,)( kk vufvuf == 1111 K Диаграмма
( ( ) ( ) ( )nn
k QxQuQu
φρm 11
1 K
o= , где )()()( nn
k QxQvQvρ:T 1
11
11 K→ , причем ( ) ( ) ( ) idρ nn
k QxQvQv
=
1
11
1 K
, p,q – тождественные
вложения, а TQxQvQr:v nn
k →)()()( 1
11
1 K – из определения Obs-открытой стрелки) коммутативна. При
тождественном вложении q длина пути β сохранится, т.е. она сохранится при rφ o1 , а значит, длины путей β
и β
~~
( β
~~
– прообраз β при морфизме 1φ ) совпадают. Аналогично, для β
~~
и β~ . Таким образом,
)
~
()( ββ lengthlength = .
Пусть есть путь γ , βγ ~ , )(]),([ nn Qx110 ⊂γ , тогда если γ~ – его образ в 2T , то γ и γ~ R-соотносимы по
доказанному. Кроме того, βγ ~
~~ , т.к. морфизмы сохраняют гомотопность путей (Утверждение 1.5). Таким
образом, β и β~ R-бисимуляционны.
Аналогично в сторону от 2T в 1T .
.⇐ Пусть 21 ~ TT R . Построим следующую THDTS T : рассмотрим пару R-бисимуляционных пробегов
)
~
,( ββ , рассмотрим их гомотопические классы эквивалентности }~),({)( βγγβ tsK Π∈=1 ,
}
~
~~)~,~(~{)
~
( βγγβ tsK Π∈=2 , где sβ =)(0 , tβ =)(1 , sβ ~)(
~
=0 , tβ
~)(
~
=1 . Сопоставим каждой такой паре классов
точку (состояние), т.е. )( 00 Qx , где 00
TFx ∈ . По определению, если γ и γ~ (пробеги в 1T и 2T соответственно)
R-бисимуляционны, sam =)(γ , sam
~)(~ =γ , то для любого пути 1ββ = такого, что sa =)( 0β , ,)(
1
µβ =Tl
существует путь 1
~~ ββ = ( sa ~)(
~
0 =β , µβ =)
~
(
2Tl ) такой, что γβ и βγ ~~ R-бисимуляционны. Каждой такой паре
ββ ~
, , т.е. каждой паре функций ,Fx µ
T
µ
11 ∈ ,Fx µ
T
µ
22 ∈ таких, что µxlxl µ
T
µ
T == )()( 21 21
, sxb µ =)( 1 , sxb µ ~)( =2 ,
)()( 11 βxe µ = , )(
~
)( 12 βxe µ = , сопоставим кубическую функцию ,Fx
µ
T
µ ∈ такую, что µxl µ
T =)( ,
( ) ( )( )γ,KγK)b(x µ ~
21= , ( ) ( )( )βγ,KγβK)e(x
µ ~~
21= .
Очевидно, существует (естественная) стрелка 1111 T:T,fφ →= α (сопоставление, обратное указанному
выше). Можно выбрать такие ,Fx
µ
T
µ ∈ , чтобы эта стрелка была изометрией. Тогда стрелка 2222 T:T,fφ →= α
тоже будет изометрией (это следует из определения 2.3).
Ясно, что если диаграмма
(где ∈QP, Obs, qpm ,, – стрелки) коммутативна, то существует стрелка TQr →: такая, что pmr =o и
qrφ =o1 . Т.е. стрелка 1φ Obs-открыта.
Аналогично для стрелки 2222 T:T,fφ →= α .
Теорема доказана.
P T
p
Q
1T
q
1φ
m
)()()( nn
k QxQuQu 11
1 K T
)()()( nn
k QxQvQv 1
11
1 K 1T
p
1φ
q
rm
Заключение
В работе были получены следующие результаты: введена геометрическая модель временных
многомерных систем переходов; с помощью гомотопии на введенной модели определена бисимуляционная
эквивалентность; построена категория временных многомерных систем переходов; дана альтернативная
характеризация бисимуляции через открытые морфизмы.
В дальнейшем предполагается разработать гомологическую характеризацию бисимуляционной
эквивалентности временных многомерных систем переходов.
Литература
1. F. Bourceux. Handbook of Categorical Algebra. Cambridge: Cambridge University Press (1994).
2. R. van Glabbek. Bisimulation Semantics for Higher Dimentional Automata. Manuscript available on the web as
http://theory.stanford.edu/rvg/hda
3. E. Goubalt, T.P. Jensen. Homology of Higer-Dimensional Automata. Lecture Notes in Computer Science 630 (1992) 254–268.
4. E. Goubalt. Domains of Higer-Dimensional Automata. Lecture Notes in Computer Science 715 (1993).
5. E. Goubalt. The Geometry of Concurrency. PhD thesis, Ecole Normale Superieure. Available at http://www.dmi.ens.fr/goubault.
6. T. Hune, M. Nielsen. Timed Bisimulation and Open Maps. Lecture Notes in Computer Science 1450 (1998) 378–387.
7. M. Joyal, M. Nielsen, G. Winskel. Bisimulation from Open Maps. Information and Computation 127(2) (1996) 378–387.
8. V Pratt. Modeling Concurrency with Geometry. Proceedings of 18th ACM Symposium on Principles of Programming Languages. ACM
Press(1991).
9. V. Sassone, G.L. Catani. Higher-Dimensional Transition Systems. Proceedongs of LICS’96.
10. G. Winskel, M. Nielsen. Models for Concurrency. In Handbook of Logic in Compiter Science 4 (1995)
|
| id | nasplib_isofts_kiev_ua-123456789-2322 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Russian |
| last_indexed | 2025-12-07T17:48:53Z |
| publishDate | 2004 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Ошевская, Е.С, 2008-09-17T14:18:43Z 2008-09-17T14:18:43Z 2004 Об одной геометрической модели временных параллельных процессов / Е.С.Ошевская // Проблеми програмування. — 2004. — N 2,3. — С. 23-29. — Бiбліогр.:10 назв. - рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2322 681.3 The intention of the paper is to study geometric properties of timed concurrent processes. First, we introduce a notion of timed higher
 dimentional transition sistems and then we provide a category-theoretic characterization of bisimulation equivalence in the context of the
 model under consideration. 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/2322 |
| work_keys_str_mv | AT oševskaâes obodnoigeometričeskoimodelivremennyhparallelʹnyhprocessov |