Теоретико-категорная характеризация трассовой эквивалентности для временных автоматных моделей
Данная работа посвящена теоретико-категорному исследованию трассовой эквивалентности в контексте временных автоматных систем переходов. Для данной модели определено понятие открытого морфизма и доказан критерий открытости. Далее сформулировано определение абстрактной эквивалентности в терминах сущ...
Saved in:
| Date: | 2004 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут програмних систем НАН України
2004
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/2338 |
| 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. — С. 16-22. — Бібліогр.: 5 назв. - рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859797244831596544 |
|---|---|
| author | Грибовская, Н.С. |
| author_facet | Грибовская, Н.С. |
| citation_txt | Теоретико-категорная характеризация трассовой эквивалентности для временных автоматных моделей / Н.С. Грибовская// Проблеми програмування 2004. — N 2-3. — С. 16-22. — Бібліогр.: 5 назв. - рос. |
| collection | DSpace DC |
| description | Данная работа посвящена теоретико-категорному исследованию трассовой эквивалентности в контексте временных
автоматных систем переходов. Для данной модели определено понятие открытого морфизма и доказан критерий открытости. Далее
сформулировано определение абстрактной эквивалентности в терминах существования конструкции открытых морфизмов и доказано,
что трассовая эквивалентность совпадает с этой абстрактной эквивалентностью.
The intention of the paper is to show the applicability of the general categorical framework of open maps to the setting of timed
automata models. In particular, we use the framework of open maps to obtain an abstract equivalence notion which is established to coincide with a
timed extension of the well-known trace equivalence.
|
| first_indexed | 2025-12-07T15:10:30Z |
| format | Article |
| fulltext |
Теоретико-категорная характеризация
трассовой эквивалентности для
временных автоматных моделей*
Грибовская Наталия Сергеевна
Институт систем информатики имени А.П.Ершова
Проспект Ак. Лаврентьева, 6, г. Новосибирск, Россия, 630090
moskalyova@iis.nsk.su
Аннотация. Данная работа посвящена теоретико-категорному исследованию трассовой эквивалентности в контексте временных
автоматных систем переходов. Для данной модели определено понятие открытого морфизма и доказан критерий открытости. Далее
сформулировано определение абстрактной эквивалентности в терминах существования конструкции открытых морфизмов и доказано,
что трассовая эквивалентность совпадает с этой абстрактной эквивалентностью.
Abstract. The intention of the paper is to show the applicability of the general categorical framework of open maps to the setting of timed
automata models. In particular, we use the framework of open maps to obtain an abstract equivalence notion which is established to coincide with a
timed extension of the well-known trace equivalence.
1. Введение
В последнее десятилетие методы теории категорий активно используются для описания и изучения
параллельных систем и процессов. Категория включает в себя множество моделей и морфизмы между ними,
которые представляют собой некоторый вид моделирования. Часто такая теория используется для сравнения
различных моделей.
Одним из наиболее важных понятий теории параллельного программирования является понятие
эквивалентности между процессами. Поведенческие эквивалентности обычно используются при
спецификации и верификации с целью сравнения поведения систем, а также упрощения их структуры.
Наиболее известными из них являются трассовые эквивалентности [3]. В этом случае эквивалентность
формулируется в терминах равенства языков систем.
В работе [6] был предложен новый теоретико-категорный подход к исследованию эквивалентностей на
примере бисимуляции. В рамках этого подхода эквивалентность представляется конструкцией открытых
морфизмов. В дальнейшем этот подход стал использоваться и для определения других эквивалентностей
(трассовой, слабой и сильной бисимуляционной, бисимуляционной с сохранением истории и т.д.) (см. [7]).
В настоящее время резко возрос интерес к разработке и исследованию распределенных систем,
функционирующих в режиме реального времени. Поэтому в литературе были сделаны попытки ввести
понятие времени в эквивалентные отношения, чтобы позволить исследовать временные аспекты поведения
систем. Так, например, в статье [4] методами теории категорий была решена проблема разрешимости
временной бисимуляции для временных автоматных моделей – временных систем переходов.
Цель данной работы состоит в разработке теоретико-категорной основы для построения и изучения
временной трассовой эквивалентности в контексте автоматных моделей реального времени – временных
систем переходов.
Статья организована следующим образом. Во втором разделе описывается категория временных систем
переходов, предложенная Хуне и Нильсеном в работе [5], а также различные свойства этой категории. В разд.
3 вводится понятие открытого морфизма и доказывается его критерий. Разд. 4 посвящен теоретико-
категорной характеризации временной трассовой эквивалентности. В частности, в этом разделе определяются
временная трассовая эквивалентность и абстрактная эквивалентность в терминах существования
симметричной конструкции открытых морфизмов. Далее показывается совпадение этих эквивалентностей
для временных систем переходов. Заключение можно найти в разд. 5.
2. Категория временных систем переходов
В данном разделе описывается модель временных систем переходов, их категория, построенная
авторами в работе [5], а также свойства этой категории. Кроме того, данный раздел содержит ряд полезных
определений и обозначений.
* Данная работа частично поддержана Министерством образования Российской Федерации (грант А03-2.8-
353) и Российским фондом фундаментальных исследований (грант 04-01-00789).
Определение 1. Временная система переходов ℑ – это набор (S, Σ, s0, X, T), где
- S – множество состояний, а s0 – начальное состояние,
- Σ – конечный алфавит действий,
- X – множество временных переменных,
- T – множество переходов таких, что T ⊆⊆⊆⊆ S × Σ × ∆ × 2X × S. Здесь ∆ – временная
конструкция, построенная по правилу: ∆ ::= c # x | x+с # y | ∆ ∧ ∆ , где # ∈{≤, <,≥, >}, с
– положительная вещественная постоянная, а x,y – временные переменные. Переход (s, σ, δ, λ,
s') будем обозначать ',, ss → λδσ .
На рисунке 1 состояния временной системы переходов изображаются кругами, а начальное состояние
помечается двойным кругом. Переходы между состояниями изображаются стрелками. Каждая стрелка
помечается действием, временной конструкцией и множеством временных переменных.
Рисунок 1. Пример временной системы переходов.
Пример 1. На рис. 1 изображена временная система переходов ℑ1, в которой множество временных
переменных X1 состоит из двух переменных x и y, а алфавит действий Σ1 содержит три действия: a,b и c.
Чтобы объяснить поведение временной системы переходов приведем ряд полезных понятий.
Множество вещественных неотрицательных чисел будем обозначать как R+.
Определение 2. Временным словом над алфавитом Σ называется конечная последовательность
пар α = (σ1,τ1)(σ2,τ2)(σ3,τ3)…(σn,τn), где для любого 0 ≤ i ≤ n σi ∈ Σ, τi ∈ R+ и, кроме того, τi < τi+1.
Определение 3. Временной функцией прогресса называется функция ν : X → R+, которая каждой
временной переменной системы сопоставляет конкретный момент времени. Определим временную функцию
прогресса (ν+c)(x):=ν(x)+c для любой временной переменной x. Если λ -– множество временных
переменных, то
∈
=→
. (x),
, x 0,
:0](x)[
иначе
если
ν
λ
λν
Будем говорить, что временная конструкция δ выполнена для временной функции прогресса ν тогда
и только тогда, когда выражение δ[ν(x)/x] истинно. Здесь запись δ[y/x] означает синтаксическую замену
переменной x на y в конструкции δ. Временная конструкция δ определяет подмножество в множестве Rm
(m – число временных переменных в множестве X). Будем называть это подмножество δ-подмножеством и
обозначать ||δ||X. Временная функция прогресса ν определяет точку в множестве Rm (обозначается ||ν||X).
Таким образом, временная конструкция δ выполнена для временной функции прогресса ν тогда и только
тогда, когда ||ν||X ∈ ||δ||X.
Определение 4. Пусть ℑ = (S, Σ, s0, X, T) – временная система переходов. Тогда конфигурацией ℑ
называется пара 〈s,ν〉, где s состояние, а ν – временная функция прогресса. Будем говорить, что во
временной системе переходов ℑ существует последовательность выполнения
nnsss nn ννν τστστσ ,...,, ,,
11
,
00
2211 → → → тогда и только тогда, когда для любого i > 0
существует переход ii ss iii →−
λδσ ,,
1 такой, что ||νi-1 + (τi-1 -τi)||X ∈ ||δi||X и νi = (νi-1 + (τi-1 -τi))[λi
→ 0]. Здесь s0 – начальное состояние, ν0 – нулевая постоянная функция и τ0 равно 0. Эта
последовательность выполнения порождает временное слово (σ1,τ1)(σ2,τ2)(σ3,τ3)…(σn,τn).
Теперь можно привести определение языка временной системы переходов.
Определение 5. Языком временной системы переходов ℑ = (S, Σ, s0, X, T) называется
множество { nnnn sssL nn ννντστστσ τστστσ ,...,,),)...(,(),()( ,,
11
,
002211
2211 → → →=ℑ
последовательность выполнения в }ℑ .
Пример 2. Языком временной системы переходов ℑ1, изображенной на рис. 1, является множество
L(ℑ1) = {(a,d1)(c,d2), (a,t1)(b,t2)…(a,t2k-1)(b,t2k)(a,t2k+1)(c,t2k+2) | 0 < d1 ≤ 1, (d2 - d1) ≤ 2, k ≥ 1,
1≤ i ≤ k, 0 < (t2i-1 - t2i-2) ≤ 1, 2 < (t2i - t2i-1) < 4, (t2i - t2i-2) > 4, t0 = 0, 0 < (t2k+1 - t2k ) ≤ 1, (t2k+2 -
t2k+1) ≤ 2}.
В работе [5] авторы построили категорию временных систем переходов, состоящую из временных
систем переходов и морфизмов между ними. Приведем определение морфизма между двумя временными
системами переходов.
Определение 6. Пусть ℑ = (S, Σ, s0, X, T), ℑ' = (S', Σ', s'0, X', T') – две временные системы
переходов. Пара (µ,η) называется морфизмом между ℑ и ℑ' если µ : S → S' – отображение между
множествами состояний, а η : X' → X – отображение между множествами временных переменных,
удовлетворяющие следующим условиям:
- ,')( 00 ss =µ
- Если ',, ss → λδσ в ℑ, то )'()( '',, ss µµ λδσ → в ℑ', кроме того
1. )(' 1 ληλ −= , где { }ληλη ∈∈=− )'(|'')(1 xXx ,
2. ||δ ||X ⊆ || δ'[η(x)/x]||X.
Рисунок 2. Временная система переходов, которая может быть отображена при помощи морфизма во
временную систему переходов, изображенную на рис.1.
Пример 3. Между временными системами переходов ℑ1, изображенной на рис. 1, и ℑ2,
изображенной на рис. 2, существует морфизм (µ1,η1). Функция µ1 отображает состояния t0 и t2 в состояние
s0, а состояния t1 и t3 в состояние s1. Функция η1 отображает временную переменную x во временную
переменную z и временную переменную y в u.
Для функции η : X' → X и временной функции прогресса ν : X → R+ определим временную
функцию прогресса )(1 νη − : X' → R+ , действующую по следующему правилу: ))((:)(1 xηννη =− .
Теперь можно привести полезное свойство морфизма.
Теорема 1. ([5]) Пусть ℑ = (S, Σ, s0, X, T) и ℑ' = (S', Σ', s'0, X' ,T') – временные системы
переходов и (µ,η) – морфизм из ℑ в ℑ'. Тогда если nnsss nn ννν τστστσ ,...,, ,,
11
,
00
2211 → → →
– последовательность выполнения во временной системе переходов ℑ, порождающая временное слово α =
(σ1,τ1)(σ2,τ2)(σ3,τ3)…(σn,τn), то во временной системе переходов ℑ' существует последовательность
выполнения )(),(...)(),()(),( 1,,
1
1
1
,
0
1
0
2211
nnsss nn νηµνηµνηµ τστστσ −−− → → → ,
порождающая то же самое временное слово.
Далее приводится формальное определение категории временных систем переходов.
Определение 7. Категория CTTS∑ содержит временные системы переходов и морфизмы,
определенные выше. При этом композиция морфизмов (µ,η) : ℑ → ℑ' и (µ',η ') : ℑ' → ℑ'' определена по
правилу (µ′,η′)° (µ,η) = (µ′° µ, η° η′), а тождественный морфизм – это пара тождественных функций.
Категория временных систем переходов обладает рядом свойств, которые были доказаны в статье [5].
В качестве основного свойства этой категории отметим наличие бинарных произведений.
3. Открытый морфизм
Данный раздел посвящен изучению открытого морфизма. В частности, здесь определяется
подкатегория категории временных систем переходов CTTS∑ , по этой подкатегории строится понятие
открытого морфизма, а в завершении доказывается критерий открытости для морфизмов вышеупомянутой
категории.
Для начала построим по временному слову α временную систему переходов ℑα.
Определение 8. Пусть α = (σ1,τ1)(σ2,τ2)(σ3,τ3)…(σn,τn) – временное слово. Определим временную
систему переходов ℑα = ),,,,( *
0 αααα TXsS Σ следующим образом:
*,,,,*
1
,,*
0
222111
nsss nnn → → → λδσλδσλδσ
L . То есть данная временная система переходов содержит
n+1 состояние, а множество временных переменных этой системы состоит из всех подмножеств
множества { }**
2
*
1
*
0 ,,,, nssssS K=α . Определим λi и δi по правилам: { }jiji xsx ∈= *|λ и
)( ),( ji
j
xsIij
Xx
i x ττδ −== ∧
∈
, где )|max(),( **
jkji xsikkxsI ∈∧<= , если же такого k не существует,
то 0),( * =ji xsI . Кроме того, считаем, что τ0 = 0. Временные системы переходов вида ℑα определяют
подкласс TTSTW в категории CTTS∑ .
Утверждение 1. Подкласс TTSTW вместе с тождественными морфизмами и морфизмами с пустой
областью определения образуют подкатегорию CTTSTW в категории CTTS∑.
Далее для категории временных систем переходов и выделенной подкатегории можно определить
понятие открытого морфизма, следуя общей схеме, предложенной в работе [JNW96].
Определение 9. Морфизм (µ,η) : ℑ → ℑ' в категории CTTS∑ называется открытым тогда и
только тогда, когда из существования морфизмов (µ1,η1) : ℑα' → ℑ', (µ2,η2) : ℑα → ℑ в категории
CTTS∑ и морфизма (µ3,η3) : ℑα → ℑα' в подкатегории CTTSTW таких, что (µ,η)° (µ2,η2) = (µ,η)°
(µ3,η3), следует существование морфизма (µ4,η4) : ℑα → ℑ в категории CTTS∑ такого, что (µ1,η1) =
(µ,η)° (µ4,η4) и (µ2,η2) = (µ4,η4)° (µ3,η3).
Принимая во внимание построение подкатегории CTTSTW получаем следующую характеризацию
открытого морфизма.
Утверждение 2. Морфизм (µ,η) : ℑ → ℑ' в категории CTTS∑ называется открытым тогда и
только тогда, когда из существования морфизма (µ1,η1) : ℑα → ℑ' следует существование морфизма
(µ2,η2) : ℑα → ℑ такого, что (µ1,η1) = (µ,η)° (µ2,η2).
Теперь приведем критерий открытости для морфизмов в категории CTTS∑..
Теорема 2. Пусть ℑ и ℑ' – временные системы переходов и (µ,η) – морфизм из ℑ в ℑ'. Морфизм
(µ,η) открыт тогда и только тогда, когда для любой последовательности выполнения
nnsss nn ','...','',' ,,
11
,
00
2211 ννν τστστσ → → → в ℑ', порождающей временное слово
(σ1,τ1)(σ2,τ2)(σ3,τ3)…(σn,τn), существует последовательность выполнения
nnsss nn ννν τστστσ ,...,, ,,
11
,
00
2211 → → → в ℑ, порождающая то же самое временное слово и
для любого 0 ≤ i ≤ n выполнено следующее: s'i = µ(si) и )(' 1
ii νην −= .
Доказательство. (⇒) Пусть (µ,η) – открытый морфизм. И пусть
nnsss nn ','...','',' ,,
11
,
00
2211 ννν τστστσ → → → – произвольная последовательность выполнения в
ℑ', порождающая временное слово (σ1,τ1)(σ2,τ2)(σ3,τ3)…(σn,τn). Докажем, что существует
последовательность выполнения nnsss nn ννν τστστσ ,...,, ,,
11
,
00
2211 → → → в ℑ, порождающая то
же самое временное слово и такая, что для любого 0 ≤ i ≤ n выполнено следующее: s'i = µ(si) и
)(' 1
ii νην −= . По теореме 4, доказанной в работе [5], так как
nnsss nn ','...','',' ,,
11
,
00
2211 ννν τστστσ → → → – последовательность выполнения в ℑ', то данной
последовательности можно сопоставить морфизм (µ1,η1) : ℑα → ℑ' такой, что ii ss ')( *
1 =µ ,
{ })0)('()1(|)( *
1 =∧≤≤= xnisx ii νη . Тогда по утверждению 2, так как (µ,η) – открытый морфизм,
убеждаемся в существовании морфизма (µ2,η2) : ℑα → ℑ такого, что (µ1,η1) = (µ,η)° (µ2,η2). Вновь по
теореме 4 из работы [5], морфизму (µ2,η2) можно сопоставить последовательность выполнения
nnsss nn ννν τστστσ ,...,, ,,
11
,
00
2211 → → → в ℑ, при этом ii ss =)( *
2µ ,
{ })0)(()1(|)( *
2 =∧≤≤= xnisx ii νη . Далее имеем, что для любого 0 ≤ i ≤ n s'i = =)( *
1 isµ µ °
=)( *
2 isµ µ(si). Кроме того, так как η1 = η2 ° η, то по определению этих функций получаем:
{ })0)('()1(|)( *
1 =∧≤≤= xnisx ii νη = == ))(()( 22 xx ηηηη o { })0))((()1(|* =∧≤≤ xnis ii ην .
Таким образом, получаем, что для любого 0 ≤ i ≤ n верно ( ) ( )0))((0)(' =⇔= xx ii ηνν . Отсюда,
учитывая то, что обе последовательности выполнения порождают одно и тоже слово, получаем, что
)(' 1
ii νην −= .
(⇐) Пусть выполнены условия теоремы, то есть из существования последовательности выполнения
nnsss nn ','...','',' ,,
11
,
00
2211 ννν τστστσ → → → в ℑ', порождающей временное слово
(σ1,τ1)(σ2,τ2)(σ3,τ3)…(σn,τn), следует существование последовательности выполнения
nnsss nn ννν τστστσ ,...,, ,,
11
,
00
2211 → → → в ℑ, порождающей то же самое временное слово и
удовлетворяющей следующим свойствам: s'i = µ(si) и )(' 1
ii νην −= для любого 0 ≤ i ≤ n. Докажем, что
морфизм (µ,η) открыт. Для этого воспользуемся утверждением 2. Пусть (µ1,η1) : ℑα → ℑ' – морфизм.
Тогда по теореме 4 из работы [5] этому морфизму можно сопоставить последовательность выполнения
nnsss nn ','...','',' ,,
11
,
00
2211 ννν τστστσ → → → в ℑ', порождающую временное слово α =
(σ1,τ1)(σ2,τ2)(σ3,τ3)…(σn,τn), при этом ii ss ')( *
1 =µ , а { })0)('()1(|)( *
1 =∧≤≤= xnisx ii νη . По условию
теоремы имеем последовательность выполнения nnsss nn ννν τστστσ ,...,, ,,
11
,
00
2211 → → → в ℑ,
порождающую то же самое временное слово и удовлетворяющую следующим свойствам: s'i = µ(si) и
)(' 1
ii νην −= для любого 0 ≤ i ≤ n. Вновь по теореме 4 из работы [5] данной последовательности
выполнения можно сопоставить морфизм (µ2,η2) : ℑα → ℑ такой, что ii ss =)( *
2µ ,
{ })0)(()1(|)( *
2 =∧≤≤= xnisx ii νη . Отсюда заключаем, что =)( *
1 isµ s'i = µ(si) = µ( )( *
2 isµ ) = µ °
)( *
2 isµ для любого αSsi ∈* . Кроме того, имеем, что =)(1 xη
{ })0)('()1(|* =∧≤≤ xnis ii ν ={ })0))((()1(|* =∧≤≤ xnis ii ην = )())(( 22 xx ηηηη o= . То есть,
(µ1,η1) = (µ,η)° (µ2,η2). Таким образом, в силу утверждения 2 морфизм (µ,η) открыт.
4. Характеризация трассовой эквивалентности
В данном разделе определяется понятие абстрактной эквивалентности для временных систем
переходов, приводится определение временной трассовой эквивалентности, а также доказывается совпадение
этих эквивалентностей.
Определение 10. Две временные системы переходов ℑ и ℑ' называются TW*-эквивалентными
тогда и только тогда, когда существует конструкция открытых морфизмов '* )'',(),( ℑ →ℑ ←ℑ ηµηµ
с вершиной ℑ*.
Корректность этого определения следует из теоремы 3, доказанной в статье [5], и утверждения 3,
приведенного в работе [6].
Далее приведем понятие временной трассовой эквивалентности.
Определение 11. Две временные системы переходов ℑ и ℑ' называются трассово эквивалентными
тогда и только тогда, когда их языки совпадают, то есть L(ℑ) = L(ℑ′).
Пример 4. На рис. 3 изображены трассово эквивалентные временные системы переходов ℑ3 и ℑ4.
Временные же системы переходов ℑ1 и ℑ2 не являются трассово эквивалентными, так как временное слово
(a,1)(c,2) принадлежит языку L(ℑ1), но не принадлежит L(ℑ2).
Рисунок 3. Трассово эквивалентные временные системы переходов.
Теперь можно сформулировать основной результат данной статьи.
Теорема 3. Две временные системы переходов ℑ и ℑ' TW*-эквивалентны тогда и только тогда,
когда они трассово эквивалентны.
Доказательство. (⇒) Пусть ℑ и ℑ' TW*-эквивалентны, тогда по определению существует
конструкция открытых морфизмов '* )'',(),( ℑ →ℑ ←ℑ ηµηµ . Покажем, что L(ℑ) = L(ℑ*). Пусть
)(ℑ∈ Lα . Тогда по теореме 1 заключаем, что *)(ℑ∈ Lα , так как (µ,η) – морфизм. Это означает, что
L(ℑ) ⊆ L(ℑ*). Пусть теперь *)(ℑ∈ Lα . Тогда в силу того, что (µ,η) открытый морфизм, по теореме 2
получаем, что )(ℑ∈ Lα , то есть L(ℑ*) ⊆ L(ℑ). Таким образом, L(ℑ) = L(ℑ*). Аналогично получаем,
что L(ℑ′) = L(ℑ*), а значит L(ℑ) = L(ℑ′). То есть временные системы переходов ℑ и ℑ' трассово
эквивалентны.
(⇐) Пусть ℑ и ℑ' трассово эквивалентны, тогда по определению получаем, что L(ℑ) = L(ℑ′). По
теореме 2 из статьи [5] получаем существование произведения ℑ × ℑ' двух временных систем переходов ℑ и
ℑ'. По свойствам бинарного произведения в категории получаем существование морфизмов (µ,η) : ℑ × ℑ'
→ ℑ и (µ',η ') : ℑ × ℑ' → ℑ'. Проверим, что эти морфизмы открыты. Воспользуемся утверждением 2.
Пусть существует морфизм (µ1,η1) : ℑα → ℑ, где временное слово α = (σ1,τ1)(σ2,τ2)… (σn,τn ). Тогда
по теореме 4 из работы [5] получаем, что в ℑ существует последовательность выполнения
nnsss nn ννν τστστσ ,...,, ,,
11
,
00
2211 → → → , порождающая временное слово α. Так как по
условию теоремы L(ℑ) = L(ℑ′), то в ℑ' существует последовательность выполнения
nnsss nn ','...','',' ,,
11
,
00
2211 ννν τστστσ → → → , порождающая то же самое временное слово.
Вновь по теореме 4, доказанной в статье [5], получаем, что данной последовательности выполнения можно
сопоставить морфизм (µ2,η2) : ℑα → ℑ'. Тогда по свойствам произведения в категории (см. работу [1])
получаем существование морфизма (µ3,η3) : ℑα → ℑ × ℑ' такого, что (µ1,η1) = (µ,η)° (µ3,η3) и (µ2,η2)
= (µ',η ')° (µ3,η3). Таким образом, в силу утверждения 2 морфизм (µ,η) открыт. Аналогично доказывается
открытость морфизма (µ′,η′).
5. Заключение
В этой работе сделана попытка применить методы теории открытых морфизмов [6] при исследовании
трассовых эквивалентностей временных автоматных моделей. В частности, была получена теоретико-
категорная характеризация наиболее известной эквивалентности – временной трассовой эквивалентности –
для временных систем переходов. В дальнейшем планируется расширить полученный результат на
временные варианты тестовой эквивалентности.
Литература:
1. М.Ш. Цаленко, Е.Г. Шульгейфер. Лекции по теории категорий. – М: Наука, 1974, – 438 с.
2. Н.С. Москалева. Теоретико-категорная характеризация трассовой эквивалентности временных параллельных моделей.
Препринт ИСИ СО РАН № 99, 2002.
3. C.A.R. Hoare. Communicating Sequential Processes. – Prentice-Hall, 1985.
4. T. Hune, M. Nielsen. Timed bisimulation and open maps. // Lect. Notes Comput. Sci.– Berlin etc., 1998. – Vol. 1450. – p. 378-387.
5. T. Hune, M. Nielsen. Timed bisimulation and open maps. Technical Report RS-98-4, BRICS, 1998.
6. А. Joyal, M. Nielsen, G. Winskel. Bisimulation from open maps. // Information and Computation, 1996. – Vol. 127(2). – p. 164-185.
7. M. Nielsen, A. Cheng. Observing behaviour categorically. // Lect. Notes Comput. Sci.– Berlin etc., 1996. – Vol. 1026. – p. 263-278.
|
| id | nasplib_isofts_kiev_ua-123456789-2338 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Russian |
| last_indexed | 2025-12-07T15:10:30Z |
| publishDate | 2004 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Грибовская, Н.С. 2008-09-17T15:24:20Z 2008-09-17T15:24:20Z 2004 Теоретико-категорная характеризация трассовой эквивалентности для временных автоматных моделей / Н.С. Грибовская// Проблеми програмування 2004. — N 2-3. — С. 16-22. — Бібліогр.: 5 назв. - рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2338 681.3 Данная работа посвящена теоретико-категорному исследованию трассовой эквивалентности в контексте временных автоматных систем переходов. Для данной модели определено понятие открытого морфизма и доказан критерий открытости. Далее сформулировано определение абстрактной эквивалентности в терминах существования конструкции открытых морфизмов и доказано, что трассовая эквивалентность совпадает с этой абстрактной эквивалентностью. The intention of the paper is to show the applicability of the general categorical framework of open maps to the setting of timed automata models. In particular, we use the framework of open maps to obtain an abstract equivalence notion which is established to coincide with a timed extension of the well-known trace equivalence. Данная работа частично поддержана Министерством образования Российской Федерации (грант А03-2.8-353) и Российским фондом фундаментальных исследований (грант 04-01-00789). 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/2338 |
| work_keys_str_mv | AT gribovskaâns teoretikokategornaâharakterizaciâtrassovoiékvivalentnostidlâvremennyhavtomatnyhmodelei |