Nonsequential Automata Semantics for a Concurrent, Object-Based Language

Electronic Notes in Theoretical Computer Science 14 (1998)

URL: http://www.elsevier.nl/locate/entcs/volume14.html

29 pages

Nonsequential Automata Semantics for a Concurrent, Object-Based Language P. Blauth Menezes 1 Departamento de Informatica Teorica, Instituto de Informatica Universidade Federal do Rio Grande do Sul Caixa Postal 15064, 91501-970, Porto Alegre, Brazil Email: [email protected]

A. Sernadas 1 Departamento de Matematica, Instituto Superior Tecnico, Universidade Tecnica de Lisboa Av. Rovisco Pais, 1096 Lisboa Codex, Portugal Email: [email protected]

J. Felix Costa 1 Departamento de Informatica, Faculdade de Ci^encias, Universidade de Lisboa Campo Grande, 1700 Lisboa, Portugal Email: [email protected]

Abstract

Nonsequential automata constitute a categorial semantic domain based on labeled transition system with full concurrency, where restriction and relabeling are functorial and a class of morphisms stands for rei cation. It is a model for concurrency which satis es the diagonal compositionality requirement, i.e., rei cations compose (vertically) and distribute over combinators (horizontally). To experiment with the proposed semantic domain, a semantics for a concurrent, object-based language is given. It is a simpli ed and revised version of the object-oriented speci cation language GNOME, introducing some special features inspired by the semantic domain such as rei cation and aggregation. The diagonal compositionality is an essential property to give semantics in this context. This work is partially supported by: FAPERGS (Project Qap-For) and CNPq (Project GRAPHIT), in Brazil; PRAXIS XXI Projects 2/2.1/MAT/262/94 SitCalc, as well as by PRAXIS XXI Projects 2/2.1/MAT/262/94 SitCalc, PCEX/P/MAT/46/96 ACL plus

1

c

1998 Published by Elsevier Science B. V.

Menezes, Sernadas & Costa

1 Introduction We construct a semantic domain with full concurrency which satis es the diagonal compositionality requirement, i.e., rei cations compose (vertically), re ecting the stepwise description of systems, involving several levels of abstraction, and distributes through combinators (horizontally), meaning that the rei cation of a composite system is the composition of the rei cation of its parts. Taking into consideration the developments in Petri net theory (mainly with seminal papers like [29,18,21]) it was clear that nets might be good candidates. However, most of net-based models such as Petri nets in the sense of [20] and labeled transition systems (see [19]) lack composition operations (modularity) and abstraction mechanisms in their original de nitions. This motivate the use of the category theory: the approach in [29] provides the former, where categorical constructions such as product and coproduct stand for system composition, and the approach in [18] provides the later for Petri nets where a special kind of net morphism corresponds to the notion of implementation. Also, category theory provides powerful techniques to unify dierent categories of models (i.e., classes of models categorically structured) through adjunctions (usually re ections and core ections) expressing the relation of their semantics as in [21], where a formal framework for classi cation of models for concurrency is set. A nonsequential automaton ( rst introduced in [13]) is a kind of automaton with monoidal structure on states and transitions, inspired by [18]. Structured states are "bags" of local states like tokens in Petri nets (as in [20]) and structured transitions specify a concurrency relationship between component transitions in the sense of [2,11]. The resulting category is bicomplete where the categorial product stands for parallel composition. A rei cation maps Categories cN2

c a

Automata N1

N2

tcN2

Fig. 1. Transitive closure and transitions mapped into transactions

transitions into transactions re ecting an implementation of an automaton on top of another. It is de ned as an automaton morphism where the target 2/2.1/TIT/1658/95 LogComp, and ESPRIT IV Working Groups 22704 ASPIRE and 23531 FIREworks in Portugal

2

Menezes, Sernadas & Costa object is enriched with all conceivable sequential and nonsequential computations that can be split into permutations of original transitions, respecting source and target states. Computations are induced by an adjunction between a category of categories and the category of nonsequential automata, as illustrated in the Figure 1, where tc is the composition of nc followed by cn. The composition of two rei cations ': N !tcN and : N !tcN where the target of ' is dierent from the source of , is inspired by Kleisli categories, as illustrated in the Figure 2. Therefore, the vertical compositionality requirement is achieved. Moreover we nd a general theory of rei cation of systems which also satis es the horizontal compositionality requirement. i.e., for rei cations ': N !tcM , : N !tcM , we have that: 1

1

1

2

2

3

2

'N  N = ' (N N ) 1

2

1

2

where 'N  N and N N are parallel compositions and the rei cation morphism ' is induced by ' and . Restriction and relabeling are func1

2

1

2

o

N1

tcN3 flattening

tcN2

tc

tc2N3

Fig. 2. Composition of rei cation morphisms

torial operations de ned using bration and co bration techniques based on [14] and inspired by [29]. Both functors are induced by morphisms at the label level. A restriction restricts the transitions of an automaton according to some table of restrictions (of labels). A relabeling relabels the transitions of an automaton according to some morphism of labels. Synchronization u-1 Table

sync Ni

syncNi

(forgetful functor)

Automata u-1 Li

Labels

u synchronization morphism Table

Li

Fig. 3. Induced synchronization functor

and encapsulation of nonsequential automata are special cases of restriction and relabeling, respectively. A synchronization restricts a parallel composition according to some table of synchronizations (at label level), as illustrated in the Figure 3, where N i and syncN i denote the parallel composition and the 3

Menezes, Sernadas & Costa synchronized automaton, respectively, and sync is the induced synchronization functor (between subcategories of nonsequential automata). The synchronization of a rei ed automata is the synchronization of the source automata whose rei cation is induced by component rei cations. In this construction, the horizontal compositionality is an essential property. An important result is that the horizontal compositionality requirement is extended for synchronization. A view of an automaton is obtained through hiding of transitions introducing an internal nondeterminism. A hidden transition cannot be used for synchronization. The hiding of a rei cation is induced by the hiding of the source automaton. Categories of Petri nets and categories of nonsequential automata can be uni ed through adjunctions. In [13] and [15]) we show that nonsequential automata are more concrete than Petri nets (in fact, categories of Petri nets are isomorphic to subcategories of nonsequential automata) extending the approach in [21]. Also, we show that Petri nets do not satisfy the diagonal compositionality, i.e., nonsequential automata is the least concrete model for concurrency (among considered models) which satisfy this requirement. To experiment with the proposed semantic domain, a semantics for a concurrent object-based speci cation language (using the terminology of [28]) is given. The language named Nautilus is based on the object-oriented language GNOME [23] which is a simpli ed and revised version of OBLOG [26,25,24]. It is a high level speci cation language for concurrent, communicating systems. Some features inspired by the semantic domain (and not present on GNOME) such as rei cation and aggregation are introduced. Also, the state-dependent calling of GNOME is generalized for interaction, aggregation and rei cation in Nautilus. For simplicity and in order to keep the paper short, we do not deal with some feature of GNOME such as classes of objects and inheritance. The main features of Nautilus are the following:  objects may interact through callings;  an object may be the aggregation of component objects;  an object may be rei ed into a sequential or parallel computations of another object;  an object may be a view of another object;  interaction, aggregation and rei cation may be state-dependent, i.e., may depend dynamically on some conditions;  interaction, aggregation and rei cation are compositional;  the evaluation of an action is atomic;  the clauses of an action may be composed in a sequential or multiple ways. The main dierence between interaction and aggregation is that, in the former, the relationship between objects is de ned within each object while in the later, the relationship is de ned externally to the component objects. A multiple composition is a special composition of concurrent clauses based 4

Menezes, Sernadas & Costa on Dijkstras guarded commands [5] where the valuation clauses are evaluated before the results are assigned to the corresponding slots. A nonsequential automata semantics for Nautilus is easily de ned. Since an action may be a sequential or multiple composition of clauses executed in an atomic way, the semantics of a simple object is given by a rei cation where the target automaton called base is determined by the computations of a freely generated automaton able to simulate any object speci ed over the involved attributes and the source automaton is a relabeled restriction of the base. Therefore, the semantics of an action in Nautilus is a nonsequential automaton transition (and thus is atomic) rei ed into a (possible complex) computation. The semantics of a rei cation is the composition of semantics, i.e., the rei cation of the source automata over the target composed with the rei cation of the target over its base. The semantics of an interaction, aggregation and encapsulation in Nautilus are straightforward since they are given by synchronization and encapsulation of rei cation morphisms of nonsequential automata (an aggregation also de nes a relabeling). An action with inputs or outputs is associated to a family of transitions indexed by the corresponding values. The semantics of a community of concurrent objects is the parallel composition of the semantics of component objects, i.e., the parallel composition of rei cations. In the proposed approach, the diagonal compositionality is an essential property as follows:  for the semantics of a rei cation, the vertical compositionality is essential;  for the semantics of an interaction, aggregation and a community of concurrent objects, the horizontal compositionality is essential. With respect to previous works as in [17], in this paper we introduce the synchronization and encapsulation of rei ed automata and we extend the language Nautilus with the features of interaction and aggregation which are compositional with respect to the object rei cation.

2 Nonsequential Automata A nonsequential automaton is a re exive graph labeled on arcs such that nodes, arcs and labels are elements of commutative monoids. A re exive graph represents the shape of an automaton where nodes and arcs stand for states and transitions, respectively, with identity arcs interpreted as idle transitions. A structured transition specify a concurrency relation between component transitions. A structured state can be viewed as a "bag" of local states where each local state can be viewed as a resource to be consumed or produced, like a token in Petri nets. 5

Menezes, Sernadas & Costa 2.1 Category of Nonsequential Automata Nonsequential automata and its morphisms constitute a category which is complete and cocomplete with products isomorphic to coproducts. A product (or coproduct) can be viewed as the parallel composition. In what follows CMon denotes the category of commutative monoids and suppose that i2I whereI is a set and k2f0, 1g (for simplicity, we omit that i2I and k2f0, 1g). De nition 2.1 (Nonsequential Automaton) A nonsequential automaton N = (V, T, 0, 1, , L, lab) is such that T = (T , ,  ), V = (V , , e), L = (L, ,  ) are CMon-objects of transitions, states and labels respectively, 0, 1: T!V are CMon-morphisms called source and target respectively, : V!T is a CMon-morphism such that k  = idV and lab: T!L is a CMonmorphism such that lab(t) =  whenever there is v 2V where (v) = t. We may refer to a nonsequential automaton N = (V, T, 0 , 1, , L, lab) by N = (G, L, lab) where G = (V, T, 0, 1, ) is a re exive graph internal to CMon (i.e., V, T are CMon-objects and 0, 1 ,  are CMon-morphisms) representing the shape of N . In an automaton, a transition labeled by  represents a hidden transition (and therefore, can not be triggered from the outside). Note that, all idle transitions are hidden. The labeling procedure is not extensional in the sense that two distinct transitions with the same label may have the same source and target states (as we will se later, it is an essential property to give semantics for an object rei cation in Nautilus). For simplicity, in this paper we are not concerned with initial states. A transition t such that 0(t) = X , 1(t) = Y is denoted by t: X !Y . Since a state is an element of a monoid, it may be denoted as a formal sum n1A1: : :nmAm , with the order of the terms being immaterial, where Ai2V and ni indicate the multiplicity of the corresponding (local) state, for i = 1: : :m. The denotation of a transition is analogous. We also refer to a structured transition as the parallel composition of component transitions. When no confusion is possible, a structured transition x  : X A!Y A where t: X !Y and A: A!A are labeled by x and  , respectively, is denoted by x: X A!Y A. For simplicity, in graphical representation, we omit the identity transitions. States and labeled transitions are graphically represented as circles and boxes, respectively. Example 2.2 Let (fA, B , X , Y g, ft1 , t2, t3, A, B , C , X , Y g , 0, 1, , fx, yg , lab) be a nonsequential automaton with 0 , 1 determined by the local arcs t1 : 2A!B , t2 : X !Y , t3 : Y !X and lab determined by t1 7!x, t2 7!x, t3 7!y. The distributed and in nite schema in Figure 4 (left) represents the automaton. Since in this framework we do not deal with initial states, the graphical representation makes explicit all possible states that can be reached by all possible independent combination of component transitions. For instance, if we consider the initial state A2X , only the corresponding part of the schema of the automata in the gure has to be considered. In Figure 4 (right), we illustrate a labeled Petri net which simulates the behavior of 6

Menezes, Sernadas & Costa the automaton. Comparing both schema, we realize that, while the concurrence and possible reachable markings are implicit in a net, they are explicit in an automaton. Also, comparing with asynchronous transition systems ( rst introduced in [2]), the independence relation of a nonsequential automaton is explicit in the graphical representation. 2A

X

x

2A X

x

3A

A

X

2

x

B

x

y

B X

Y

y

x x

y

2A Y

x

x

B Y

x

x y

A B

...

x

x

y

B

Y

Fig. 4. A nonsequential automaton (left) and the corresponding labeled Petri net (right)

De nition 2.3 (Nonsequential Automaton Morphism) A nonsequential automaton morphism h: N !N where N = (V , T ,  ,  ,  , L , lab ) and N 2 = (V2 , T2 ,  0 2 ,  1 2 , 2 , L2 , lab2 ) is a triple h = (hV , hT , hL) such that hV : V1 !V2 , hT : T1 !T2 , hL : L1 !L2 are CMon-morphisms, hV  k 1 =  k 2 hT , hT 1 = 2 hV and hL lab1 = lab2 hT . Nonsequential automata and their morphisms constitute the category NAut. Proposition 2.4 The category NAut is bicomplete with products isomorphic to coproducts. Proof. The category RGr(CMon) of shapes of automata is the category of re exive graphs internal to CMon where the properties about limits and colimits are inherited from CMon. Thus, RGr(CMon) is bicomplete with products isomorphic to coproducts. NAut can be de ned as the comma category id#inc where id: RGr(CMon)!RGr(CMon) is the identity functor and inc: CMon!RGr(CMon) takes each monoid into its corresponding one node graph. Since inc preserves limits (and id trivially preserves colimits), NAut is bicomplete with products isomorphic to coproducts. 2 The above proof justify the notation N = (G, L, lab) introduced previously for an automaton N = (V, T, 0 , 1 , , L, lab). A categorical product of two automata N 1NAutN 2 where N 1 = (V1, T1, 01 , 1 1 , 1, L1 , lab1 ) and N 2 = (V2 , T2 , 0 2 , 12 , 2 , L2 , lab2 ) is: 1

2

1

1

1

01

11

1

1

1

(V CMonV ; T CMonT ;  1  2 ;  1  2 ;   ; L CMonL ; lab lab ) 1

2

1

2

0

0

1

1

1

2

1

2

1

2

where k 1 k 2 ,   and lab lab are uniquely induced by the product construction. Example 2.5 Consider the nonsequential automata Consumer and Producer 7 1

2

1

2

Menezes, Sernadas & Costa (with free monoids) determined by the labeled transitions prod: A!B , send: B !A for the Producer and rec: X !Y , cons: Y !X for the Consumer. Then, the resulting object of the parallel composition ConsumerProducer is illustrated in the Figure 5 (for simplicity, prod, send, rec and consare abbreviated by p, s, r and c, respectively). p

r A X

A p

X s

B

r

s c

Y

p r

p c

B X r

c

...

A Y s r

s c

p

B Y c

s

Fig. 5. Parallel composition of nonsequential automata

2.2 Restriction and Relabeling Restriction and relabeling of transitions are functorial operations de ned using the bration and co bration techniques. Both functors are induced by morphisms at the label level. The restriction operation restricts an automaton "erasing" all those transitions which do not re ect some given table of restrictions: (i) let N be a NAut-object with L as the CMon-object of labels, Table be a CMon-object called table of restrictions and restr: Table!L be a restriction morphism. Let u:NAut!CMon be the obvious forgetful functor taking each automaton onto its labels; (ii) the functor u is a bration and the bers u?1 Table and u?1L are subcategories of NAut. The bration u and the morphism restr induce a functor between bers restr: u?1L!u?1Table. The functor restr applied to N provides the automaton re ecting the desired restrictions. The steps for relabeling are as follows: (i) let N be a NAut-object with L1 as the CMon-object of labels and relab: L1 !L2 be a relabeling morphism. Let u be the same forgetful functor used for synchronization purpose; (ii) the functor u is a co bration (and therefore, a bi bration) and the bers u?1 L1 and u?1 L2 are subcategories of NAut. The co bration u and the 8

Menezes, Sernadas & Costa morphism relab induce a functor relab: u? L !u? L . The functor relab applied to N provides the automaton re ecting the desired relabeling. In what follows, we show that the forgetful functor which takes each nonsequential automaton onto its labels is a bration and then we introduce the restriction functor. Proposition 2.6 The forgetful functor u: NAut!CMon that takes each nonsequential automaton onto its underlying commutative monoid of labels is a bration. Proof. Remember that NAut can be de ned as the comma category id#inc where id: RGr(CMon)!RGr(CMon) and inc: CMon!RGr(CMon) are functors. Let f : L !L be a CMon-morphism and N = (G , L , lab ) be a nonsequential automaton where G = (V , T ,  2 ,  2 ,  ) is a RGr(CMon)object. Let the object G together with lab : G !incL and uG: G !G be the pullback of f : incL !incL and lab : G !incL . De ne N = (G , L , lab ) which is an automaton by construction. Then u = (uG , f ): N !N is cartesian with respect to f and N . 2 De nition 2.7 (Functor restr) Consider the bration u: NAut!CMon, the automata N = (V, T,  ,  , i, L, lab) and the restriction morphism restr: Table!L. The restriction of N is given by the functor restr: u? L!u? Table induced by u and restr applied to N . In what follows, we show that the forgetful functor which takes each nonsequential automaton into its labels is a bration and then we introduce the restriction functor. Proposition 2.8 The forgetful functor u: NAut!CMon that maps each automaton onto its underlying commutative monoid of labels is a co bration. Proof. Let f : L !L be a CMon-morphism and N = (V , T ,  1 ,  1 ,  , L , lab ) be an automaton. De ne N = (V , T ,  1 ,  1 ,  , L , f lab1 ). Then u = (idV 1 , idT 1 , f ): N 1 !N 2 is cocartesian with respect to f and N 1 .2 De nition 2.9 (Functor relab) Consider the bration u: NAut!CMon, the automaton N = (V, T,  ,  , , L , lab) and the relabeling morphism relab: L !L . The relabeling of N satisfying relab is given by the relab: u? L !u? L induced by u and relab applied to N . 1

1

1

1

2

2

2

2

2

1

2

1

1

2

2

0

2

1

2

2

2

1

1

2

1

2

2

1

1

1

1

1

2

2

0

1

1

1

1

2

1

1

2

0

1

1

1

1

1

1

1

1

0

1

1

1

1

1

0

1

2

1

2

2

2.3 Synchronization and Hiding Since the product (or coproduct) construction in NAut stands for parallel composition, re ecting all possible combination between component transitions, it is possible to de ne a synchronization operation using the restriction operation erasing from the parallel composition all those transition which do not re ect some table of synchronizations. For this purpose, we also introduce a categorial way to construct tables of synchronizations for calling and sharing 9

Menezes, Sernadas & Costa (or both) and the corresponding synchronization morphism. The following approach generalizes the one in [16,14] for more than two systems. A table of synchronizations is given by a colimit whose resulting diagram has a shape illustrated in the Figure 6 (left) where the central arrow has as source an object named channel and as target the table of synchronizations. We say that a shares x if and only if a calls x and x calls a. In what follows, we denote by ajx a pair of synchronized transitions. CMon Li' calli

inci Li

Channel

colimit pi

q Table

Fig. 6. Table of synchronizations

De nition 2.10 (Table of Synchronizations) Let fN i g be a set of nonsequential automata with fLi g as the corresponding commutative monoids of

labels, Channel be the least commutative monoid determined by all tuples of transitions to be synchronized, Li' be the least commutative submonoid of Li containing all transitions of N i which call other transitions, calli : Li ' !Channelbe the morphisms such that, for a2Li', if a calls x1,: : :, xn then calli(a) = ajx1j: : :jxn and D be the diagram represented in the Figure 6 (right) where inci: Li ' !Li are inclusion morphisms. The table of synchronizations Table is given by the colimit of D. Example 2.11 Consider the free commutative monoids of labels L1 = fa, b, cg , L2 = fx, yg . Suppose that acalls x, b calls y and y calls b (i.e., b shares y). Then, Channel = fajx, bjyg , L1' = fa, bg , L2' = fyg and Table = fc, x, ajx, bjyg . Let D be a diagram whose colimit determines Table together with pi: Li ! Table. Then there are retractions for pi denoted by piR such that, for every b2Table, if there is a2Li such that p(a) = b then piR (b) = a else piR(b) =  . Let Li together with inj i: Li !Li be the product of fLig where inj i are monomorphisms. De nition 2.12 (Synchronization Morphism) Let s: Channel!Li be a monomorphism that de nes Channel as a subobject of Li. The synchronization morphism sync: Table!Li determined by the diagram D is such that sync( ) =  and for each a6= in Table, if q R (a) 6= , then sync(a) = sq R (a), else there is a unique k such that pk R (a) 6= and sync(a) = inj k pk R (a). Therefore, the restriction functor induced by the synchronization morphism 10

Menezes, Sernadas & Costa

sync is the synchronization functorial operation sync. The functor sync applied to the parallel composition of component automata provides the desired synchronized automaton. Example 2.13 Consider the nonsequential automata Consumer and Producer (with free monoids) determined by the labeled transitions prod: A!B , send: B !A for the Producer and rec: X !Y , cons: Y !X for the Consumer. Suppose that we want a joint behavior sharing the transitions send and rec (a communication without buer such as in CSP [9] or CCS [19]). Then,

Channel = fsendjrecg and Table = fprod, cons, sendjrecg . The resulting automaton is illustrated in the Figure 7. Note that the transitions send, rec are erased and the transition sendjrec is included. A

Y

prod

A X

cons

send rec prod

cons

B X

A Y

...

prod cons B

X

cons

B Y

prod

Fig. 7. Synchronized automaton

For encapsulation purposes, we work with hiding morphisms. A hiding morphism is an injective morphism except for those labels we want to hide (i.e., to relabel by  ). In what follows e denotes a zero object in CMon (any monoid with only one element) and ! denotes the unique morphism with e as source or target. De nition 2.14 (Hiding Morphism) Let L be the commutative monoid of labels of the automata to be encapsulated, L be least commutative submonoid of L containing all labels to be hidden and inc: L!L be the inclusion. Let L together with hide: L !L and q: e!L be the pushout of !: L!e and inc: L!L . Then, the hiding morphism is the morphism hide. Therefore, applying the relabeling functor induced by a hiding morphism to some giving automaton results on its encapsulation. Example 2.15 Consider the resulting automata of the previous example. Suppose that we want to hide the synchronized transition sendjrec. Then, the hiding morphism is induced by sendjrec7! and the encapsulated automaton is as illustrated in the Figure 7 except that the transition sendjrec has its label replaced by  . 11 1

1

1

2

1

1

2

2

Menezes, Sernadas & Costa 2.4 Rei cation

A rei cation is de ned as a special automaton morphism where the target object is closed under computations, i.e., the target (more concrete) automaton is enriched with all the conceivable sequential and nonsequential computations that can be split into permutations of original transitions, respecting source and target states. The category of categories internal to CMon is denoted by Cat(CMon). We introduce the category LCat(CMon) which can be viewed as a generalization of labeling on Cat(CMon). There is a forgetful functor from LCat(CMon) into NAut. This functor has a left adjoint which freely generates a nonsequential automaton into a labeled internal category. The composition of both functors from NAut into LCat(CMon) leads to an endofunctor, called transitive closure. The composition of rei cations of nonsequential automata is inspired by Kleisli categories (see [1]). In fact, the adjunction above induces a monad which de nes a Kleisli category. Then we show that rei cation distributes over the parallel composition and therefore, the resulting category of automata and rei cations satis es the diagonal compositionality. De nition 2.16 (Category LCat(CMon)) Consider the category Cat(CMon). The category LCat(CMon) is the comma category idCat CMon #idCat CMon where idCat CMon is the identity functor in Cat(CMon). Therefore, a LCat(CMon)-object is triple N = (G, L, lab) where G, L are Cat(CMon)-objects and lab is a Cat(CMon)-morphism. Proposition 2.17 The category LCat(CMon) has all (small) products and coproducts. Moreover, products and coproducts are isomorphic. De nition 2.18 (Functor cn) Let N = (G, L, lab) be a LCat(CMon)-object and h = (hG, hH ): N !N be a LCat(CMon)-morphism. The functor cn: LCat(CMon)!NAut is such that: (i) the Cat(CMon)-object G = (V, T,  ,  , , ;) is taken into the RGr(CMon) object G = (V, T',  ',  ', '), where T' is T subject to the equational rule below and  ',  ', ' are induced by  ,  ,  considering the monoid T'; the Cat(CMon)-object L = (V, L,  ,  , , ;) is taken into the CMon-object L', where L' is L subject to the same equational rule; the LCat(CMon)-object N = (G, L, lab) is taken into the NAut-object N = (G, L', lab) where lab is the RGr(CMon)-morphism canonically induced by the Cat(CMon)-morphism lab; (

(

)

(

)

)

1

2

0

0

0

1

1

1

0

1

0

1

t : A!B 2T0 u : B !C 2T0 t0 : A0!B 02T0 u : B 0!C 02T0 (t; u) (t0; u0) = (t t0); (u u0 ) (ii) the LCat(CMon)-morphism h = (hG , hH ): N1 !N2 with hG = (hN V , hN T ), hH = (hLV , hLT ) is taken into the NAut-morphism h = (hN V , hN T , hLT ): N 1!N 2 where hN T and hLT are the monoid morphisms 12 0

0

0

0

Menezes, Sernadas & Costa induced by hN T and hLT , respectively. The functor cn has a requirement about concurrency which is (t;u) (t';u') = (t t');(u u'). That is, the computation determined by two independent composed transitions t;u and t';u' is equivalent to the computation whose steps are the independent transitions t t' and u u'. De nition 2.19 (Functor nc) Let A = (G, L, lab) be a NAut-object and h = (hG, hL): A1 !A2 be a NAut-morphism. The functor nc: NAut!LCat(CMon) is such that: (i) the RGr(CMon)-object G = (V, T,  0 ,  1 , ) with V = (V , , e), T = (T , ,  ) is taken into the Cat(CMon)-object G = (V, Tc,  0 c,  1 c, , ;) with Tc = (T c, ,  ),  0 c,  1 c, -;-: TcTc!Tc inductively de ned as follows: t : A!B 2T t : A!B 2Tc

t : A!B 2Tc u : C !D2Tc t u : AC !B D2Tc

t : A!B 2Tc u : B !C 2Tc t; u : A!B 2Tc subject to the following equational rules:

t2Tc  ; t = t t;  = t

t : A!B 2Tc A; t = t t; A = t

t : A!B 2Tc u : B !C 2Tc v : C !D2Tc t; (u; v) = (t; u); v t2Tc u2Tc t2Tc A2Tc B 2Tc t u = u t t  = t A B =  A B t2Tc u2Tc v2Tc t (u v) = (t u) v the CMon-object L is taken into the Cat(CMon)-object L = (1, Lc, !, !, !, ;) as above; the NAut-object A = (G, L, lab) is taken into the LCat(CMon)-object A = (G, L, lab) where lab is the morphism induced by lab; (ii) the NAut-morphism h = (hV , hT , hL ): A !A is taken into the Cat(CMon)morphism h = (hG , hH ): A !A where hG = (hV , hT c), hH = (!, hL c) and hT c, hL c are the monoid morphisms generated by the monoid morphisms hT and hL, respectively. Proposition 2.20 The functor nc: NAut!LCat(CMon)is left adjoint to cn: LCat(CMon)!NAut. 1

1

Proof.

2

13

2

Menezes, Sernadas & Costa (i) The unity of the adjunction is the natural transformation : idNAut!cnnc where, for each component graph, the transitions are taken into the corresponding transitions of its transitive closure. (ii) Dually, the counity of the adjunction is the natural transformation : nccn!idLCat CMon where, for each component graph, a composed transition (t);(u) or (t) (u) is taken into the corresponding transitions (t;u) or (t u), respectively. Therefore, (nc, cn, , ): NAut!LCat(CMon)is an adjunction. 2 De nition 2.21 (Transitive Closure Functor) The transitive closure functor is: tc = cnnc : NAut!NAut: Example 2.22 Consider the nonsequential automaton with free monoids on states and transitions, determined by the transitions a: A!B and b: B !C . Then, for instance, a; 2b: AB !B C is a transition in the transitive closure. Note that, a; 2b represents a class of transitions. In fact, from the equations we can infer that: (

)

a; 2b = a; (b b) =  [B ] a); (b b) = ( [B ]; b) (a; b) = b (a; b) = (b;  [C ]) ( [A]; (a; b)) = (b  [A]); ( [C ] (a; b)) = b; a; b = : : :: Let (nc, cn, , ): NAut!LCat(CMon) be the adjunction above. Then, T = (tc, , ) is a monad on NAut such that  = cnnc: tc !tc where cn: cn!cn and nc: nc!nc are the identity natural transformations and cnnc is the horizontal composition of natural transformations. For some given automaton N , we have that:  tcN is N enriched with its computations;   N : N !tcN includes N into its computations;  N : tc N !tcN attens computations of computations into computations. A rei cation morphism ' from A into the computations of B could be de ned as a NAut-morphism ': A!tcB . In this case, the composition of rei cations could be as in Kleisli categories (each adjunction induces a monad which de nes a Kleisli category). However, for giving semantics of objects in Nautilus, rei cations should to not preserve labeling (and thus, they are not NAutmorphisms). As we show below, each rei cation induces a NAut-morphism. Therefore, we may de ne a category whose morphisms are NAut-morphisms induced by rei cations. Both categories are isomorphic. De nition 2.23 (Rei cation) Let t = (tc, , ) where  = (G, L),  = (G , L) be the monad induced by (nc, cn, , ): NAut!LCat(CMon). The category of nonsequential automata and rei cations, denoted by ReifNAut, is such that (suppose the NAut-objects N k = (Gk , Lk , labk ), for k2f1, 2, 3g): (i) ReifNAut-objects are the NAut-objects; 14 2

2

Menezes, Sernadas & Costa (ii) ' = 'G : N 1 !N 2 is a ReifNAut-morphism where 'G : G1 !tcG2 is a RGr(CMon)-morphism and for each NAut-object N , ' = G : N !N is the identity morphism of N in ReifNAut; (iii) let ': N 1 !N 2 , : N 2 !N 3 be ReifNAut-morphisms. The composition ' is a morphism GK 'G: N 1!N 3 where GK 'G is as illustrated in the Figure 8. RGr(CMon) G

G1

tc G 2

tc G

G

tc2 G 3

tc G 3

G •K G

Fig. 8. Composition of rei cations is the composition in the Kleisli category forgetting about the labeling

In what follows, an automaton (G, L, lab) may be denoted as a morphism lab: G!incLor just by lab: G!L. De nition 2.24 (Rei cation with Induced Labeling) Let t = (tc, , ) where  = (G,  L ),  = (G , L) be the monad induced by the adjunction (nc, cn, , ). The category of nonsequential automata and rei cations with induced labeling ReifNAutL is such that (suppose the NAut-objects N k = (Gk , Lk , labk ), for k2f1, 2, 3g): (i) ReifNAutL-objects are the NAut-objects; (ii) let 'G : G !tcG be a RGr(CMon)-morphism. Then ' = ('G , 'L ): N !N is a ReifNAutL-morphism where 'L is given by the pushout illustrated in the Figure 9 (left). For each NAut-object N , ' = (G : G!tcG, 'L: L!L): N !N is the identity morphism of N in ReifNAutL where 'L is as above; (iii) let ': N !N , : N !N be ReifNAutL-morphisms. The composition ' is a morphism ( GK 'G, LH 'L ): N !N where GK 'G and L H 'L is as illustrated in the Figure 9 (right). It is easy to prove that ReifNAut and ReifNAutL are isomorphic (we identify both categories by ReifNAut). Thus, every rei cation morphism can be viewed as a NAut-morphism. For a ReifNAut-morphism ': A!B , the corresponding NAut-morphism is denoted by ': A!tcB . Since rei cations constitute a category, the vertical compositionality is achieved. In the following proposition, we show that, for some given rei cation morphisms, the morphism (uniquely) induced by the parallel composition is also a rei cation morphism and thus, the horizontal compositionality is achieved. Proposition 2.25 Let f'i : N i!tcN ig be an indexed family of rei cations. 15 1

1

2

2

1

2

2

3

1

1

2

3

Menezes, Sernadas & Costa RGr(CMon) lab 1

G1

L1

G

G1

lab 1

tc G 2

L1 L

G

tc G 2

G •k G

tc lab2

p.o. tc L2 lab 2,

L2,

L •L L

G

tc2 G 3 G

tc G3

p.o. tc lab 3

tc L3

L3,

•

lab 3, •

Fig. 9. Rei cation with induced labeling Then i'i : i N 1 i !itcN 2i is a rei cation. Proof. Remember that tc = cnnc. Since nc is left adjoint to cn then nc preserves colimits and cn preserves limits. Since products and coproducts are isomorphic in LCat(CMon), tc preserves products. Following this approach,

it is easy to prove that i'i is a rei cation morphism.

2

2.5 Restriction and Relabeling of Rei cations The restriction of a rei cation is the restriction of the source automaton. The restriction of a community of rei cations (i.e., the parallel composition of rei ed automata) is the restriction of the parallel composition of the source automata whose rei cation is induced by the component rei cations. Note that, the proposed approach also de nes synchronization and hiding for rei cations. In the following construction, the horizontal compositionality requirement is essential. Remember that tc preserves products and that every restriction morphism has a cartesian lifting at the automata level. De nition 2.26 (Restriction of a Rei cation) Let ': N 1 !tcN 2 be a rei cation and restrL : Table!L1 be a restriction morphism and restrN : restrN 1 !N 1 be its cartesian lifting. The rei cation of the restricted automaton restrN 1 is restr': restrN 1 !tcN 2 such that restr' = 'restrN . Proposition 2.27 Let f'i : N 1 i!tcN 2 ig be an indexed family of rei cations where N ki = (Gki , Lki , labki ). Let restrL : Table!i L1i be a restriction morphism and restrN : restrN 1i !iN 1 i be its cartesian lifting. The restriction of the parallel composition of component rei cations is restr'i : restrN 1 i !tc(i N 2 i ) such that restr'i = i 'i restrN where i 'i is uniquely induced by the product construction. Proof. Consider the Figure 10 (left). Since the horizontal compositionality requirement is satis ed, the proof is straightforward. 2 16

Menezes, Sernadas & Costa NAut restr N1i

RGr(CMon)

restr N N1i

relab• lab1 G1

i N1i

i

restr i

tc G2 tc ( i N 2 i )

relab L

G

i i

tc N 2 i

L1'

tc lab 2

p.o. tc L2 relab lab 2,

L2, '

Fig. 10. Restriction and relabeling of rei cations

The relabeling of a rei cation is induced by the relabeling of the source automaton. De nition 2.28 (Relabeling of a Rei cation) Consider the Figure 10 (right). Let ': N !tcN be a rei cation where N k = (Gk , Lk , labk ) and ' = ('G , 'L ). Let lab: L !L be a relabeling morphism and relabN = (G , L , relablab ) the relabeled automaton. Then, the relabeling of the rei cation morphism is relab' = ('G, relab'L). 1

2

1

2

1

1

2

1

3 Language Nautilus and its Semantics In this brief introduction to the language Nautilus we introduce some key words in order to help the understanding of the examples below. The speci cation of an object in Nautilus depends on if it is a simple object or the resulting object of an encapsulation (view), aggregation (aggregation), rei cation (over) or a parallel composition. In any case, a speci cation has two main parts: interface and body. The interface declares imported (import only for the simple object) and exported (export) actions and the category (category) of some actions (birth, death, request). The body (body) declares the attributes (slot - only for the simple object) and the methods of all actions. An action (act) may occur spontaneously, under request or both. A birth or death action may occur at most one time and determines the birth or the death of the object. An action may occur if its enabling (enb) condition holds. An action with alternatives (alt) is enabled if at least one alternative is enabled. In this case, only one enabled alternative may occur where the choice is an internal nondeterminism. The evaluation of an action (or an alternative within an action) is atomic. An action may be a sequential (seq/end seq) or multiple (cps/end cps) composition of clauses. A multiple composition is a special composition of concurrent clauses based on Dijkstras guarded commands [5] where the valuation (val) clauses are evaluated before the results are assigned to the corresponding slots. In order to keep the paper short, we introduce some details of the language Nautilus through examples and, at the same time, we give its semantics using nonsequential automata. 17

Menezes, Sernadas & Costa 3.1 Simple Object The rst example introduces a simple object in Nautilus. In what follows, for an attribute a, ?a denotes its initial (birth) value. For instance, the set of all possible values of an attribute a of type boolean is f?a , Fa, Tag. Example 3.1 (Simple Object) Consider object Obj in Figure 11 (in this example, do not consider the rightmost column). Note that the birth action Start has two alternatives. Both alternatives are always enabled, since they do not have enabling conditions. However, since it is a birth action, it occurs only once. Due to the enabling conditions, each action occurs once and in the following order: Start, Proc and Finish. object Obj category birth Start death Finish body slot a: boolean slot b: boolean act Start alt S1 seq val a