Extending mCRL2 with ready simulation and iocos input-output conformance simulation

The mCRL2 toolset is a leading tool for the use of formal methods. It integrates modelling, analysis and verification methods and techniques strongly based on up to date research results and algorithms. In this paper we describe an extension of mCRL2 that integrates two branching semantics initially not present at the original bundle, the classic ready simulation and the newer input-output conformance simulation (iocos). We use systems from the Very Large Transition Systems (VLTS) benchmark, with states ranging from 103 to 106, to check the implementations and to compare the results with the simpler simulation semantics already included in mCRL2. The results show the feasibility and applicability of the ready and iocos semantics introduced in mCRL2. The good results, in general, highlights the interest of the family of branching semantics for their use in formal methods.