* Taking the CTL properties generated above as a specification, the model-checker can be used to determine whether some reactions can be removed without changing those CTL properties
* Here, the decomplexation reactions are shown to be unnecessary for the CTL specification obtained by generate_ctl.
Not surprinsingly, eliminating the dephosphorylation reactions produce a stiffer response of the cascade, but preserves its main qualitative properties.