PEPA Atomic Formalism
Möbius supports PEPA as an atomic modeling formalism. PEPA is a process algebra. Instead of creating a PEPA atomic model in a graphical editor, the model is created using an editor provided in Möbius in a form that resembles a formal language. Möbius extends the basic PEPA language to include process parameters, guards, and value passing. This extension is known as the PEPAk language.
The PEPAk language
This section covers the basic building blocks of the PEPAk language including process variables, formal parameters, guards, choices, prefixes, hide, and cooperation.
- Process Variable: In the PEPAk language, processes are represented using process variables. A process variable is defined by assigning an equation to a symbolic name using the assignment operator “”. For example, the following defines the process variable :
- Formal Parameters: The PEPAk language extends PEPA to include the possibility of formal parameters for process variables. In the example above the process variable takes a single parameter, . More parameters may be specified by a comma delimited list as follows: .
- Guards: The introduction of guards to the PEPAk language allows the selective enabling and disabling of a process expression based on the guard conditions. A process expression is enabled if its guard evaluates to true, and disabled if its guard evaluates to false. Guards are represented by boolean expressions enclosed in square brackets before a process expression, and may contain references to formal parameters. In the above example, the two process expressions are guarded by conditions, , and && . Thus the first process expression is enabled only if the parameter is greater than five, and the second process expression is enabled only if the parameter is greater than zero and less than five. The guard operator “” assigns a process expression to a given guard expression.
- Choice: The choice operator “” is used to allow a process to behave in different ways under different circumstances as defined by a process expression. The first enabled process expression to complete is selected and the remainder of the expressions are discarded. In the above example we see a choice between two guarded process expressions.
- Prefix: The simplest way to describe the behavior of a process is to add a prefix to the preferences to the process variable. Prefixes are denoted using the form , where is some action which has a duration that is exponentially distributed with rate . After the action has completed, it then behaves according to the referenced process variable. In the case of a choice between multiple enabled processes expressions, it is the activity that completes first which is selected.
- Hide: The hide operator “” is a combinator that is used to hide activities. With respect to a process, the hidden activities are considered silent. As in many other process algebras, the combinator is used to express abstraction.
- Cooperation: Processes and are said to cooperate over a set of shared activities if they contain one or more shared activities and are defined as cooperating over these activities. They are defined as cooperating over an activity through the definition of a new process variable as follows:
- The “” operator is the cooperation operator and takes its parameters as a comma delimited list of activities to be shared between the cooperating processes. If a process enables an activity within the shared set, it will not be able to continue with the activity until the cooperating process also enables this activity. Both processes then complete the shared activity. When defining a prefix for a shared activity, one of the cooperating processes may define it with rate , indicating that it is a passive activity and the duration of the activity is to be determined based on the duration generated by the other cooperating process, illustrated in the following example:
Note that, in order to solve a PEPAk model using any of the Möbius solvers (see Solving Models), the underlying Markov chain must have a finite state space and must be irreducible and ergodic. A necessary (although not sufficient) condition for this is that the model is composed from the processes using the hide or cooperation combinator. These combinators are static in the sense that they are not “destroyed” by activity transitions. The necessary condition ensures that the structure of the model does not grow unboundedly over time.