Appendix A
FSP Quick Reference
A process is defined by a one or more local processes separated by commas. The definition is terminated by a full stop.
STOP and ERROR are primitive local processes.Example
Process = (a -> Local),
Local = (b -> STOP).
Action Prefix -> |
If x is an action and P a process then (x->P) describes a process that initially engages in the action x and then behaves exactly as described by P. |
Choice | |
If x and y are actions then (x->P|y->Q) describes a process which initially engages in either of the actions x or y. After the first action has occurred, the subsequent behavior is described by P if the first action was x and Q if the first action was y. |
Guarded Action |
The choice (when B x -> P | y -> Q) means that when the guard B is true then the actions x and y are both eligible to be chosen, otherwise if B is false then the action x cannot be chosen. |
Alphabet |
The alphabet of a process is the set of actions in which it can engage. P + S extends the alphabet of the process P with the actions in the set S. |
Table A.1 - Process operators
A composite process is the parallel composition of one or more processes. The definition of a composite process is preceded by
||.Example
||Composite = (P || Q).
Parallel |
If P and Q are processes then (P||Q) represents the concurrent execution of P and Q. |
Replicator |
forall [i:1..N] P(i) is the parallel composition (P(1) || ... || P(N)) |
Process |
a:P prefixes each label in the alphabet of P with a. |
Process |
{a1,..,ax}::P replaces every label n in the alphabet of P with the labels a1.n,...,ax.n. Further, every transition (n->Q) in the definition of P is replaced with the transitions ({a1.n,...,ax.n}->Q). |
Priority High << |
||C =(P||Q)<<{a1,...,an} specifies a composition in which the actions a1,...,an have higher priority than any other action in the alphabet of P||Q including the silent action tau. In any choice in this system which has one or more of the actions a1,...,an labeling a transition, the transitions labeled with lower priority actions are discarded. |
Priority Low >> |
||C=(P||Q)>>{a1,...,an} specifies a composition in which the actions a1,...,an have lower priority than any other action in the alphabet of P||Q including the silent action tau. In any choice in this system which has one or more transitions not labeled by a1,...,an, the transitions labeled by a1,...,an are discarded. |
Table A.2 - Composite Process Operators
The operators in Table A.3 may be used in the definition of both processes and composite processes.
Conditional |
The process if B then P else Q behaves as the process P if the condition B is true otherwise it behaves as Q. If the else Q is omitted and B is false, then the process behaves as STOP. |
Re-labeling / |
Re-labeling is applied to a process to change the names of action labels. The general form of re-labeling is: |
Hiding \
|
When applied to a process P, the hiding operator \{a1..ax} removes the action names a1..ax from the alphabet of P and makes these concealed actions "silent". These silent actions are labeled tau. Silent actions in different processes are not shared. |
Interface @ |
When applied to a process P, the interface operator @{a1..ax} hides all actions in the alphabet of P not labeled in the set a1..ax. |
Table A.3 - Common Process Operators
Safety |
A safety property P defines a deterministic process that asserts that any trace including actions in the alphabet of P, is accepted by P. |
Progress |
progress P = {a1,a2..an} defines a progress property P which asserts that in an infinite execution of a target system, at least one of the actions a1,a2..an will be executed infinitely often. |
Table A.4 - Safety and Progress Properties