=Paper=
{{Paper
|id=None
|storemode=property
|title=A Domain View of Timed Behaviors
|pdfUrl=https://ceur-ws.org/Vol-1032/paper-10.pdf
|volume=Vol-1032
|dblpUrl=https://dblp.org/rec/conf/csp/DubtsovOV13
}}
==A Domain View of Timed Behaviors==
https://ceur-ws.org/Vol-1032/paper-10.pdf
A Domain View of Timed Behaviors ?
Roman Dubtsov1 , Elena Oshevskaya2 , and Irina Virbitskaite2
1
Institute of Informatics System SB RAS,
6, Acad. Lavrentiev av., 630090, Novosibirsk, Russia;
2
Institute of Mathematics SB RAS,
4, Acad. Koptyug av., 630090, Novosibirsk, Russia;
dubtsov,eso,virb@iis.nsk.su
Abstract. The intention of this paper is to introduce a timed extension
of transition systems with independence, and to study its categorical
interrelations with other timed ”true-concurrent” models. In particular,
we show the existence of a chain of coreflections leading from a category
of the model of timed transition systems with independence to a category
of a specially defined model of marked Scott domains. As an intermediate
semantics we use a model of timed event structures, able to properly
capture causality, conflict, and concurrency among events which arise in
the presence of time delays of the events.
1 Introduction
The behaviour of concurrent systems is often specified in terms of states and
transitions between states, the labels on the transitions represent the observable
part of system’s behaviour. The simplest formal model of computation able to
express naturally this idea is that of labelled transition systems. However, they
are a representative of the interleaving approach to concurrency and hence do
not allow one to draw a natural distinction between interleaved and concurrent
executions of system’s actions. Two most popular ”true concurrent” extensions of
transition systems, aiming to overcome limitations of the interleaving approach,
are asynchronous transition systems, introduced independently by Bednarczyk
[1] and Shields [2], and transitions systems with independence, proposed by
Winskel and Nielsen [3].
Category theory [4] has been successfully exploited to structure the tangled
world of models for concurrency. Within this framework, objects of categories
represent processes and morphisms correspond to behavioural relations between
the processes, i.e. to simulations. The category-theoretic approach allows for
natural formalization of the fact that one model is more expressive than another
in terms of an ”embedding”, most often taking the form of a coreflection, i.e. an
adjunction in which the unit is an isomorphism. For example, Hildenbrandt and
?
The second author is supported in part by the RFBR (grant 12-01-00873-a), by the
President Program ”Leading Scientific Schools” (grant NSh-7256.2010.1), and by the
Federal Program ”Research and educational personnel for innovative Russia” (grant
8206).
112 R. Dubtsov, E. Oshevskaya, I. Virbitskaite
Sassone [5] have constructed a full subcategory of a category of asynchronous
transition systems and have shown the existence of a coreflection between the
subcategory and a category of transition systems with independence. In their
next paper [6], the authors have enriched the model of transition systems with
independence by adding multi-arcs and have yielded a precise characterization
of the model in terms of (event-maximal, diamond-extensional) labeled asyn-
chronous transition systems, by constructing functors between categories of the
models.
It is generally acknowledged that time plays an important role in many con-
current and distributed systems. This has motivated the lifting of the theory
of untimed systems to the real-time setting. Timed transition system like mod-
els have been studied thoroughly within the two last decades (see [7,8] among
others), while timed ”true concurrent” extensions have hitherto received scant
attention.
The aim of this paper is to introduce a timed extension of transition systems
with independence, and to study its categorical interrelations with other timed
”true-concurrent” models. In particular, we show the existence of a chain of
coreflections leading from a category of the model of timed transition systems
with independence to a category of a specially defined model of marked Scott
domains. As an intermediate semantics we use a model of timed event structures,
able to properly capture causality, concurrency, and conflict among events which
arise in the presence of time delays of the events.
The paper is organized as follows. In Section 2, the notions and notations
concerning the structure and behaviour of timed transition systems with in-
dependence are described. Also, an unfolding of timed transition systems with
independence is constructed, and it is shown that together with the inclusion
functor the unfolding functor defines a coreflection. Section 3 establishes the in-
terrelations in terms of the existence of a coreflection between timed occurrence
transition systems with independence and timed event structures. In Section 4,
using the equivalence of the categories of timed event structures and marked
Scott domains, stated in [9], functors between the categories of timed transition
systems with independence and marked Scott domains are constructed to consti-
tute a coreflection. Section 5 provides a direct translation from timed transition
systems with independence to marked Scott domains, established in the categor-
ical setting. In section 6, we conclude with a short summary of the discovered
relationships.
2 Timed Transition Systems with Independence
In this section, we first describe the basic notions and notations concerning the
structure and behaviour of timed transition systems with independence.
We start with untimed case. A transition system with independence is a
tuple T I = (S, sI , L, T ran, I), where S is a countable set of states, sI ∈ S is the
initial state, L is a countable set of labels, T ran ⊆ S × L × S is the transition
relation, and I⊆ T ran×T ran is the irreflexive, symmetric independence relation,
A Domain View of Timed Behaviors 113
such that, using ≺ to denote the following relation on transitions (s, a, s0 ) ≺
(s00 , a, u) ⇐⇒ ∃(s, b, s00 ), (s0 , b, u) ∈ T ran s.t. (s, a, s0 ) I (s, b, s00 ) ∧ (s, a, s0 ) I
(s0 , b, u)∧(s, b, s00 ) I (s00 , a, u), and ∼ for the least equivalence relation containing
≺, we have:
1. (s, a, s0 ) ∼ (s, a, s00 ) ⇒ s = s00 ,
2. (s, a, s0 ) I (s, b, s00 ) ⇒ ∃(s0 , b, u), (s00 , a, u) ∈ T ran (s, a, s0 ) I (s0 , b, u) ∧
(s, b, s00 ) I (s00 , a, u),
3. (s, a, s0 ) I (s0 , b, u) ⇒ ∃(s, b, s00 ), (s00 , a, u) ∈ T ran (s, a, s0 ) I (s, b, s00 ) ∧
(s, b, s00 ) I (s00 , a, u),
4. (s, a, s0 ) ∼ (s00 , a, u) I (w, b, w0 ) ⇒ (s, a, s0 ) I (w, b, w0 ).
Let Diama,b (s, s0 , s00 , u) ⇐⇒ ∃(s, a, s0 ), (s, b, s00 ), (s0 , b, u), (s00 , a, u) ∈ T ran
(s, a, s0 ) I (s, b, s00 ) ∧ (s, a, s0 ) I (s0 , b, u) ∧ (s, b, s00 ) I (s00 , a, u). We say that the
transitions above form an independence diamond, and denote the ∼-equivalence
class of a transition t ∈ T ran as [t].
A transition system with independence functions by executing transitions
from one state to another. A possibly infinite sequence π = t0 t1 . . . with ti =
(si , ai , si+1 ) ∈ T ran (i ≥ 0) is called a path. The starting state of π is denoted
as dom(π), and the ending state as cod(π) if π is a finite path. A computation is
a path π such that dom(π) = sI . Let Comp(T I) (Comp0 (T I)) be the set of all
(finite) computations of T I. A transition t is said to be reachable, if there exists a
computation π ∈ Comp0 (T I) such that t appears in π. From now on, we consider
only those transition systems with independence in which all transitions are
reachable. Let '⊆ Comp(T I) × Comp(T I) be the least equivalence relation such
that πs (s, a, s0 )(s0 , b, u)πv ' πs (s, b, s00 )(s00 , a, u)πv ⇐⇒ Diama,b (s, s0 , s00 , u),
and let [π] stand for the '-equivalence class of a computation π.
We now incorporate time into the model of transition systems with indepen-
dence. By analogy with the paper [8], we assume a global, fictitious clock, whose
actions advance time by nonuniform amounts and whose value is set to zero at
the beginning of system’s functioning. All transitions are associated with timing
constraints represented as minimal and maximal time delays, and happen ”in-
stantaneously”, while timing constraints restrict the times at which transitions
may be executed. Unlike the paper [8], in our timed model the time domain is
changed to the integers, and the maximal delays associated with transitions are
always equal to ∞, therefore they are not specified explicitly.
Let N be the set of non-negative integers.
Definition 1. A timed transition system with independence is a tuple T T I =
(S, sI , L, T ran, I, δ), where JT T IK = (S, sI , L, T ran, I) is the underlying transi-
tion system with independence, and δ : T ran → N is the delay function such
that δ(t) = δ(t0 ) for any t, t0 ∈ T ran such that t ∼ t0 .
A timed computation of a timed transition system with independence T T I =
(S, sI , L, T ran, I, δ) is a pair Π = (π, τ ) ∈ (Comp((S, sI , L, T ran, I)) × (N ∪
{∞})) with τ ≥ δ(π) = sup{δ(t) | t ∈ π}. Define dom(Π) = dom(π) and
cod(Π) = cod(π). We denote the set of all (finite) timed computations of T T I as
114 R. Dubtsov, E. Oshevskaya, I. Virbitskaite
TComp(T T I) (TComp0 (T T I)), and write Π 'τ Π 0 iff π ' π 0 and τ = τ 0 . It is
easy to see that 'τ is an equivalence relation; the 'τ -equivalence class of a timed
computation Π is denoted as [Π]τ . Let TComp'τ (T T I) (TComp0'τ (T T I)) be
the sets of 'τ -equivalence classes of all (finite) timed computations of T T I.
For timed transition systems with independence T T I = (S, sI , L, T ran, I, δ)
and T T I 0 = (S 0 , s0I , L0 , T ran0 , I 0 , δ 0 ), a morphism h : T T I → T T I 0 is a pair of
mappings h = (σ : S → S 0 , λ : L →∗ L0 )3 such that:
1. σ(sI ) = s0I ,
2. (s, a, s0 ) ∈ T ran ⇒ (σ(s), α(a), σ(s0 ) ∈ T ran0 if a ∈ dom λ, and σ(s) =
σ(s0 ), otherwise,
3. (s, a, s0 )I(s̄, ā, s̄0 ) and a, ā ∈ dom λ ⇒ (σ(s), α(a), σ(s0 )I 0 (σ(s̄), α(ā), σ(s̄0 ),
4. δ 0 ((σ(s), α(a), σ(s0 ))) ≤ δ((s, a, s0 )).
Timed transition systems with independence and morphisms between them
form a category TTSI with unit morphisms 1T T I = (1S , 1L ) : T T I → T T I for
any T T I = (S, sI , L, T ran, I, δ), and with composition defined in a component-
wise manner.
We next aim at unfolding of timed transition systems with independence. To
that end, we first define a subclass of timed transition systems with indepen-
dence that serves as a target of unfolding. After that, we construct an unfolding
mapping and show that together with the inclusion functor the unfolding functor
defines a coreflection.
Definition 2. A timed occurrence transition system with independenceT oT I =
(S, s0 , L, T ran, I, δ) is an acyclic timed transition system with independence such
that (s00 , a, u) 6= (s0 , b, u) ∈ T ran ⇒ ∃s ∈ S s.t. Diama,b (s, s0 , s00 , u), for all
(s00 , a, u), (s0 , b, u) ∈ T ran.
Let ToTSI be the full subcategory of the category TTSI.
Define an unfolding mapping ttsi .totsi : TTSI → ToTSI as follows. For a
timed transition system with independence T T I = (S, sI , L, T ran, I, δ), specify
ttsi .totsi (T T I) as (S'τ , [(sI , 0)]τ , L, T ran'τ , I'τ , δ'τ ), where
– S'τ = {[Π = (π, δ(π))]τ ∈ TComp0'τ (T T I)},
– ([Π = (π, δ(π))]τ , a, [Π 0 = (π 0 , δ(π 0 ))]τ ) ∈ T ran'τ ⇐⇒ ∃tπ,π0 = (s, a, s0 ) ∈
T ran Π 0 'τ (πtπ,π0 , max{δ(π), δ(π 0 )}),
– ([Π]τ , a, [Π 0 ]τ )I'τ ([Π̄]τ , b, [Π̄ 0 ]τ ) ⇐⇒ tπ,π0 Itπ̄,π̄0 ,
– δ'τ ([Π]τ , a, [Π 0 ]τ ) = δ(tπ,π0 ).
Lemma 1. Given a timed transition system with independence T T I,
ttsi .totsi (T T I) is a timed occurrence transition system with independence.
3
A partial mapping from a set A into a set B is denoted as f : A →∗ B. Let
dom f = {a ∈ A | f (a) is defined}. For a subset A0 ⊆ A, define f A0 = {f (a0 ) | a0 ∈
A0 ∩ dom f }.
A Domain View of Timed Behaviors 115
In order to demonstrate that the mapping ttsi .totsi is adjoint to the inclusion
functor ToTSI ,→ TTSI, we define a mapping and prove that it is the unit of
this adjunction. For a transition system with independence T T I, let εT T I =
(σε , 1L ) : ttsi .totsi (T T I) → T T I, where σε ([Π]τ ) = cod(Π) for all [Π]τ ∈ S'τ .
It is easy to see that εT T I is a morphism of TTSI.
Lemma 2 (εT T I is couniversal). For any object T T I of TTSI, any object
T oT I of ToTSI and any morphism h : T oT I → T T I of TTSI, there exists a
unique morphism h0 : T oT I → ttsi .totsi (T T I) of ToTSI such that h = εT T I ◦h0 .
The next theorem presents a categorical characterization of the unfolding.
Theorem 1 (,→a ttsi .totsi ). The unfolding mapping ttsi .totsi extends to a
functor from TTSI → ToTSI which is right adjoint to the functor ,→: ToTSI →
TTSI. Moreover, this adjunction is a coreflection.
3 Timed Event Structures
In this section we relate timed occurrence transition systems with independence
and timed event structures, establishing the close relationships between cate-
gories of the models.
We start with the definition of an untimed variant of event structures. An
event structure is a triple E = (E, ≤, #), where E is a countable set of events;
≤⊆ E × E is a partial order (the causality relation) such that ↓e = {e0 ∈ E |
e0 ≤ e} is a finite set for each e ∈ E, #⊆ E × E is the symmetric irreflexive
conflict relation such that e # e0 ≤ e00 ⇒ e # e00 . A set of events C ⊆ E is
said to be a configuration of an event structure E if ∀e ∈ C ↓e ⊆ C, and
∀e, e0 ∈ C ¬(e # e0 ). We say that events e, e0 ∈ E are concurrent and write
e ^ e0 if ¬(e ≤ e0 ∨ e0 ≤ e0 ∨ e # e0 ). Introduce the concept of a reflexive conflict
as follows: e ∨∨ e0 ⇐⇒ e # e0 ∨ e = e0 .
We now recall the definition of timed event structures from [9]. Similarly to
the model of timed transition systems with independence, there is a global non-
negative integer-valued clock. Each event in the structure is associated with a
time delay with respect to the initial time moment; i.e., if an event e is associated
with a time delay t, then e may not occur earlier than all the predecessors of
the event occur and the clock shows time t. In this case, the event itself occurs
instantaneously.
Definition 3. A timed event structure is a tuple T E = (E, ≤, #, ∆), where
(E, ≤, #) is an event structure and ∆ : E → N is the delay function such that
e0 ≤ e ⇒ ∆(e0 ) ≤ ∆(e).
A timed configuration of T E is a pair (C, τ ), where C is a configuration of
(E, ≤, #) and τ ∈ N ∪ {∞} such that τ ≥ ∆(C) = sup{∆(e) | e ∈ C}. The
set of all (finite) timed configurations of a timed event structure T E is denoted
as TConf(T E) (TConf 0 (T E)). We define a transition relation −→ on the set
116 R. Dubtsov, E. Oshevskaya, I. Virbitskaite
TConf(T E) as follows: (C, t) −→ (C 0 , t0 ) if C ⊆ C 0 and t ≤ t0 . Clearly, the
relation −→ specifies a partial order on the set TConf(T E).
Let T E = (E, ≤, #, ∆) and T E 0 = (E 0 , ≤0 , #0 , ∆0 ) be timed event structures.
A partial mapping θ : E →∗ E 0 is a morphism if ↓θ(e) ⊆ θ ↓e; θ(e) ∨∨ θ(e0 ) ⇒
e ∨∨ e0 , for all e, e0 ∈ dom θ; ∆0 (θ(e)) ≤ ∆(e), for all e ∈ dom θ. Timed event
structures with their morphisms define a category TES with unit morphisms
1T S = 1E : T S → T S for all T S = (E, ≤, #, ∆) and the composition being a
usual composition of partial functions.
We now establish the relationships between the categories of timed event
structures and timed occurrence transition systems with independence. For this
purpose, we first define a mapping tpes.totsi : TPES → ToTSI extending the
mapping pes.otsi from [3] to the timed case. For a timed event structure T E =
(E, ≤,#,∆), let tpes.totsi (T E) be (ST E , sIT E , LT E , T ranT E , IT E , δT E ), where
– ST E = (C, ∆(C)) ∈ TConf 0 (T E) ;
– sIT E = (∅, 0);
– LT E = E;
– (C, ∆(C)), e, (C 0 , ∆(C 0 )) ∈ T ranT E ⇐⇒ C 0 \ C = {e};
– (C, ∆(C)), e, (C 0 , ∆(C 0 )) IT E (C̄, ∆(C̄)), ē, (C̄ 0 , ∆(C̄ 0 )) ⇐⇒ e ^ ē;
– δT E ((C, ∆(C)), e, (C 0 , ∆(C 0 ))) = ∆(e).
It is easy to see that the above definition is correct, i.e. tpes.totsi maps timed
event structures to timed occurrence transition systems with independence.
Next, we construct a mapping totsi .tpes : ToTSI → TPES. For a timed
occurrence transition system with independence T oT I = (S, sI , L, T ran, I, δ),
let totsi .tpes(T oT I) be (T ran∼ , ≤, #,∆), where
– T ran∼ = {[t] | t ∈ T ran},
– [t] < [t0 ] ⇐⇒
∀(π t̄0 , τ ) ∈ TComp0 (T oT I) t̄0 ∼ t0 ⇒ (∃t̄ ∈ π t̄ ∼ t); ≤=< ∪ =,
– [t] # [t0 ] ⇐⇒
∀(π, τ ) ∈ TComp0 (T oT I), ∀t̄ ∈ [t], ∀t̄0 ∈ [t0 ] t̄ ∈ π ⇒ t̄0 ∈
/ π,
– ∆([t]) = max{δ(t0 ) | [t0 ] ≤ [t]}.
On morphisms h = (σ, λ) : T oT I → T oT I 0 in ToTSI, the mapping totsi .tpes
acts as follows: totsi .tpes(h) = θ, where θ([(s, a, s0 )]) = [(σ(s), λ(a), σ(s0 )], if
a ∈ dom λ, and θ([(s, a, s0 )]) is undefined, otherwise.
Proposition 1. totsi .tpes : ToTSI → TPES is a functor.
Finally, we define the unit of the adjunction. For a timed event structure
T E, let ηT E : ET E → Etotsi.tpes◦tpes.totsi(T E) be a mapping such that ηT E (e) =
[(C, ∆(C)), e, (C ∪ {e}, ∆(C ∪ {e}))]. It is straightforward to show that ηT E is an
isomorphism in TPES. In order to demonstrate the existence of the adjunction,
we need to check that ηT E is indeed a unit, i.e. it is universal.
Lemma 3 (ηT E is universal).
For any object T E of TPES, any object T oT I of ToTSI, and any mor-
phism θ : T E → totsi .tpes(T oT I) in TPES, there exists a unique morphism
h : tpes.totsi (T E) → T oT I in ToTSI such that θ = totsi .tpes(h) ◦ ηT E .
A Domain View of Timed Behaviors 117
The next theorem establishes the existence of a coreflection between the
categories of timed event structures and timed occurrence transition systems
with independence.
Theorem 2 (tpes.totsi a totsi .tpes). The map tpes.totsi can be extended to
a functor tpes.totsi : TPES → ToTSI, which is left adjoint to the functor
totsi .tpes. Moreover, this adjunction is a coreflection.
4 Marked Scott Domains
In this section, we extend the established chain of coreflections to marked Scott
domains. To that end, we first recall related notions and notations.
Let (D, v) be a partial order, d ∈ D and X ⊆ D. Then,
– ↑d = {d0 ∈ D | d v d0 } is an upper cone of element d, ↓d = {d0 ∈ D | d0 v d}
is a lower cone of element d,
– X is downward (upward) closed if ↓d ⊆ X (↑d ⊆ X) for every d ∈ X,
– X is a compatible set (denoted as X↑), if the following assertion is true:
∃d ∈ D∀x ∈ X x v d, i.e., X has an upper bound. If X = {x, y}, we write
x ↑Fy instead of {x, y}↑. The least upper bound of the set X isddenoted
as X (if it exists), and the greatest lower bound is denoted as X (if it
exists). The least upper bound of two elements x and y is denoted as x t y,
and the greatest lower bound, as x u y.
– X is a finitely compatible set if any finite subset of it X 0 ⊆ X is compatible.
– X is a (upper) directed set if any finite subset of it X 0 ⊆ X has an upper
bound belonging to the set X (thus, X is a finitely compatible and nonempty
set).
– (D, v) is a directed-complete
F partial order (dcpo for short) if every directed
subset X ⊆ D has X.
– d is a finite (compact) element of a dcpo (D, F v) if, for any directed subset
X ⊆ D, the following assertion is true: d v X ⇒ ∃x ∈ X d v x. The set
of finite elements is denoted as C(D). F
– A dcpo (D, v) is said to be algebraic if, for any d ∈ D, d = {e v d | e ∈
C(D)}. It is said to be ω-algebraic if C(D) is countable.
– (D, v) is a consistently F complete partial order (ccpo) if any finitely compat-
F
ible subset X ⊆ D has X. Clearly, a ccpo has the least element ⊥ = ∅,
and is also a dcpo.
– An ω-algebraic ccpo is called a Scott domain. A Scott domain (D, v) is said
to be finitary if ↓d is finite for every d ∈ C(D).
Describe some properties of Scott domains. An element p of a Scott F domain
(D, v) is said to be prime if, for any compatible subset X ⊆ D p v X ⇒ ∃x ∈
X p v x. The set of the prime elements is denoted as F P (D). A Scott domain
(D, v) is called prime algebraic if, for any d ∈ D, d = {p v d | p ∈ P (D)} and
coherent if all subsets X ⊆ D satisfying the condition ∀d0 , d00 ∈ X d0 ↑ d00 have
F
X.
118 R. Dubtsov, E. Oshevskaya, I. Virbitskaite
Let (D, v) be a Scott domain and ≺ = @ \ @2 be a covering relation. For
elements d, d0 ∈ D such that d ≺ d0 , the pair [d, d0 ] is called a prime interval. The
set of all prime intervals is denoted as I(D). We write [c, c0 ] ≤ [d, d0 ] if and only
if c = c0 u d ∨ d0 = c0 t d. The relation ∼ is defined to be a transitive symmetric
closure of the relation ≤. Note that ∼-equivalent prime intervals model one and
the same action. Let [d, d0 ]∼ denote the ∼-equivalence class of the prime interval
[d, d0 ].
Now we are ready to present the definition of marked Scott domains. Infor-
mally, a marked Scott domain is meant to be a prime algebraic, finitary, and
coherent Scott domain with the prime intervals modeling two – instantaneous
and delayed – types of system actions. The former actions do not require time
and are marked by zero, and the latter take one unit of time and are marked by
one. It is natural to require that the ∼-equivalent prime intervals corresponding
to one and the same system action are marked identically.
Definition 4. A marked domain is a triple (D, v, m), where (D, v) is a prime
algebraic, finitary, and coherent Scott domain and m : I(D) −→ {0, 1} is a
marking such that [c, c0 ] ∼ [d, d0 ] ⇒ m([c, c0 ]) = m([d, d0 ]).
Introduce auxiliary notions and notations. For d, d0 ∈ D and i ∈ {0, 1}, we
write d ≺i d0 , if d ≺ d0 ∧ m([d, d0 ]) = i, and d 4i d0 , if d ≺i d0 ∨ d = d0 ;
vi = (≺i )∗ ; ↓i d = {d0 | d0 vi d}, and ↑i d = {d0 | d vi d0 }; P i (D) = {p ∈
P (D) | ∃d ∈ D m([d, p]) = i}. For a finite element d ∈ D and a covering
chain σ having the form ⊥ = d0 ≺k1 d1 · · · dn−1 ≺kn dn = d (the P chain is
n
finite as (D, v) is finitary), define the norm of d along σ by kdkσ = i=1 ki .
Since (D, v) is a prime algebraic Scott domain and m respects ∼, the value of
kdkσ does not depend on σ. Therefore, we shall use kdk to denote the norm of a
finite element d. For a non-finite element d ∈ D, its norm is defined as follows:
kdk = sup{kd0 k | d0 ∈ ↓d ∩ C(D)}. A marked domain (D, v, m) is said to be
linear if for any d ∈ D such that kdk < ∞, (↑1 d, v1 ) ∼ = (N, ≤); regular if for any
d, d0 ∈ D, d ↑ d0 ⇒ ∀d1 ∈ ↑1 d, ∀d01 ∈ ↑1 d0 (d1 ↑ d01 ).
It is not difficult to see that linear regular marked domains, together with the
additive stable mappings [10] preserving 40 and ≺1 , form the category MDom.
As shown in [9], marked Scott domains are related with timed event struc-
tures via a pair of functors tpes.mdom : TPES → MDom and mdom.tpes :
MDom → TPES defined as follows4 .
For a timed event structure T E = (E, ≤, #, ∆), let tpes.mdom(T E) be
(TConf(T E), −→, mT E ), where
0, if C 0 \ C = {e} ∧ τ 0 = τ,
m( (C, τ ), (C 0 , τ 0 ) ) =
1, if C 0 = C ∧ τ 0 = τ + 1.
For a marked Scott domain M D = (D, v, m) ∈ MDom, define
mdom.tpes(M D) to be (E, ≤, #, ∆), where E = P 0 (D), p ≤ p0 ⇐⇒ p v p,
p # p0 ⇐⇒ p 6↑ p0 , and ∆(p) = kpk.
4
We do not specify how tpes.mdom and mdom.tpes act on morphisms since it is not
essential to this paper.
A Domain View of Timed Behaviors 119
Theorem 3. [9]. The functors tpes.mdom and mdom.tpes constitute an equiv-
alence between the categories TPES and MDom.
Theorems 1, 2 and 3 yield the following corollary.
Theorem 4. The functor ,→ ◦tpes.totsi ◦ mdom.tpes : MDom → TTSI is
left adjoint to the functor tpes.mdom ◦ totsi .tpes ◦ ttsi .totsi : TTSI → MDom.
Moreover, this adjunction is a coreflection.
5 Direct Characterization
In this section, we establish some relationships between timed transition systems
with independence and marked Scott domains in a direct way.
We start with introducing auxiliary notations. For a transition system with
independence T I = (S, sI , L, T ran, I) and computations π, π 0 ∈ Comp0 (T I), we
write π E π 0 iff there exists a path π 00 such that ππ 00 ' π 0 :
;•\
π 00
•P ' π0
π
sI
For possibly infinite computations π, π 0 ∈ Comp(T I), let π E π 0 iff for every
finite prefix π̄ of π there exists a finite prefix π̄ 0 of π 0 such that π̄ E π̄. It
is straightforward to check that E is a partial order on Comp(T I). Specify a
partial order on timed computations as follows: Π = (π, τ ) Eτ Π 0 = (π 0 , τ 0 ) iff
π E π 0 ∧ τ ≤ τ 0 . Define a partial order v on the 'τ -equivalence classes of timed
computations as follows: [Π]τ v [Π 0 ]τ iff Π Eτ Π 0 .
Lemma 4. (TComp'τ (T T I), v) is a finitary ω-algebraic dcpo. Moreover,
C((TComp'τ (T T I), v)) = TComp0'τ (T T I).
In order to directly relate timed transition systems with independence and
0
marked Scott domains, we construct a mapping ttsi .mdom : TTSI → MDom.
Before doing so, consider a prime interval [Π = (π, τ )]τ , [Π 0 = (π 0 , τ 0 )]τ in
(TComp'τ (T T I), v). It is not difficult to check that either π 0 ' π ∧τ 0 = τ +1 or
π 0 ' πt ∧ τ 0 = τ for some transition t. Define a map mT T I : I((TComp'τ (T T I),
v)) → {0, 1} as follows:
0, if τ = τ 0 ,
mT T I ( [Π]τ , [Π 0 ]τ ) =
1, otherwise.
Let ttsi .mdom 0 (T T I) = (TComp'τ (T T I), v, mT T I ), for any timed transition
system with independence T T I.
120 R. Dubtsov, E. Oshevskaya, I. Virbitskaite
Proposition 2. ttsi .mdom 0 can be extended to a functor ttsi .mdom 0 : TTSI →
MDom isomorphic to ttsi .mdom = tpes.mdom ◦ ottsi .tpes ◦ ttsi .ottsi .
At last, we are ready to state the fact which is the last main result of this
paper and that provides a direct characterisation.
Theorem 5. ttsi .mdom 0 is right adjoint to mdom.ttsi = tpes.mdom ◦ottsi .tpes ◦
ttsi .ottsi . Moreover, this adjunction is a coreflection.
6 Conclusion
We have defined and studied a timed extension of a well-known ”true concurrent”
model of transition systems with independence and have shown that there exists
a chain of coreflections between a category of the model and a category of marked
Scott domains as well as a direct translation. The diagram below summarises
the established relationships:
ttsi.totsi / totsi.tpes
/
TTSI o > ? _ ToTSI o > TPES
tpes.totsi ?
_
s
tt
pe
si > .t
.t
.m
m
m
m
do
∼=
do
do ⊥ om
do
m
m
m
.m
tt
si
es
ts
.m
tp
i
d
) MDom
0
References
1. Bednarczyk, M.: Categories of asynchronous systems. PhD thesis, University of
Sussex, UK (1987)
2. Shields, M.: Concurrent Machines. The Computer Journal 28(5) (1985) 449–465
3. Sassone, V., Nielsen, M., Winskel, G.: Models for concurrency: towards a classifi-
cation. Theoretical Computer Science 170(1-2) (1996) 297–348
4. McLane, S.: Categories for the working mathematician. Graduate Texts in Math-
ematics. Springer, Berlin (1971)
5. Hildebrandt, T., Sassone, V.: Comparing Transition Systems with Independence
and Asynchronous Transition Systems. International Conference on Concurrency
Theory (1996) 84–97
6. Hildebrandt, T., Sassone, V.: Transition Systems with Independence and Multi-
Arcs. BRICS Report Series RS-97-10, BRICS, Department of Computer Science,
University of Aarhus, April (1997)
7. Alur, R., Dill, D.: A theory of timed automat. Theoretical computer science 126(2)
(1994) 183–235
8. Henzinger, T., Manna, Z., Pnueli, A.: Timed transition systems. In: Real-Time:
Theory in Practice, Springer (1992) 226–251
A Domain View of Timed Behaviors 121
9. Virbitskaite, I.B., Dubtsov, R.S.: Semantic domains of timed event structures.
Programming and Computer Software 34(3) (2008) 125–137
10. Winskel, G.: Event structures. Lecture Notes in Computer Science 255 (1987)
325–392
Appendix A: Elements of Category Theory
Here we briefly recall notions from category theory [4] important to this paper.
Let G : B → A be a functor between categories A and B, and let, for each object
A of A, there exist an object F (A) of B and a morphism ηA : A → G ◦ F (A) in
A that is universal in the following sense: for any morphism h : A → G(B) in
A, where B is an object of B, there exists a unique morphism h0 : F (A) → B
in B such that G(h0 ) ◦ ηA = h; i.e., the following diagram commutes.
A F (A) A
ηA
/ G ◦ F (A)
∀h ∃!h0 h
w G(h0 )
G(B) B G(B)
In this case, we say that there exists an adjunction from A to B, and the family
of morphisms {ηA | A ∈ A} is said to be a unit of this adjunction. Then, F can
be extended to a functor by assuming that, for any morphism h : A → A0 in A,
F (h) : F (A) → F (A0 ) is a unique morphism in B such that G ◦F (h)◦ηA = ηA0 ◦h.
In this case, F is said to be left adjoint to G (denoted as F ` G), and G right
adjoint to F (denoted as G a F ). In addition, if ηA is an isomorphism for
each A, then the adjunction is called a coreflection. Categories A and B are
equivalent if F is adjoint to G and both the unit and counit of the adjunction
are isomorphisms.