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 core ections leading from a category of the model of timed transition systems with independence to a category of a specially de ned model of marked Scott domains. As an intermediate semantics we use a model of timed event structures, able to properly capture causality, con ict, and concurrency among events which arise in the presence of time delays of the events.
The behaviour of concurrent systems is often speci ed 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
[
Category theory [
It is generally acknowledged that time plays an important role in many
concurrent and distributed systems. This has motivated the lifting of the theory
of untimed systems to the real-time setting. Timed transition system like
models have been studied thoroughly within the two last decades (see [
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 core ections leading from a category of the model of timed transition systems with independence to a category of a specially de ned model of marked Scott domains. As an intermediate semantics we use a model of timed event structures, able to properly capture causality, concurrency, and con ict 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
independence 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 de nes a core ection. Section 3 establishes the
interrelations in terms of the existence of a core ection 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 [
In this section, we rst 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 2 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 irre exive, symmetric independence relation, such that, using to denote the following relation on transitions (s; a; s0) (s00; a; u) () 9(s; b; s00); (s0; b; u) 2 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) ) 9(s0; b; u); (s00; a; u) 2 T ran
(s; b; s00) I (s00; a; u), 3. (s; a; s0) I (s0; b; u) ) 9(s; b; s00); (s00; a; u) 2 T ran
(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). (s; a; s0) I (s0; b; u) ^ (s; a; s0) I (s; b; s00) ^ Let Diama;b(s; s0; s00; u) () 9(s; a; s0); (s; b; s00); (s0; b; u); (s00; a; u) 2 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 2 T ran as [t].
A transition system with independence functions by executing transitions from one state to another. A possibly in nite sequence = t0 t1 : : : with ti = (si; ai; si+1) 2 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 nite path. A computation is a path such that dom( ) = sI . Let Comp(T I) (Comp0(T I)) be the set of all ( nite) computations of T I. A transition t is said to be reachable, if there exists a computation 2 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
independence. By analogy with the paper [
Let N be the set of non-negative integers.
De nition 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 transition system with independence, and : T ran ! N is the delay function such that (t) = (t0) for any t; t0 2 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 = ( ; ) 2 (Comp((S; sI ; L; T ran; I)) (N [ f1g)) with ( ) = supf (t) j t 2 g. De ne dom( ) = dom( ) and cod( ) = cod( ). We denote the set of all ( nite) timed computations of T T I as TComp(T T I) (TComp0(T T I)), and write ' 0 i ' 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 ( nite) timed computations of T T I.
For timed transition systems with independence T T I = (S; sI ; L; T ran; I; ) and T T I0 = (S0; s0I ; L0; T ran0; I0; 0), a morphism h : T T I ! T T I0 is a pair of mappings h = ( : S ! S0; : L ! L0)3 such that: 1. (sI ) = s0I , 2. (s; a; s0) 2 T ran
(s0), otherwise, 3. (s; a; s0)I(s; a; s0) and a; a 2 dom 4. 0(( (s); (a); (s0))) ((s; a; s0)).
) ( (s); (a); (s0) 2 T ran0 if a 2 dom , and (s) = ) ( (s); (a); (s0)I0( (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 de ned in a componentwise manner.
We next aim at unfolding of timed transition systems with independence. To that end, we rst de ne a subclass of timed transition systems with independence 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 de nes a core ection.
De nition 2. A timed occurrence transition system with independence T 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) 2 T ran ) 9s 2 S s.t. Diama;b(s; s0; s00; u), for all (s00; a; u); (s0; b; u) 2 T ran.
Let ToTSI be the full subcategory of the category TTSI.
De ne 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' = f[ = ( ; ( ))] 2 TComp0' (T T I)g, { ([ = ( ; ( ))] ; a; [ 0 = ( 0; ( 0))] ) 2 T ran'
T ran 0 ' ( t ; 0 ; maxf ( ); ( 0)g), { ([ ] ; a; [ 0] )I' ([ ] ; b; [ 0] ) () t ; 0 It ; 0 , { ' ([ ] ; a; [ 0] ) = (t ; 0 ). () 9t ; 0 = (s; a; s0) 2 Lemma 1. Given a timed transition system with independence ttsi :totsi (T T I) is a timed occurrence transition system with independence. T T I, 3 A partial mapping from a set A into a set B is denoted as f : A ! B. Let dom f = fa 2 A j f (a) is de nedg. For a subset A0 A, de ne f A0 = ff (a0) j a0 2 A0 \ dom f g.
In order to demonstrate that the mapping ttsi :totsi is adjoint to the inclusion functor ToTSI ,! TTSI, we de ne 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 [ ] 2 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 core ection. 3
In this section we relate timed occurrence transition systems with independence and timed event structures, establishing the close relationships between categories of the models.
We start with the de nition 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 = fe0 2 E j e0 eg is a nite set for each e 2 E, # E E is the symmetric irre exive con ict relation such that e # e0 e00 ) e # e00. A set of events C E is said to be a con guration of an event structure E if 8e 2 C #e C, and 8e; e0 2 C :(e # e0). We say that events e; e0 2 E are concurrent and write e ^ e0 if :(e e0 _ e0 e0 _ e # e0). Introduce the concept of a re exive con ict as follows: e __ e0 () e # e0 _ e = e0.
We now recall the de nition of timed event structures from [
De nition 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 con guration of T E is a pair (C; ), where C is a con guration of (E; ; #) and 2 N [ f1g such that (C) = supf (e) j e 2 Cg. The set of all ( nite) timed con gurations of a timed event structure T E is denoted as TConf(T E ) (TConf0(T E )). We de ne a transition relation ! on the set TConf(T E ) as follows: (C; t) ! (C0; t0) if C C0 and t t0. Clearly, the relation ! speci es a partial order on the set TConf(T E ).
Let T E = (E; ; #; ) and T E 0 = (E0; 0; #0; 0) be timed event structures. A partial mapping : E ! E0 is a morphism if # (e) #e; (e) __ (e0) ) e __ e0, for all e; e0 2 dom ; 0( (e)) (e), for all e 2 dom . Timed event structures with their morphisms de ne 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 rst de ne a mapping tpes:totsi : TPES ! ToTSI extending the
mapping pes:otsi from [
() e ^ e; It is easy to see that the above de nition 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 = f[t] j t 2 T rang, { [t] < [t0] ()
8( t0; ) 2 TComp0(T oT I) t0 t0 ) (9t 2 t { [t] # [t0] ()
8( ; ) 2 TComp0(T oT I), 8t 2 [t], 8t0 2 [t0] t 2 { ([t]) = maxf (t0) j [t0] [t]g. t);
=< [ =, ) t0 2= ,
On morphisms h = ( ; ) : T oT I ! T oT I0 in ToTSI, the mapping totsi :tpes acts as follows: totsi :tpes(h) = , where ([(s; a; s0)]) = [( (s); (a); (s0)], if a 2 dom , and ([(s; a; s0)]) is unde ned, otherwise.
Proposition 1. totsi :tpes : ToTSI ! TPES is a functor.
Finally, we de ne 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 [ feg; (C [ feg))]: 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 morphism : 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 .
The next theorem establishes the existence of a core ection 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 core ection. 4
In this section, we extend the established chain of core ections to marked Scott domains. To that end, we rst recall related notions and notations.
Let (D; v) be a partial order, d 2 D and X D. Then, { "d = fd0 2 D j d v d0g is an upper cone of element d, #d = fd0 2 D j d0 v dg is a lower cone of element d, { X is downward (upward) closed if #d X ("d X) for every d 2 X, { X is a compatible set (denoted as X"), if the following assertion is true: 9d 2 D8x 2 X x v d, i.e., X has an upper bound. If X = fx; yg, we write x " y instead of fx; yg". The least upper bound of the set X is denoted as F X (if it exists), and the greatest lower bound is denoted as d 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 nitely compatible set if any nite subset of it X0 X is compatible. { X is a (upper) directed set if any nite subset of it X0 X has an upper bound belonging to the set X (thus, X is a nitely compatible and nonempty set). { (D; v) is a directed-complete partial order (dcpo for short) if every directed subset X D has F X. { d is a nite (compact) element of a dcpo (D; v) if, for any directed subset X D, the following assertion is true: d v F X ) 9x 2 X d v x. The set of nite elements is denoted as C(D). { A dcpo (D; v) is said to be algebraic if, for any d 2 D, d = Ffe v d j e 2
C(D)g. It is said to be !-algebraic if C(D) is countable. { (D; v) is a consistently complete partial order (ccpo) if any nitely compatible subset X D has F X. Clearly, a ccpo has the least element ? = F ;, and is also a dcpo. { An !-algebraic ccpo is called a Scott domain. A Scott domain (D; v) is said to be nitary if #d is nite for every d 2 C(D).
Describe some properties of Scott domains. An element p of a Scott domain (D; v) is said to be prime if, for any compatible subset X D p v F X ) 9x 2 X p v x. The set of the prime elements is denoted as P (D). A Scott domain (D; v) is called prime algebraic if, for any d 2 D, d = Ffp v d j p 2 P (D)g and coherent if all subsets X D satisfying the condition 8d0; d00 2 X d0 " d00 have F X.
Let (D; v) be a Scott domain and = @ n @2 be a covering relation. For elements d; d0 2 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 de ned 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 de nition of marked Scott domains. Informally, a marked Scott domain is meant to be a prime algebraic, nitary, 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.
De nition 4. A marked domain is a triple (D; v; m), where (D; v) is a prime algebraic, nitary, and coherent Scott domain and m : I(D) ! f0; 1g is a marking such that [c; c0] [d; d0] ) m([c; c0]) = m([d; d0]).
Introduce auxiliary notions and notations. For d; d0 2 D and i 2 f0; 1g, we write d i d0, if d d0 ^ m([d; d0]) = i, and d 4i d0, if d i d0 _ d = d0; vi= ( i) ; #id = fd0 j d0 vi dg, and "id = fd0 j d vi d0g; P i(D) = fp 2 P (D) j 9d 2 D m([d; p]) = ig. For a nite element d 2 D and a covering chain having the form ? = d0 k1 d1 dn 1 kn dn = d (the chain is nite as (D; v) is nitary), de ne the norm of d along by kdk = Pin=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 nite element d. For a non- nite element d 2 D, its norm is de ned as follows: kdk = supfkd0k j d0 2 #d \ C(D)g. A marked domain (D; v; m) is said to be linear if for any d 2 D such that kdk < 1, ("1d; v1) = (N; ); regular if for any d; d0 2 D, d " d0 ) 8d1 2 "1d; 8d01 2 "1d0 (d1 " d01).
It is not di cult to see that linear regular marked domains, together with the
additive stable mappings [
As shown in [
For a timed event structure T E = (E; ; #; ), let tpes:mdom(T E ) be (TConf(T E ); !; mT E ), where m( (C; ); (C0; 0) ) = 0; if C0 n C = feg ^ 0 = ; 1; if C0 = C ^ 0 = + 1:
For a marked Scott domain M D = (D; v; m) mdom:tpes(M D) to be (E; ; #; ), where E = P 0(D), p p # p0 () p 6" p0, and (p) = kpk. 2
p0 () p v p,
4 We do not specify how tpes:mdom and mdom:tpes act on morphisms since it is not
essential to this paper.
Theorem 3. [
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 core ection. 5
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 2 Comp0(T I), we write E 0 i there exists a path 00 such that 00 ' 0: 00 P ; \ ' sI 0 For possibly in nite computations ; 0 2 Comp(T I), let E 0 i for every nite pre x of there exists a nite pre x 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) i
E 0 ^ 0. De ne a partial order v on the ' -equivalence classes of timed computations as follows: [ ] v [ 0] i E 0.
Lemma 4. (TComp' (T T I); v) is a nitary !-algebraic dcpo. Moreover,
C((TComp' (T T I); v)) = TComp0' (T T I):
In order to directly relate timed transition systems with independence and marked Scott domains, we construct a mapping ttsi :mdom0 : TTSI ! MDom. Before doing so, consider a prime interval [ = ( ; )] ; [ 0 = ( 0; 0)] in (TComp' (T T I); v). It is not di cult to check that either 0 ' ^ 0 = + 1 or 0 ' t ^ 0 = for some transition t. De ne a map mT T I : I((TComp' (T T I); v)) ! f0; 1g as follows: mT T I ( [ ] ; [ 0] ) = 0; if = 0; 1; otherwise.
Let ttsi :mdom0(T T I) = (TComp' (T T I); v; mT T I ), for any timed transition system with independence T T I. Proposition 2. ttsi :mdom0 can be extended to a functor ttsi :mdom0 : 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 :mdom0 is right adjoint to mdom:ttsi = tpes:mdom ottsi :tpes ttsi :ottsi . Moreover, this adjunction is a core ection. 6
We have de ned 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 core ections 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 o ttsi:>totsi /? _ ToTSI o _
m ttsi:m ttsi:md?odmom0>:ttsidom )
MDom totsi:tpes
> tpes:totsi / TPES
? :tpes m do = m tpes:m dom
Here we brie y recall notions from category theory [
B
A