# Compression¶

Compression converts a labelled-transition system (LTS) into an equivalent LTS that, hopefully, is smaller and thus more efficient to use in a check. Generally, one of the many compression functions that FDR provides is applied to a component of a parallel composition. For example, normal is one commonly-used compression functions, as could, for instance be applied as normal(Q) ||| R. Compression will have little affect on a process that contains no hiding. Thus, it makes sense to compress a process that has just had a significant amount of hiding applied to it. For example, if P \ A is used at some point in a system and A contains a large number of the events P can perform, then compressing P \ A may significantly reduce size of the system that needs to be verified. Intuitively, compression removes the hidden events in such a way as to preserve sufficient behaviour, but not too much. This also implies that it is worth hiding as much as possible as early as possible (i.e. as far down the process tree as possible), since that gives compression more options to remove events.

Note it is not worth compressing a whole system. For example, when verifying if Q is deadlock-free, there is no point in verifying normal(Q) is deadlock-free instead, since FDR has to traverse the whole of Q to construct the normalised version anyway.

FDR provides many compression functions, as listed in Compression Functions, all of which are CSPM functions of type (Proc) -> Proc. Generally, the most useful functions to apply are normal, wbisim, and the function sbdia(P) = sbisim(diamond(P)) which combines sbisim and diamond. Further advice on how to choose a compression function is given in Compression Functions, but note that it is difficult to predict in advance which compression function will be most effective, and thus some experimentation will be required. The best method of assessing the effectiveness of compressions is to use the machine structure viewer, which can display details regarding the number of states and transitions that are saved by compression.

A more advanced usage of compression is inductive compression. In this, the system is constructed in stages, with each intermediate stage being compressed. For example, when modelling a token ring, only the events on the very left-most and very right-most processes must not be hidden. Therefore, the system can be constructed inductively by taking the existing system, adding one more node, hiding the events between the old system and the new node, and then compressing it. Understanding Concurrent Systems describes this in more detail. Further, the file Inductive Compression contains some utility functions, written by Roscoe, for constructing systems in such a way.