Appendix A

FSP Quick Reference

    1. Processes

      2. 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
      when

      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
      Extension       +

      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

    2. Composite Processes

      3. 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
      Composition       ||

      If P and Q are processes then (P||Q) represents the concurrent execution of P and Q.

      Replicator
      forall

      forall [i:1..N] P(i) is the parallel composition (P(1) || ... || P(N))

      Process
      Labeling       :

      a:P prefixes each label in the alphabet of P with a.

      Process
      Sharing       ::

      {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

    3. Common Operators

      4. The operators in Table A.3 may be used in the definition of both processes and composite processes.

      Conditional
      if then else

      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:
      /{newlabel_1/oldlabel_1,... newlabel_n/oldlabel_n}.

      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

    4. Properties

Safety
property

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

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