Two extensions of the partial order reduction algorithm of Clarke, Jha and Marrero are presented. The proposed algorithms are suitable for branching security protocols, e.g. optimistic fair contract signing schemes. The first extension is proved to generate a reduced state space which is branching bisimilar to the full state space, while the second extension generates a state space that is trace equivalent to the full state space. Experimental results using an implementation of the algorithms in the toolset of the µCRL process algebra are reported.
|Title of host publication||Proceedings 10th International Conference on Application of Concurrency to System Design (ACSD'10, Braga, Portugal, June 21-25, 2010)|
|Publisher||IEEE Computer Society|
|Publication status||Published - 2010|