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