2 Structure of this paper, We focus on a sub language of PEPA We describe the conversion of models in the language. into a representation by a pair of matrices termed the pre and post matrices which are. the basis for the subsequent analysis of the system At this point we summarise the relevant. techniques for structural analysis of Petri nets which we have used for the analysis of models. in our stochastic process algebra We then present a procedure which can be used to extend. our sub language to full PEPA by adding the hiding operator Finally we point to future. directions of this work,3 The PEPA language, We are not making use here of the added system description information which is provided. by the rates which are paired with each occurrence of an activity within a model and so in. order to simplify the presentation of the method of structural analysis we remove the spe. cifications of rates from models This action is justified because in PEPA we have the special. case of all activity rates being parameters of negative exponential distributions with infin. ite support In this situation we know that rate information can be systematically restored. afterwards CABC93, In order to facilitate the explanation of our present consideration of structural properties of. process algebra models we use the PEPA language without the hiding operator We will show. in Section 7 that the hiding operator could be added without any significant complication. Thus the simplified stochastic process algebra which we are using here is simply a convenient. explanatory device and does not compromise the usefulness of our work The grammar of the. language is presented in Figure 1,S sequential components. A constant,S S choice,P parallel components,S degenerate case. co operation on L,Figure 1 Grammar for the PEPA sub language. Constants are bound by defining equations of the form A P The function to determine. the activities of a component written as Act A calculates the complete alphabet of the. component syntactically as the set of all activity names which are used in the description of. the component, A consequence of the grammar is that the collection of equations describing a system can. be partitioned into two sets The equations which specify the behaviour of the sequential com. ponents are known as defining equations those which specify how those components interact. are termed model equations Note that via a process of back substitution we can always. reduce the set of model equations to a single system equation We impose the constraint that. the constant introduced on the left hand side of the system equation cannot be used recurs. ively Without loss of generality throughout the remainder of this paper we will assume that. PEPA models are formed by a set of defining equations and a single system equation Thus. those combinators which are used to construct sequential components are dynamic combin. ators whereas those which are used to construct parallel components are static components. The significance of this is that the number of parallel components contained within a model. will be invariant over all states,4 An overview of Petri nets. Petri nets are another formalism which is widely used in the modelling and analysis of systems. that exhibit complex behaviour due to the interleaving of parallelism and synchronisation. We concentrate here on Place Transitions P T net systems and summarise only enough for. our present needs For a thorough introduction to the topic the reader should consult the. following references Mur89 Pet81, A P T net is a bipartite directed graph represented as a quadruple N hP T Pre Posti. where P and T are the sets of the two kinds of nodes places and transitions and Pre and. Post are the P T sized natural valued incidence matrices which represent the arcs. Post p t w means that there is an arc from t to p with weight or multiplicity w and. Pre p t 0 indicates that there is no arc from p to t A marking m is a P sized natural. valued vector In the graphical representation of a P T net a place is represented by a circle. a transition by a box or bar and the marking by a number of dots or tokens present in each. place A P T system is a pair S hN m0i where m0 is the initial marking A transition t. is enabled in a marking m if and only if m Pre P t Its occurrence or firing yields a new. marking m0 m C P t where C Post Pre is called the token flow matrix. A P T system is live when every transition is live i e it can ultimately occur from. every reachable marking and it is deadlock free when every reachable marking enables some. transition A P T system is bounded when every place is bounded i e its marking value. is less than some bound at every reachable marking Boundedness precludes overflows and. liveness ensures that no single transition in the system can become unattainable. Structural techniques provide a valuable approach to the analysis of Petri net models. These techniques are based on the idea that useful information about the behaviour of the. system can be gained from the structure of the net and the initial marking without neces. sarily carrying out a reachability analysis This has led to the development of some efficient. algorithms for the analysis of P T systems Two techniques have been predominantly used. i graph theory and ii linear algebra or convex geometry Starting from the ideas of live. ness and boundedness in this paper we are seeking to define analogous properties for PEPA. models and to develop similar techniques for their investigation Here structure is replaced. by syntax we aim to analyse the behaviour of the model without generating a derivative. graph but merely by syntactic analysis of the definitional equations analogous to the net. structure and the system equation corresponding both to net structure and initial marking. In Rib95 it was proved that any PEPA model can be seen as a GSPN Ribaudo s. approach was to define a labelled GSPN semantics of PEPA models in which a corresponding. net construction is associated with each of the combinators of the language One consequence. of this work is that in principle at least all the structural theory developed for Petri nets is. available for the analysis of PEPA models However based on Ribaudo s approach it is not. immediately apparent how this theory can be exploited at the level of the PEPA model. In the following sections we will describe how to construct pre and post incidence matrices. for a PEPA model This has the consequence that a P T system can be defined from each. PEPA model However unlike Ribaudo s work finding the corresponding P T system is. not the objective of our work Instead based on the matrix approach we will see that. some important results from Petri net theory can be used in a straightforward manner to. obtain information about the PEPA model We must point out however that the approach. of the two formalism is quite different and this must be taken into account for a correct. interpretation of the results as we shall see,5 Conversion to a matrix representation. We explain the conversion from the process algebra definitional equations to an equivalent. representation as a pair of matrices which record the activities which are performed and the. derivatives which result from this The presentation of the matrices has a column for each. activity instance and a row for each component derivative whether named by an identifier or. not Note that these are not the derivatives of the complete model which would be generated. by application of the semantics to the system equation but the derivatives of the sequential. components generated by application of the semantics to the definitional equations Thus the. resulting matrices have a block structure each block corresponding to one component in the. system equation, We note that a similar representation of PEPA models in terms of pre and post transition. vectors for activities was previously presented by Sereno Ser95 for the purpose of investig. ating product form equilibrium distributions, In order to establish the starting state of the PEPA model in addition to the pre and post. incidence matrices we must also construct a state vector s0 analogous to the initial marking. m0 Recall that the specification of a PEPA model consists of a set of defining equations. and the system equation The local states of our model are the sequential derivatives defined. by the defining equations Given this set of places each global state s is the number of. instances of each sequential derivative apparent in the syntactic form representing that state. In particular the initial state s0 is a vector in which the entry for each derivative is the. number of instances of that syntactic form which are found on the right hand side of the. system equation As with the incidence matrices we can think of this vector as having a. block structure corresponding to the components of the model. Just as the Pre and Post matrices of a P T system can be combined to form the token. flow matrix C Post Pre the Pre and Post matrices of a PEPA model can be combined. to form the characteristic matrix C Post Pre,5 1 Prefix. Consider the following very simple component which only performs the activities and in. alternation, This component has two states and two activities and the information in its defining equation. may be recorded in the following pair of pre and post matrices The pre matrix is compiled. by recording the information that the component P can perform an activity thereby placing. an entry in the first row and the component P can perform a activity thereby placing. an entry in the second row The post matrix is compiled in a similar fashion by recording. that the component P is reached after performing a activity and that the component P. is reached after performing an activity,P 1 0 P 0 1. P 0 1 P 1 0, Observe that we can associate with each non null element of the pre matrix another non null. element of the post matrix i e we move from one local state to another Therefore the number. of non null elements in any column will be the same in the pre matrix and the post matrix. 5 2 Choice, Here a component performs a sequence of activities in which each activity is followed by. either a or a activity, The component has two states both of which are named and three activities Its represent. ation in terms of pre and post matrices follows,Q 1 0 0 Q 0 1 1. R 0 1 1 R 1 0 0, The preservation property which we noted in the previous case does not hold for rows We. see this because the non null elements of a row in the pre matrix represent syntactically. distinct occurrences of an activity which can be performed in that state in order to evolve to. a derivative of that component However the corresponding row in the post matrix represents. a local state which was reached after performing those activities which are associated with. non null entries There is no reason for these two numbers to be the same In our example. here the state Q can only perform a single activity but could have been reached by one of. two distinct activities A complementary property can be observed of the state R. 5 3 Cooperation,5 3 1 A first example, We consider a pair of components P and Q which synchronise on their common activities. and and P performs an individual activity before returning to the activity. Q This has three states and, The system which we are representing in the matrices is P. three activities,P 1 0 0 P 0 0 1,P 0 1 0 P 1 0 0,Pre P 0 0 1 Post P 0 1 0. Q 1 0 0 Q 0 1 0,Q 0 1 0 Q 1 0 0, Until this point because we were working with a single sequential component the states which. were associated with the rows of the matrices were coincident with the states of the system. Now that we have a cooperation between two sequential components we note that the rows. present information about the local states of subcomponents of the model The advantage. which this decomposition affords is that the sequential subcomponent which is performing the. activity is identified This information would be lost if the state of the whole model P. Q or P Q was used as the designator of each row in each matrix. The row vector representation of the system equation of this model is shown below. The column labels of this vector are the row labels from the pre and post matrices We will. normally omit these labels when presenting vector representations of system states. We can observe from this example that synchronisations between the components P and. Q here can be clearly seen from the matrix representation where there is any column in the. pre matrix whose sum is greater than one However it should be noted that in general a. column whose sum is greater than one merely represents a potential synchronisation between. components If the model which is being investigated contains activities which are never able. to be performed then potential synchronisations might never actually occur. 5 3 2 A second example, In the previous example the matrix representation had more rows than the number of states. in the process algebra model of the system This is because the component Q is tightly. synchronised to P in a slave relationship We now consider an example where the numbers. are ordered in the other way with the number of states in the process algebra model greater. than the number of rows in the matrix representation. Consider the following model which has three components P Q and R where Q enforces. fairness between P performing activities and R performing activities. The system which we consider is P Q R The activity which P and Q synchronise upon. is and the activity which Q and R synchronise upon is The matrix representation for. this model is shown below The process algebra model has eight states and twelve transitions. The system equation gives s0 1 0 1 0 1 0,P 1 0 0 0 P 0 1 0 0. P 0 1 0 0 P 1 0 0 0,Q 1 0 0 0 Q 0 0 1 0,Q 0 0 1 0 Q 1 0 0 0. R 0 0 1 0 R 0 0 0 1,R 0 0 0 1 R 0 0 1 0,5 3 3 A third example. Observe that the possible activities in a PEPA model do not always coincide with the columns. in the pre and post matrices Even more since the matrices are derived in a purely syntactic. way there may appear to be synchronisations recorded in the matrices which in fact will never. occur For matrices derived from Petri net representations the presence of these phantom. synchronisations indicates a flaw in the given net However this is not the case for process. The system which we consider is P Q Components P and Q synchronise upon execute. and on their own and synchronise again upon This model has five states and six. transitions, The matrix representation for this model is shown below In determining the transcription. of in the matrices since each component has two instances of four apparent synchron. isation points are noted Two of these are real the leading activities from P and Q and. the trailing activities from P and Q and two of these are phantoms a leading with a. trailing in both cases From the system equation we have s0 1 0 0 1 0 0. P 1 1 0 0 0 0 P 0 0 1 1 0 0,0 0 0 0 1 0 P,1 1 0 0 0 0. 0 0 1 1 0 0 P,0 0 0 0 1 0,1 0 1 0 0 0 Q,0 1 0 1 0 0. Q 0 0 0 0 0 1 Q 1 0 1 0 0 0,Q 0 1 0 1 0 0 Q 0 0 0 0 0 1. Note that Sereno explicitly excludes the case of repeated instances of an activity within a. sequential component Ser95 He also imposes that when sequential components undertake. activities of the same name they must do so in cooperation We do not include this restriction. as the following example shows,5 3 4 A fourth example. Until now all of our examples have considered systems where the model components syn. chronised on all of their common activities In PEPA it is possible to express pure parallel. execution of activities as synchronisation over the empty set of activities This permits the. representation of an implicit choice where for example cooperations take place pairwise. between two of three components We show this in the present example along with the. treatment of self loops where performing an activity leaves a model component in the same. The system we consider is P Q R Pair wise synchronisations take place between P. and R and between Q and R This model has four states and eight transitions The system. equation gives s0 1 0 1 0 1 The matrix representation for this model is shown below. It is evidently important to represent clearly the pair wise synchronisations and not to allow. the inference of a three way synchronisation between P Q and R For this reason the matrix. must devote two columns to the two kinds of synchronisations on the activity. P 1 0 0 0 P 0 1 0 0,P 0 1 0 0 P 1 0 0 0,Pre Q 0 0 1 0 Post Q 0 0 0 1. Q 0 0 0 1 Q 0 0 1 0,R 1 0 1 0 R 1 0 1 0,5 4 A fifth example. For our final example we consider the problem of capturing component duplication in the. system equation of a PEPA model To illustrate one of the reasons why this can be problematic. we consider a model where the duplicated components are initiated in different local states. by the system equation,Q P 0 R Here because the two copies of. The system which we consider is P, the component P are initiated in the orientation which suits their partner component in. the cooperation expression the model has four states and eight transitions In contrast the. Q P R immediately deadlocks We require these two PEPA models. system P 0, to have different representations and these differ only in their initial state vectors as shown. P P 0 Q Q P P 0 R R,1 0 1 0 0 1 1 0,P P 0 Q Q P P 0 R R. 0 1 1 0 1 0 1 0, As we note from these vectors our method of processing duplicated components is to add. rows to the matrices for each of the copies In net terms this corresponds to duplicating the. net structure We omit the pre and post matrices,6 Application of structural analysis techniques. In this section we show how structural analysis techniques from P T nets can be applied to. stochastic process algebra models expressed in the PEPA language We begin by introducing. relevant terminology which will enable us to classify structurally flawed PEPA models. 6 1 Notions of liveness, The concept of liveness is well understood for Petri nets We introduce a variation on this. group liveness which can be mirrored in process algebra PEPA liveness and introduce a. stronger notion of liveness for process which implies PEPA liveness. P T liveness PN From each reachable state of a net there is for each transition a. sequence of firings which leads to the transition becoming enabled. Group liveness PN From each reachable state of a labelled net there is for each label. a sequence of firings which will lead to a transition with that label being enabled. PEPA liveness PA For each reachable state and every action type there exists another. state which is reachable where an activity of that type can be performed. Full liveness PA For each reachable state and each syntactic occurrence of an activity. within a sequential component there exists another state which is reachable where this. occurrence of the activity can be performed, The most interesting relationship between these four notions is the relation of P T liveness to. full liveness If we consider the P T system corresponding to a fully live PEPA model we can. see that P T liveness implies full liveness but that the converse is not true Problems arise. because of the possibility of phantom synchronisations these are an artifact of the algebraic. representation of a model and do not arise in Petri net models. It should be clear that full liveness implies PEPA liveness and that the notions of group. liveness and PEPA liveness are equivalent notions in the two formalisms The existence. of phantom synchronisations does not present a difficulty here because there will be another. instance of the synchronisation on the same activity which can be performed from some state. All of these notions of liveness guarantee freedom from deadlock. 6 2 Boundedness in process algebra models, Boundedness for P T systems is defined in terms of a bound on the number of tokens which. can reside in each place of the net For a process algebra model syntactic forms of sequential. components play a role analogous to places Thus we can say that a model is bounded if. there is a bound on the number of instances of each sequential derivative which will appear. in any state of the model, Given the direct mapping between syntactic states of the PEPA model and the states of. the underlying Markov process boundedness is clearly a necessary condition for finiteness of. the stochastic model,6 3 Significance of the structural analysis. We wish to have the structural analysis determine the strongest form of liveness namely full. liveness We caution the reader that this does not guarantee the well known cyclic condition. for PEPA models but an example which makes clear the difference is not easy to construct. and so we do not present such an example here The curious reader may consult Col89. One of the principal tools used in the analysis of P T systems is the state equation Recall. that when one transition t is fired from a state m the new state that is reached m0 can be. obtained as m0 m C P t Analogously if a sequence is fired the state that is reached. can be computed as, where t represents the number of times transition t occurs in the sequence Unfortunately. there may be solutions of the equation that do not correspond to firable sequences these are. termed spurious solutions, For any P T net flows semiflows are integer natural annullers of C Right and left. annullers are called T and P semi flows respectively Flows are important because they. induce certain invariant relations which are useful for reasoning about the behaviour of the. net For instance if y 0 and y C 0 then every reachable state m satisfies y m y m0. This implies the existence of a invariance relation which can be expressed in terms of the. number of tokens distributed over the places of the net Similarly any repetitive transition. sequence which returns a marking to itself satisfies that C 0. The existence of certain annullers or similar vectors define several behavioural properties. over the corresponding net These properties will hold for any P T system with the given. net structure i e for any initial marking For example. N is consistent structurally repetitive if and only if x 0 exists such that C x 0. N is conservative structurally bounded if and only if y 0 exists such that y C 0. The characteristic matrix of a PEPA model is always conservative because as we previ. ously remarked any non null element in the pre matrix has a corresponding element in the. post matrix In particular this means that the number of copies of processes does not change. as the system evolves which from a Petri net point of view means that the system is bounded. In bounded P T systems with a finite number of states liveness cannot be achieved. unless there is a repetitive sequence covering all the transitions Therefore consistency is a. necessary condition for liveness in bounded systems This condition has been improved by. the addition of an upper bound to the rank of the token flow matrix The bound is based on. the definition of an equivalence relation between transitions. Definition 1 Equal conflict relation We say that transitions t and t0 are in equal con. flict relation if Pre P t Pre P t0 6 0 Each equivalence class is an equal conflict set. denoted for a given t EQS t SEQS is the set of all the equal conflict sets of a given net. Theorem 1 The Rank Theorem TS96 If S is a live and bounded system then it is. consistent conservative and rank C SEQS 1, This theorem cannot be applied directly to PEPA models because as we previously remarked. full liveness in PEPA models does not imply liveness of the associated P T system. Our reasoning in the proof of the rank theorem for PEPA requires a slight restriction on. the form of PEPA models We make use of a condition which we term uniqueness of guards. defined as follows, Definition 2 Uniqueness of guards In each sequential component the action types of. activities which are guards on choices i e the activities which are in competition can never. be performed again without first re visiting the state where the choice was made. The Rank Theorem for PEPA models is based on the following Lemma for P T systems For. the statement of the Lemma we need the following definition. Definition 3 Circuit arbiter Let N be a P T net and let e be an equal conflict set such. that e 1 A net Ce hPe e Pree Poste i is an ordinary circuit arbiter for the equal. conflict set e if and only if Ce is a net in which all arcs are weighted 1 such that Pe P. and its underlying graph is an elementary circuit, The effect of the circuit arbiter is to impose a fair ordering over the firings of the transitions. of the equal conflict set, Lemma 6 1 Let S hN m0i be a P T system that is bounded group live and such that all. the transitions that belong to non trivial equal conflict sets are live Let e SEQS such that. e 1 Let Ce be a circuit arbiter for e and let N 0 be the net N merged with the circuit. arbiter Ce sharing the transitions in e Then, 1 There exists a marking m0 0 with m0 0 P m0 such that S 0 hN 0 m00 i is bounded. group live and all the transitions in non trivial equal conflict sets are live. 2 rank C0 rank C e 1 where C0 is the token flow matrix of N 0. Theorem 2 The PEPA rank theorem Let S be a fully live PEPA model satisifying the. uniqueness of guards restriction Then its associated characteristic matrix C satisfies that. There exists y 0 such that y C 0, There exists x 0 whose support covers all the action types in S and such that C x 0. rank C SEQS 1, Proof The existence of the positive left annuller is an immediate consequence of the fact. that in PEPA sequential processes are not created nor destroyed. Since the number of states of the system is finite for it to be live there must exist a. repetitive sequence of activities We cannot ensure this sequence will cover all the columns. of the matrix due to the possible existence of false synchronisations but it must contain. every action type at least once Observe that this also means that the corresponding P T. system is group live although not necessarily live The token flow matrix of this net C is. equal to the characteristic matrix C of the PEPA model. Furthermore observe that the uniqueness of guards condition ensures that in the corres. ponding net all the transitions in non trivial equal conflict sets are live. Thus we can apply the Lemma Let N 0 be the corresponding net N together with integ. rated circuit arbiters for every non trivial equal conflict set Applying point 2 of Lemma 6 1. repeatedly after each circuit arbiter is merged P which can be done thanks to point 1 of the. Lemma it follows that rank C0 rank C e SEQS e 1 Moreover this system re. mains bounded and group live hence there must exist a repetitive transition sequence and. thus C SEQS 1 Rearranging the above inequalities we obtain a bound for the rank of. the PEPA characteristic matrix C,rank C y e 1 1, where y is the number of columns in C Since e SEQS e T y this bound is SEQS 1. and the result follows 2, By analysing the defining equations of a PEPA model we can partition the activities of the. model into equal conflict sets which are equivalent to the equal conflict sets of transitions in. the corresponding P T system Thus this result becomes a procedure of structural analysis. which can be applied to any PEPA model to ascertain whether it is possible for it to be fully. 6 3 1 Determining absence of liveness, In order to clarify the reader s understanding of the notions associated with equal conflict. relations and the use of the Rank Theorem we present a small worked example which builds. the equal conflict relation for a small PEPA model with a deadlocking state The model. contains two components P and R which synchronise on activities and. The system which we study is P R which has a deadlock at P R The matrix. representation for this model is shown below,P 1 1 0 0 P 0 0 1 1. P 0 0 1 0 P 1 0 0 0,Pre P 0 0 0 1 Post P 0 1 0 0,R 0 0 1 0 R 0 0 0 1. R 0 0 0 1 R 0 0 1 0, We observe from the pre matrix that the activities and satisfy the equal conflict condition. for this model and are thereby considered equal We can now observe that we have the. following set of activities in equal conflict, For this model the rank of the matrix C is equal to the cardinality of the set of equal conflict. sets Thus solely from this structural analysis of the model we can use the Rank Theorem. to conclude that the model is either not live or it is not bounded Since all PEPA models are. bounded we can conclude that the model is not live The failure of this property signals a. logical error in the model itself which would direct the performance modeller not to proceed. onto the performance analysis of the model but rather instead to attempt to diagnose the. source of the error, Recall that for a P T net structural analysis is based solely on the net structure without. the initial marking To some extent the same is true for structural analysis of PEPA models. However note that although the system equation is used to form the initial state analogous. to the initial marking it also plays a crucial role in defining the structure of the model For. example if the system equation in the model discussed above had been P R the pre and. post matrices would each have had two columns corresponding to the two distinct instances. of the activity Moreover each instance would form a separate element within SEQS However. the rank of the characteristic matrix remains 3 indicating that the modified model is free. from deadlock which it is, When a deadlock is indicated one useful diagnostic method is to remove columns from C. in order to isolate one of the activities which appears in an equal conflict set of cardinality at. least two The modeller then attempts to solve the consistency condition by seeking a right. annuller for the reduced matrix C 0 This process corresponds to forcing a choice always to be. resolved in a particular way which has the consequence that if an annuller cannot be found. for this reduced matrix then it may be concluded that there is a problem which stems from. taking this branch of the choice Repairing problems which are found by this method will. eventually result in a model which is worthy of performance based analysis possibly with an. intervening step to determine freedom from deadlock. When analysing the possibility of deadlock the existence of phantom synchronisations. will not present a problem and the techniques used for P T systems can be used without any. modification These techniques are again based on the state equation although the existence. of spurious solutions prevents it from being a characterisation of the absence of deadlock. Theorem 3 TCS93 Let S be a P T system If there is no integer solution to. m p Pre p t t T,p Pre p t 6 0,then S is deadlock free. In general this means that the absence of solutions of several systems of equations has to be. proved However there are cases where the number of systems of equations can be significantly. reduced TCS93 In particular when analysing a PEPA model we need to consider only. a single system of equations This follows because even when the PEPA model contains. several copies of the same component each of these is represented separately in the pre. and post matrices and one linear inequality is sufficient to represent the restrictions on a. transition TCS93, Theorem 4 Let S be a PEPA model with n sequential components which we name P10 Pn0. and let the derivatives within Pi0 be named Pi0 Pini Furthermore let A be the set of activ. ity instances represented in the pre and post matrices of S If there is no solution for s for. any activity sequence represented in vector form with. s Pij Pre Pij A,Pij Pre Pij 6 0 Pij Pre Pij 6 0,then S is deadlock free. 7 Adding a hiding operator, Cooperation on activities in the PEPA language is fully general Cooperation may involve. any number of components and any number of these cooperands may play an active role This. generality is in marked contrast to the model of synchronisation in CCS Mil89 in which ex. actly two agents are involved in every synchronisation In CCS a synchronisation between two. agents is hidden as an invisible action in order to make clear the impossibility of multi way. synchronisation One purpose of hiding in a process algebra which has multi way synchron. isation as PEPA does is to prevent additional components from being able to synchronise. on a particular set of activities those activities which are hidden Another use of hiding in. a stochastic process algebra such as PEPA is to designate activities which are considered in. significant in terms of system performance because rewards cannot be associated with hidden. actions In practice the effect of hiding is to rename an activity to the reserved name which. cannot be used in any synchronisation set Thus in order to add a hiding operator to PEPA. we will describe the implementation of the operator in terms of this renaming operation The. impossibility of synchronising on a activity is enforced by choosing for each replacement an. activity 0 1 2 drawn from an unbounded set A freshly numbered activity is chosen. for each replacement so that the PEPA cooperation operator will allow these activities to be. performed independently, The renaming activity can be implemented by a substitution operation combined with the. generation of new definitional equations for model components where necessary Fresh names. for components are produced by decorating an identifier with a prime We think of the prime. symbol as an operator which can be applied to a collection of equations in order to generate. a related collection of definitions for components with primed identifiers. Before proceeding to the implementation of the operation we present a simple example. in order to reinforce the reader s intuition about this operator Consider two copies of a. component P which are prevented from synchronising on their common activity by the. intervening hiding operator This model is transformed as shown below. The definition of the implementation of the hiding operator follows The definition is stated. in terms of the hiding of a single name and is expressed in terms of the use of a hiding. operator on a PEPA sublanguage expression which of course does not use hiding This. has the consequence that it enforces the application of multiple uses of the hiding operation. to begin with the removal of inner applications and proceed outwards The extension from. our description in terms of a single hidden name to hiding a set of names is routine When. representing an expression where is hidden we first choose a fresh identifier say i and. perform the substitution represented below,E F i E i F i. where A0 E i if A E,A i A if Act A,8 Conclusions and further work. One part of our structural analysis of PEPA models which deserves further study is the. treatment of repeated components which suffers from the limitation that it does not exploit. any of the symmetry which is implicit in such a model Improving this aspect of the analysis. is a suitable direction for futher study, In Petri nets the notion of implicit places is used to assist with the structural determination. of deadlock freedom We have identified no corresponding notion for process algebra based. modelling and the investigation of the usefulness of a related concept also remains as future. We have suggested a separation of the analysis of performance models of distributed. computer systems into an initial structural analysis followed by a subsequent performance. analysis As yet these two phases in the modelling and analysis process are not integrated. in the sense that there is no means by which the modeller can take information which is. obtained in the structural analysis into the performance analysis phase The purpose of. passing this information forward to the next phase would be for exploitation perhaps in order. to make an efficiency saving in the computation of properties such as system throughput or. component utilisation Such a connection between these two phases of the analysis process. could potentially be of great benefit in facilitating the modelling of the generation of more. complex computer and communication systems which are being developed with the increase. in communication capacity and availability and the recent vastly increased use of mobile.

Faculty of Economic and Management Sciences Dean: Prof S du Plessis BCom, BComHons (Stell), MPhil (Cambridge), PhD (Stell) CALENDAR 2016 PART 10. Economic and Management Sciences i Calendar Amendments, liability and accuracy In this publication any expression signifying one of the genders includes the other gender equally, unless inconsistent with the context. The University reserves the right ...

SYLLABUS FOR B.COM DEGREE PROGRAM UNDER CBCS w.e.f. 2017-18 B.COM. (GENERAL) COURSE STRUCTURE SEMESTER I CATEGORY PAPER CC 1 General Management CC 2 Financial Accounting CC 3 Micro Economics CC 4 Commercial Arithmetic I AECC 1 Spoken English AECC 2 Environmental Studies I GE 1 Computer Application I/ Geography/ Commerce -

Income & Deductions 3 Deducting sales tax instead of income tax may be beneficial if you reside in a state with no, or low, income tax or you purchased a major item, such as a car or boat. Home-related breaks Consider both deductions and exclusions in your tax planning: Property tax deduction. As noted above, through 2025 your

Deducting sales tax instead of income tax may be beneficial if you reside in a state with no, or low, income tax or you purchased a major item, such as a car or boat. Home-related breaks Consider both deductions and exclu-sions in your tax planning: Property tax deduction. As noted earlier, through 2025 your property tax

tax. For some, traditional IRA contributions are also pre-tax, but high income earners who contribute to retirement plans at work generally cannot deduct traditional IRA contributions. SUZANNE L. SHIER Chief Wealth Planning and Tax Strategist KENNETH LITTLE Associate Tax Counsel This Wealth Planning Insights highlights year-end strategies for

Effects of Income Tax Changes on Economic Growth William G. Gale Brookings Institution and Tax Policy Center Andrew A. Samwick Dartmouth College and NBER

How to Save tax for FY 2017-18? By Amit Founder - Apnaplan.com Version 1.0 Edited: April 4, 2017 Incorporates changes made in Income Tax laws in Budget presented on February 1, 2017

science disciplines. Many excellent published style manuals for scienti?c exist for graduate students and professional scienti?c writiers. The guidelines presented here are largely based upon the CBE Style Manual (Huth et al 1994), and we provide suggestions as to other useful published writing guides. How to Use This Guide We provide this website as a introductory guide for writing a ...