Scenario-based speci¯cations are used for modeling highlycomplex, distributed systems in terms of partial runs (scenarios) the system shall have. But it is di±cult to derive an implementing, operational model from a given set of scenarios, especially if concepts like anti-scenarios which must not occur are used. In this paper, we present a novel model for scenario-based speci¯cations with Petri nets including anti-scenarios; we provide an operational semantics for our model.
? The author's work is funded by the DFG-Graduiertenkolleg 1324 \METRIK".
Oclets - scenario-based speci¯cations with Petri nets A scenario speci¯es a possible course of (future) actions and the therein involved resources in the context of a larger system. Whether a scenario suits a given situation can be subject to further conditions. In our case, we conceive and formalize a scenario as a partial, partially ordered run (a labeled causal net) with a behavioral precondition. We de¯ne a system model as a set of scenarios describing sequentially connected, concurrent, mutually exclusive, and overlapping behavior. The system behavior shall be computed by composing its scenarios.
We formalize scenarios in our Petri net class of oclets. Let Names = Actions ] Resources denote a set of labels.
De¯nition 1 (Oclet). An oclet o = hP; T; F; `; pre; typei is a labeled, safe, elementary causal net hP; T; F; `i that labels places with resources and transitions with actions; o has a non-empty, precondition pre µ (P [ T ), that is causally closed (8x 2 pre :: ²x µ pre), and a type 2 fnormal ; anti g. The set (P [ T ) n pre is the contribution of o.
A normal oclet describes a partial run that may occur in the system. An antioclet describes a partial run that may not be completed in the system; therefore an anti-oclet contributes exactly one place or transition (that must not occur). Figure 1 shows some (technical) example oclets. The system fo1; : : : ; o5g shall yield the behavior that is formalized in the occurrence net ¯5. The behavior of a set of oclets is constructed by repeatedly composing the oclets with a labeled occurrence net. An `initial' occurrence net ¯0 represents the initial state; composing ¯i with an oclet o yields an occurrence net ¯i+1.
Roughly, a normal oclet o is composed with a labeled occurrence net ¯, ¯ © o by building the union of the nets, and merging two transitions (places) if they are labeled equally and have equally labeled predecessors. This is only allowed if o's precondition is found in ¯; all nodes of o's precondition are merged with nodes of ¯. To compose an anti-oclet o with ¯, ¯ ª o, ¯rst compose o like for o1 a o3 c
U b W d o2 a
U c V d o4 b e
X d f Y g o5 anti b
X f
W d o6 anti b
X f Y
W d ¯0 ¯3 b a a U V d c W d ¯5 b X a U V d Y g e f e f c W d X
Y g
Fig. 1. Some example oclets o1; : : : ; o6 and three labeled occurrence nets ¯0; ¯3; ¯5. normal oclets, then remove the contribution of o and all successor nodes. Antioclets have priority: a node that was removed by an anti-oclet o¡ is not added again by some other oclet o+ as it is immediately removed by o¡ again.
Consider the example of Fig. 1 with the initial occurrence net ¯0 being a single place labeled a. Composing ¯0 with oclet o1, yields ¯1 := ¯0 © o1 which is isomorphic to o1. ¯2 := ¯1 © o2 adds the post-place c to transition U and transition V with post-place d. In ¯3 := ¯2 © o3, transition W is added in con°ict to V; see Fig. 1.
To compute ¯4 := ¯3 © o4, o4 has to be added twice because there are two (con°icting) places d. Composing ¯4 with anti-oclet o5 removes f and successors Y and g from the branch that depends on W; the resulting occurrence net ¯5 := ¯4 ª o5 is depicted in Fig. 1. Alternatively, composing with anti-oclet o6 removes Y and successor g, but leaves f. The runs of ¯5 are the runs of fo1; : : : ; o5g, the runs of ¯6 are the runs of fo1; : : : ; o4; o6g.
This informally sketched approach for scenario-based system speci¯cations succeeds only if we can prove its formal consistency and show that branching processes (or rather a certain kind of labeled occurrence nets) are closed under our composition operations © and ª. 3
Formalizing oclets with canonically named nodes
Our oclet composition requires to ask frequently which nodes of an oclet o and
an occurrence net ¯ describe identical actions or resources, and, hence, must
be merged. Formalizing this identity, and operations on labeled nets becomes
tedious because two isomorphic nets may have disjoint, or overlapping sets of
nodes. Identity can only be de¯ned by relating labels of nodes to labels of
neighboring nodes; this leads to graph isomorphism problems. Esparza and Heljanko
use a formalization called canonically named nodes for formalizing branching
processes of (safe) Petri nets [
Canonically named nodes determine their identity by their labels and their predecessor: two nodes are identical if and only if they have identical labels and identical predecessors. The following formalization captures this canonical identity : The set C of canonically named nodes (C-nodes) is de¯ned inductively as the least set that contains ha; ;i for every a 2 Names and if x1; : : : ; xn 2 C and a 2 Names then ha; fx1; : : : ; xngi 2 C.
C-nodes can be used as the base set of transitions and places of labeled Petri nets. A node hact ; Xi 2 C; act 2 Actions is a C-transition with label act , a node hres; Xi 2 C; res 2 Resources is a C-place with label res. We use C-nodes to formalize a speci¯c class of labeled Petri nets.
De¯nition 2 (C-net). A labeled Petri net N C = hP; T; F; `i is a C-net i® P µ C are C-places, T µ C are C-transitions, and for each x := ha; Xi 2 P [ T holds: 1. if x is a C-place, then X is a set of C-transitions, 2. if x is a C-transition, then X is a set of C-places,
In a C-net exist no two distinct, equally labeled nodes ha; Xi; ha; Y i with the
same preset X = Y , this establishes the canonical identity of C-nodes which
we described above. This is a trivial mathematical consequence, but it has an
interesting interpretation in branching processes: any two di®erent actions
(transitions) or resources (places) either have a di®erent name, or a di®erent causale.
Esparza and Heljanko have shown that for this reason, C-net structures are a
good candidate to formalize branching processes (BP) of (safe) net systems [
Our oclet approach has a similar aim: construct branching-time artifacts that
describe the behavior of a system. The di®erence is that we do not construct
our artifacts from a net structure, but from oclets. Our construction does not
only extend a branching process by adding a single transition (and its
postplaces) whenever the transition is enabled as in classical branching processes.
The precondition of an oclet can be arbitrarily complex, and added nodes may
have to be merged with the net. This means our formalization has to consider
the causal structure of a labeled occurrence net and of an oclet together. To this
end, we extend the C-node approach of [
Operations on C-nets and sets of C-nodes The structure of a C-net N C = hP; T; F; `i is completely encoded in its nodes, the information in its arcs F is redundant. Thus, the nodes XNC =df P [ T of a C-net N C are su±cient to reconstruct F and, hence, N C. Because any two isomorphic C-nets are identical, each (normal) Petri net N has a unique, isomorphic C-net N C which is completely encoded in XNC .
This greatly simpli¯es our composition operation: the union of two sets of C-nodes `merges' canonically identical nodes by their identity. If we consider the sets XoC1 and XoC2 of C-nodes of o1 and o2 in Fig. 1, the composition ¯2C := (¯0C © o1C) © o2C can be rephrased as the union X¯C2 = X¯C0 [ XoC1 [ XoC2 . For instance, ha; ;i and hU; fha; ;igi occur both in o1C and o2C. But this approach does not work for o3; o3C contains hc; ;i, while ¯2C contains hc; fhU; fha; ;igigi.
Our proposed solution is to introduce variables into nodes with empty preset, e.g. hc; vi such that the minimal nodes of an oclet which constitute the begin of a scenario can be assigned to other `compatible' nodes `further down' the occurrence net during the composition.
Let Var denote an (in¯nite) set of variables. The set A of canonically named abstract nodes (A-nodes) di®ers to C in its induction base: For every a 2 Names and every v 2 Var , ha; vi is an A-node, and if x1; : : : ; xn 2 A and a 2 Names then ha; fx1; : : : ; xngi 2 A. Correspondingly, the class of A-nets can be de¯ned; the variable takes the role of the empty pre-set, that is, a node ha; vi of an A-net N A has no predecessor in N A. Wlog. for all ha1; v1i; ha2; v2i 2 XNA holds that v1 = v2 implies a1 = a2.
With this convention in mind, we transfer the pre-set notation ²(:) from Cnodes (or Petri nets) to A-nodes; we set ²ha; vi =df v. This canonically lifts all other notions like causal relation ·, con°ict ], and concurrency jj from Petri nets and C-nodes to A-nodes. As a consequence, any two distinct nodes ha1; v1i; ha2; v2i; v1; v2 2 Var are concurrent.
We introduce variables as place-holders for the pre-set of a C-node. Thus an assignment ® maps each variable v to a (possibly empty) set ®(v) of C-nodes, ® : Var ! 2C. If xA 2 A, then xA [®] denotes the C-node that is obtained from xA by simultaneously replacing every occurrence of each variable v 2 Var with ®(v). This notion canonically lifts to sets XA µ A.
There is an important technical detail, that we have to consider: Let N be a safe, causal, labeled, elementary Petri net and let XNA be the corresponding set of A-nodes of N . An assignment ® is feasible on XNA i® for any two distinct minimal nodes ha1; v1i; ha2; v2i 2 XNA holds: ha1; ®(v1)i jj ha2; ®(v2)i. A feasible assignment guarantees that two concurrent nodes (like b and d of o4 in Fig. 1) remain concurrent under the assignment.
We may now formalize our oclet composition operations.
De¯nition 3 (Enabling assignment). Let ¯C be a labeled C-occurrence net, let oA be an A-oclet with precondition preA. An ® is enabling for oA in ¯C i® ® is feasible and preA [®] µ X¯C. Let enabled(oA; ¯C) denote the set of all enabling assignments for oA in ¯C.
Wlog. the set enabled(oA; ¯C) contains no two assignments ® that di®er only on variables which do not occur in oA.
As an example consider o1 and ¯0 of Fig. 1: preoA1 = fha; v1ig, X¯C0 = fha; ;ig. The assignment that maps v1 to ; is enabling for o1 in ¯0. Oclet o4 has two qualitatively di®erent enabling assignments in ¯3.
A further notion which we need for the composition is the causal past bxc of a C-node x with bxc =df fy 2 C j y · xg; this notion also lifts to sets of C-nodes. ¯2C =df ¯C © oA with X¯C2 =df X¯C [(XoA [®1] [ : : : [ XoA [®k]).
De¯nition 4 (Oclet composition). Let ¯C be a labeled C-occurrence net. Let oA be an A-oclet with enabled(oA; ¯C) = f®1; : : : ; ®kg.
If oA is a normal oclet, then the composition of ¯C with oA yields the C-net If oA is an anti-oclet with contribution fyog = XoA n preoA, then the composition of ¯C with oA yields the C-net ¯2C =df ¯C ª oA with X¯C2 =df fx 2 X¯C jbxc \(yo [®1] [ : : : [ yo [®k]) = ;g.
Consider o1A and ¯0C of our example; XoA1 = fp1A; t1A; p2Ag with p1A = ha; v1i, t1A = hU; fp1Agi, p2A = hb; ft1Agi. The enabling assignment f®g = enabled(o1A; ¯0C) yields XoA1 [®] = fp1C; t1C; pC
2 g with p1C = ha; ;i etc. Thus the composition ¯0C © o1A yields exactly XoA1 [®], merging the two places labeled a.
The composition with an anti-oclet is formally more involved, but straight forward: All nodes of ¯5C in Fig. 1 including the greyly shaded ones constitute ¯4C where o5A has one enabling assignment f®g = enabled(o5A; ¯4C) mapping the variables of hb; v1i and hW; v2i of o5A to fhU; fpaCgig and fhc; ftCUgig of ¯C, re4 spectively. The contributed node of o5A is yo5 = hf; ftXAgi; ® maps yo5 to the right-most node hf; ftCX;2gi = yo5 [®] of ¯4C. All nodes of ¯4C which have this node in their causal past are to be removed, i.e. hf; ftCX;2gi itself and all nodes reachable from it via the °ow-relation. This results in ¯C. 5
With this formalization one can show that labeled C-occurrence nets are closed under composition with © and ª. From the set theoretic de¯nitions of ª follows that (¯ ª o1) ª o2 = (¯ ª o2) ª o1 for any C-occurrence net ¯ and any two A-anti-oclets o1 and o2. (¯ © o1) © o2 = (¯ © o2) © o1 for normal oclets o1; o2 holds only if o2 does not introduce new enabling assignments for o1. The behavior of a set of oclets is de¯ned as its C-unfolding : De¯nition 5 (C-unfolding). Let O be a set of oclets with fo1; : : : ; okg and fok+1; : : : ; olg being the normal oclets and the anti-oclets of O, respectively. Let ¯0 be a C-occurrence net. The ¯xed point of the sequence h¯0; ¯1; ¯2; : : :i with ¯i+1 =df (¯i © o1 © : : : © ok) ª ok+1 ª : : : ª ol is the C-unfolding of O. Summary and Future Work. De¯nition 5 concludes the presentation of our basic model for scenario-based speci¯cations with Petri nets. The presented expressive means allow specifying complex behavior in terms of partial runs which may or must not occur.
The basic model has already been implemented in the Graphical Runtime EnvironmenT for Adaptive systems (GRETA). Next, we will introduce further LSC features like hot and cold annotations for specifying which actions must occur and which states are legal ¯nal states. Further, we plan to introduce the notion of an interface to specify system composition, and system interaction. Finally, the question which Petri net has the same behavior as a given set of oclets shall be addressed.