Reachability anaysis may also be performed when the components are specified as extended state machines. For the "finite state aspect" of the specifications, the reachability analysis approach discussed above can be used, while the difficulty comes from the conditions that must be satisfied by the interaction parameters and values of the additional state variables. This involves usually to write these conditions as assertions associated with the different states of the "finite state aspect" of the global model, and then verifying that these assertions hold in all reachable states of the system. Two approaches may be used toverify that these assertions always hold::

- Such verification may be sometimes performed by proving that these assertions hold. Hand-proofs, or assisted by theorem provers, are difficult to do, especially for complex systems.
**Examples:**The alternating bit protocol, specified in an extended state machine model, is discussed in my paper from 1977. The example of a queue with users is an example without a "major state" (only variables).

- Use reachability analysis tools that have support for proving assertions, and possible temporal logic formulas (such as Uppaal or Spin). Such tools are normally called "model checkers".
- Some tools explore all possible values for input parameters (which leads to a blow-up of the number of reachable states). One often verifies simplified system specifications where the range of parameters and local variables are reduced to a small number (e.g. reduce the sequence numbering space from long integers to the range 0 .. 5).
- Other tools support symbolic evaluations, which reduces the number of cases to consider, but each case is much more complex to process.

The main difficulty of reachability is the so-called** state space explosion**, meaning that the number of reachable states grows very large. There are three reasons why often the number of reachable states is too big to be manageable, even with powerful tools:

- The number of states of each component is very large because one has introduced supplementary state variables (extended models) for capturing the behavior of the sub-system, e.g. sequence numbers in protocols.
- During reachability analysis, one considers the Cartesian product of several components, which leads to a multiplication of the number of states of all the components.
- An additional “blow-up” normally due to the varying number of messages in transit (even if this number is often artificially bounded during analysis).

This state space explosition represents a problem for reachability analysis, since it is necessary to remember which global states have already been encountered (and analysed). When a new transition from the currently explored state is executed, one has to record the next global state reached and determine whether it was encountered before, or whether it is a new global state (that must be explored). The easiest way is to store all global states that have been encountered together with a boolean flag which indicates whether all transitions from this state have already been explored or not. Each global state contains the states of each component, all messages in transit (i.e. in queues) together with their parameter values, and the values of the local state variables of all components. Therefore each global state may easily require a good number of octets to store. Since memory is limited, the number of states that can be explored is limited.

The number of reachable states in not only often very large, in many cases it is even infinite. Consider for instance an FSM that has a spontaneous transition that sends a message to its partner and loops back to the same state. In this case, the number of message that may be in transit at any given time is not bounded. Therefore the number of global reachable states is infinite. Clearly such spaces cannot be covered completely. The question is: Is it necessary to explore global states with an arbitrary number of messages in transit ? - In practice, one usually explores only states with a number of messages in transit within a bound. But it is not clear what such a bound should be. Sometimes the reachability analysis shows (if a complete exploration has been done) that the number of messages in transit from a given source component to some given destination component is always less than same bound. However, it has been shown that the problem of deciding whether two given communication state machines may get into a deadlock state is undecidable. Also the question whether the number of messages in transit remains bounded is undecidable.

Holzmann (the author of Spin) proposed a method for minimizing the required memory for remembering which global state has already been analyzed (using only one bit per state). In his paper of 1986 he proposed to consider the representation of a global state as the address (in memory) for a single bit. This bit is set to 1 when the state has been explored. When a new transition is explored, the bit at the address indicated by the next state is checked to see if it has the value 1 (which means that the state was encountered before). If the state space is large, there may still not be enough memory to store a bit for all possible global states (note that not all possible global states will be reachable- therefore most bits will remain with a value 0). Therefore Holzmann proposed to hash the value of the global state into the address space of the available memory. This is called state hashing. - This, however, is not perfect, since different global states may hash to the same value, which means that if the bit for the next state explored is already set to 1, it means that either this state was encountered before, or there is a hash conflict with another global state that was encountered before (but the currently explored state is actually new). Since one cannot distinguish between these two cases, one assumes that the explored state was encountered before and will not be further explored. Therefore this leads to randomly partial exploration of the reachable state space of the system under analysis.

Analysis methods that __do not construct__ the whole reachable global state space, but only travel through the whole space (for instance through a depth-first search) and __simultaneously check__ the interesting properties are called “on-the-fly” analysis methods. In opposition, traditional methods construct the whole state space and then check the interesting properties.

The following approaches have been proposed to reduce the effect of state space explosion:

**Problem decomposition**(e.g. analyze different operational phases separately)**Reduced reachability analysis:**The idea is to reduce the number of different interleavings of concurrent activities that must be considered, but taking care that one still maintains the guarantee that all design errors will be detected**Ad-hoc analytical methods:**Ad-hoc methods may be used for showing that certain types of properties are satisfied for certain types of specifications. They often depend on the particular form of the behavior specification.**Analysis using assertions**(in the case of extended state machines): The idea is to treat the properties related to the variables using program proof methods involving assertions and/or invariants. See for example in my paper from 1977.**Incomplete analysis:**For instance- partial exploration of the reachable state space (e.g. random walk [Holz 88]);
- statistical exploration corresponding to the probabilities of the real environment;
- exploration by simulation guided by the user (this is always possible as long as the specification is executable)

Created: October 2014