Appendix A

FSP Quick Reference

A.1 Processes

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

A.2 Composite Processes

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

A.3 Common Operators

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

A.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

A.5 FLTL – Fluent Linear Temporal Logic

Fluent fluent	fluent FL = <{s1,…sn}, {e1..en}> initially B defines a fluent FL that is initially true if the expression B is true and initially false if the expression B is false. FL becomes true immediately any of the initiating actions {s1,…sn}occur and false immediately any of the terminating actions {e1..en} occur. If the term initially B is omitted then FL is initially false.
Assertion assert	assert PF = FLTL_Expression defines an FLTL property.
&&	conjunction (and)
||	disjunction (or)
!	negation (not)
->	implication ((A->B)º (!A || B))
<->	equivalence ((A<->B) º(A->B)&&(B->A))
next time X F	iff F holds in the next instant.
always []F	iff F holds now and always in the future.
eventually <>F	iff F holds at some point in the future.
until P U Q	iff Q holds at some point in the future and P holds until then.
weak until P W Q	iff P holds indefinitely or P U Q
forall	forall [i:R] FL(i) conjunction of FL(i)
exists	exists [i:R] FL(i) disjunction of FL(i)

Table A.5 – Fluent Linear Temporal Logic