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>Py>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
(PQ) 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 
{a_{1},..,a_{x}}::P
replaces every label n
in the alphabet of P
with the labels a_{1}.n,…,a_{x}.n. Further,
every transition (n>Q)
in the definition of P
is replaced with the transitions ({a_{1}.n,…,a_{x}.n}>Q). 
Priority High << 
C =(PQ)<<{a_{1},…,a_{n}} specifies
a composition in which the actions a_{1},…,a_{n}
have higher priority than any other action in the alphabet of PQ
including the silent action tau. In any choice in this
system which has one or more of the actions a_{1},…,a_{n} labeling
a transition, the transitions labeled with lower priority actions are
discarded. 
Priority Low >> 
C=(PQ)>>{a_{1},…,a_{n}} specifies
a composition in which the actions a_{1},…,a_{n}
have lower priority than any other action in the alphabet of PQ
including the silent action tau. In any choice in this
system which has one or more transitions not labeled by a_{1},…,a_{n}, the
transitions labeled by a_{1},…,a_{n} 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. 
Relabeling / 
Relabeling is applied to a process to change the names of
action labels. The general form of relabeling is: 
Hiding \ 
When applied to a process P, the hiding
operator \{a_{1}..a_{x}}
removes the action names a_{1}..a_{x}
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 @{a_{1}..a_{x}}
hides all actions in the alphabet of P not labeled in the set a_{1}..a_{x}. 
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 =
{a_{1},a_{2}..a_{n}} defines
a progress property P which asserts that in an infinite execution of a
target system, at least one of the actions a_{1},a_{2}..a_{n}
will be executed infinitely often. 
Table A.4 – Safety and Progress Properties
Fluent 
fluent FL = <{s_{1},…s_{n}}, {e_{1}..e_{n}}> 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 {s_{1},…s_{n}}occur and false immediately any of the
terminating actions {e_{1}..e_{n}}
occur. If the term initially B is omitted then FL is initially false. 
Assertion 
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