Exploiting independence in exploring state spaces

A Linear Process Specification (LPS) uses data variables to represent
the states of the underlying labelled transition system. Exploring (and
thereby constructing) this transition system requires replacing these
variables with concrete values and generating all transitions leading
to successor states. In deciding whether there is a transition from
one state to the next, not all variables are involved. The assignment
involves investigating whether this observation can be used to speed up
the exploration of the underlying transition system. Possible directions
include the use of parallelism to generate independent chuncks of the
state space, or the use of more clever and compact representations of
parts of the transition system. Further directions for research include
investigating whether similar techniques can be used in the context of
parameterised Boolean equation systems (PBESs).