Introduction to PSF

Process Expressions

In the following we list possible constructions for process expressions and describe their behaviour. Parentheses may be used to group process expressions.
atomic action  a
Execution of the atomic action a.

internal step  skip
Execution of an internal step not visible to the environment. In ACP based extensions it is known as tau.

deadlock  delta
A deadlock cannot be executed.

process  P
The process P will be replaced by an alternative composition of all the process definitions of which the left hand side matches with P.

sequential composition  x . y
Process expression x is executed and upon termination followed by the execution of process expression y.

alternative composition  x + y
A non-deterministic choice between process expressions x and y is made. Choosing a deadlock is forbidden.

parallel composition  x || y
The process expressions x and y are executed in parallel in which possible communications can take place.

generalized alternative composition  sum(v in S, x)
An abbreviation of the alternative composition of, for every value of v in the sort or set S, the process expression x in which v is replaced by the value.

generalized parallel composition  merge(v in S, x)
An abbreviation of the parallel composition of, for every value of v in the sort or set S, the process expression x in which v is replaced by the value.

encapsulation  encaps(H, x)
Can only execute actions from process expression x that are not an element of set H.

hiding  hide(I, x)
Let the executed actions from process expression x behave as the internal step skip.

conditional expression  [t = u] -> x
If the terms t and u are equal, the conditional expression evaluates to the process expression x, and to deadlock otherwise.
In addition to the above described process constructions, PSF also has the following constructions.
interruption  interrupt(x, y)
The executions of process expression x can be interrupted by process expression y at any time. After the execution of process expression y has finished, the execution of process expression x resumes.

disruption  disrupt(x, y)
The execution of process expression x can be interrupted by process expression y at any time. After the execution of process expression y has finished, instead of continueing the execution of process expression x, the execution of the whole process expression is finished.

priority  prio(S1 > ... > Sn, x)
Gives priority of actions in process expression x that appear in set Si over actions that appear in set Sj for j > i. This means that when there is a choice between actions only the actions with the highest priority and the actions without a priority can be chosen. With the priority operator, the use of the keyword atoms is extended to not only denote the set type atoms, but also to denote the set of all atomic actions. The process expression prio(S ,x) is an abbreviation of prio(S > atoms, x).

iteration  x * y
Chooses between process expressions x and y. If x is chosen, upon termination of the execution of x the iteration is repeated. If y is chosen, upon termination of the execution of y the iteration finishes.

nesting  x # y
Chooses between process expressions x and y. If x is chosen, upon termination of the execution of x the nesting is repeated. If y is chosen, upon termination of the execution of y, x is executed the number of times x has been chosen.