[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Samples] / PEPA
[Index] [Contents] [Source Text] [About] [Notation] [Copyright] [Comment/Contact] [Search ]
Tue May 1 07:16:32 PDT 2012

Contents


    PEPA -- Performance Evaluation Process Algebra

      Context -- Process Algebras

      [ ../maths/math_73_Process_algebra.html ]

      Source

      [Hillston95]

      Later Source

      [GilmoreHillstonRibaudo01]

      Lexicon

    1. hide::lexeme= "/".
    2. or_choose::lexeme= "+".
    3. precedes::lexeme= ".".
    4. passive_rate_symbol::lexeme=top, this plain "T" symbol can not be rendered in HTML, but looks like an upside down ⊥ (bottom symbol).
    5. unknown_action_symbol::lexeme=τ.

    6. given_action_type::Sets=given.
    7. constants::@identifier=given.

      Concrete Syntax

    8. expression::= hiding | prefix | cooperation | choice | constant | "(" expression ")'.

      The [ Later Source ] gives a two level syntax which seems to have become the standard.

    9. later_syntax::=following
      Net
      1. sequential_component::= action preceeds sequential_component | sequential_component or_choose sequential_component | constant & defined_as_a_sequential_component.

      2. model_component::= model_component "<" set_of_action_types ">" model_component | model_component hide set_of_action_types | constant & defined_as_a_model_component.

        These syntax descriptions do not make precedences and associativity clear or spell out how sequential_components fit with model_components.

        [click here [socket symbol] Later_PEPA if you can fill this hole]


      (End of Net)

      Note. In MATHS the first alternative is the prefered parsing for a string, so hiding takes priority over prefix and

    10. (a,r).P/L = (a,r).(P/L).

    11. hiding::= expression hide set_of_action_types.

    12. prefix::= action precedes expression.
    13. action::="(" action_type, rate ")" .

    14. cooperation::= cooperation "<" set_of_action_types ">" expression|expression, this notation is ASCIIfied and the BNF reflects the assoicativity.

    15. choice::= expression or_choose expression. Note. Choice turns out to be associative so we can take
    16. P+Q+R = (P+Q)+R.

    17. rate::= passive_rate_symbol | Positive&Real, indicates the rate at which the action completes.

    18. set_of_action_types::= "{" list_of_action_types "}".
    19. list_of_action_types::= empty | action_type | list_of_action_types "," action type.
    20. action_type::=given_action_types ~ unknown_action_symbol.

      Constants are defined terms

       A::= P

      Abstract Syntax

    21. P::=(a, r).P | P + Q | P <L> Q | P/ L | A.

    22. P||Q::= P<{}>Q.


    23. (Source)|-
      1. The precedence of the combinators provides a default interpretation of any expression. Hiding has highest precedence with prefix next, followed by cooperation. Choice has the lowest precedence. Brackets may be used to force an alternative parsing or simply to clarify meaning.
      2. ...
      3. When brackets are missing we assume the cooperation combinator associates to the left.

      Semantics

      Semantics are defined using relation (-(a,r)->) between processes and a compositional set of derivation rules. These lead to a Markov process. Assumes that actions take a random time with an exponential distribution.

    24. rate = 1/mean_duration. [ Exponential_distribution ]

      r[a](P) ::gloss=apparent rate of action type a in component P.

    25. |-r[a]((b.r).P) = if(a=b, r, 0).
    26. |-r[a](P+Q) = r[a](P)+r[a](Q).
    27. |-r[a](P/L) = if(a ∈ L, 0, r[a](P) ).
    28. |-r[a](P<L>Q) = if(a ∈ L, min(r[a](P), r[a](Q)), r[a](P)+r[a](Q) ).


    29. |- (PEPA_s1): (a,r).E -(a,r)-> E.


    30. |- (PEPA_s2): If E-(a,r)-> E' then (E+F)-(a,r)-> E' .


    31. |- (PEPA_s3): If F-(a,r)-> F' then (E+F)-(a,r)-> F' .


    32. |- (PEPA_s4a): If E-(a,r)-> E' and a not_in L then (E/L)-(a,r)-> (E'/L) .
    33. |- (PEPA_s4b): If E-(a,r)-> E' and a ∈ L then (E/L)-(τ,r)-> (E'/L) .
    34. |- (PEPA_s4c): If E-(a,r)-> E' and A=E then A-(a,r)-> E' .


    35. |- (PEPA_s5a): If E-(a,r)-> E' and a not_in L then (E<L>F)-(a,r)-> (E'<L>F) .
    36. |- (PEPA_s5b): If F-(a,r)-> F' and a not_in L then (E<L>F)-(a,r)-> (E<L>F') .


    37. |- (PEPA_s5c): If E-(a,r1)-> E' and F-(a,r2)-> F' and a ∈ L and R = (r1/r[a](E))*(r2/r[a](F)) * min (r[a](E),r[a](F) ) then (E<L>F)-(a,R)-> (E<L>F') .

    . . . . . . . . . ( end of section PEPA -- Performance Evaluation Process Algebra) <<Contents | End>>

End