Finite state systems

We have also conducted experiments with verification of finite state systems via supercompilation. We have tried some of the protocols above for the fixed amount of processors (non-parameterized verification). We used a different, more direct encoding in that case. Typically, it takes few seconds to half a minute to verify a protocol of the modest size (3-5 processors). We believe the power of the prorposed method lies mainly in the area of parameterised verification, and for the case of the finite state systems we could hardly compete with the model checking approach. However, the case of finite state systems verification worth to explore further in order to understand better the proposed method and its area of applicability. More details will follow soon.