(Last modified Fri Jun 06 00:02 2008)

FSP (Finite State Processes) is a textual notation for labeled transition systems (LTSs), developed by Jeff Magee and Jeff Kramer and described in their excellent book Magee+Kramer2006-csmj.  An LTS is a finite state machine whose transitions betweens states are labeled with actions.  FSP is used to describe them, rather than diagrams, because

• a complex state machine drawn as a diagram is difficult to work with and reason about, and state machines describing actual systems quickly become complex;  and
• FSP is conveniently machine-readable as well as human-readable, so that an LTS in FSP is easy for automated tools, and in fact FSP has a specialized tool LTSA (Labeled Transition System Analyzer) that can be downloaded or run from the web page. 

FSP is particularly useful for describing and analyzing concurrent systems, in which several processes run in parallel.  Each process is described with an LTS, and the system as a whole is described as the parallel composition of its processes' LTSs. 

Analyzing an FSP specification

To analyze a specification with FSP and LTSA:

1. Express the specification as a LTS in FSP. 
2. Define a property by making another, simple FSP model that goes to the state -1 if the property is violated. 
3. Compose the two models. 
4. Model-check the composition with LTSA to see if the state -1 is reachable. 

The FSP language

Each process has an alphabet whose symbols are the names of the actions the process recognizes.  All of the actions in the process's definition are in its alphabet.  In addition, extra symbols can be added to the alphabet as a way of saying what the process does not do:  the process recognizes such symbols but has no action that it can take for them. 

Actions are either input actions that come from the process's environment, or output actions that originate from the process.  FSP doesn't distinguish the two types of actions, but you will need to when you define the process. 

The processes are described recursively in terms of themselves and each other, which takes some getting used to but is the source of FSP's expressive power. 

By convention, action names (in the alphabet of a process) are lower-case, and process names are upper-case. 

Predefined processes

STOP is the predefined process that takes no further actions. 

ERROR is the predefined process that transitions to the state -1 and takes no further actions. 

Action prefix

Figure 1.  Firecracker

If x is an action, and P is a process, then the action prefix (x->P) is a process that consists of x followed by P. 

Example:  Figure 1 shows a LTS specifying a firecracker.  It takes one action (named boom) and thereafter does nothing else.  This automaton is written in FSP as (boom->STOP). 

Figure 2.  On-off switch

Example:  Figure 2 shows a LTS specifying a light switch.  This automaton can written in FSP as the three processes

ON and OFF are defined through mutual recursion. 

The same process can be written equivalently and more simply by inlining ON as

or by inlining both ON and OFF as

Choice

If x and y are actions and P and Q are processes, then (x->P|y->Q) is a process that either does (x->P) or (y->Q).  Another way of thinking of it is that the process's future behavior is determined by whether x or y is the next thing that happens:  if x, then thereafter P, and if y, then thereafter Q. 

Figure 3.  Brownie or cookie choice

Example:  Figure 3 shows a machine that dispenses either a brownie or a cookie, depending on which button (square or circular) is pressed.  It can be described by the FSP processes

If the actions x and y are the same, then the result is a non-deterministic choice. 

Figure 4.  Brownie or cookie surprise

Example:  Figure 4 shows a machine that dispenses either a brownie or a cookie when its single button (marked "surprise") is pressed, but there's no telling which will come out.  It can be described by the FSP processes

Indexed actions and processes

Figure 5.  Three treats

YUM dispensed two kinds of treats;  what about an analogous machine that dispenses three kinds, or 23 kinds?  That would be a tedious LTS to express and to analyze.  FSP provides indexed actions and indexed processes to simplify repetitively-structured LTSs.  A finite set of related actions is named x.0, x.1, ... , x.n and then referred to as either x[i] for some integer i∈0..n, or with a variable i as x[i], with i bound to a particular range.  Process names are indexed the same way. 

Example:  Figure 5 shows a machine that dispenses one of three treats when the corresponding button is pushed.  It can be described by the FSP process

Note how i is bound to an integer in the range 1 to 3 in the button action, then reused later as the treat index. 

Note also that the diagram for the three-treats machine is already getting a bit complicated, and that for a 23-treat machine the diagram would be challenging;  but the FSP process would still be quite manageable and understandable: 

FSP also supports range types and constant types so that a single range or constant can be reused in several processes through a range variable: 

And finally, process parameters can be used to define processes with a limit that may vary.  The parameter must have a default value and its name must begin with a capital letter. 

Guarded actions in a choice

The actions in a choice can also be guarded in order to make specific choices be conditional on the current state.  The guards are integer comparisons, resulting in a boolean value.  The integer values are typically propagated through process parameters. 

If (x->P|y->Q) is a choice, then (when B x->P|y->Q) is a choice that can follow either x->P or y->Q if B is true, but otherwise can only follow y->Q. 

Example:  The FSP processes below describe a machine that dispenses brownies or cookies while keeping track of how many it has left.  By default, it initially has 5 of each. 

Process alphabets

As noted above, each process has an alphabet (its actions).  The alphabet can be extended to explicitly show actions that the process cannot engage in.  The extra symbols are shown by following the process definition with +{...}. 

Example:  We would like to save money by making one control panel for the YUM and SURPRISEYUM machines.  The panel would have all the buttons needed by either machine:  circle, square, and surprise.  YUM would be extended as

Parallel composition

Figure 6.  Beep and honk in parallel

The great strength of FSP is in modeling and analyzing concurrency, which is expressed through parallel composition of two or more processes.  If P and Q are processes, then (P||Q) is a process representing their parallel composition, or all possible interleavings of P and Q. 

If a parallel composition is named, its name must begin with ||. 

Example:  Figure 6 shows a machine that beeps once, a machine that honks once, and their parallel composition (with all interleavings of their actions).  The possible interleavings are: 

• A beep followed by a honk (beep->honk). 
• A honk followed by a beep (honk->beep). 

The parallel composition is described by these FSP process:

If an action appears in both processes, then it is a shared action and both processes must engage in it simultaneous (or not at all) in their parallel composition.  For example, an elevator can move up or down or stop, and its doors can open and close.  In a safe elevator, the doors can only open when the elevator is stopped.  Below are FSP processes describing an elevator: 

The elevator alternates moving up or down with stopping, and its doors cycle from closed to open and back again.  Since both processes share the action stop, the doors can't open until the elevator has stopped;  and since both processes share the action closed, the elevator can't move up or down again until the doors have closed. 

Now, in order to evaluate ||ELEVATOR, we need to consider what properties we want it to satisfy.  One such property is that the elevator does not move unless the doors are closed.  We write an FSP process that goes to the error state -1 if the elevator moves with its doors open, compose it with ||ELEVATOR, and analyze the result with LTSA to see if it can reach the error state.  One such property might be

References

Magee+Kramer2006-csmj

Jeff Magee and Jeff Kramer.  Concurrency: State models and Java programming.  Second edition.  Wiley, 2006. 

Thomas A. Alspaugh
Assistant Professor, Informatics Dept.
School of Information and Computer Sciences