Proving testing preorders for process algebra descriptions

Process algebras are rapidly becoming a mathematical model used by verification engineers to extend the description capabilities of finite state machines towards higher abstraction levels. As long as design and verification methodologies at the system level are developed the wide spectrum of equivalence relations that can be defined over processes receives an ever increasing importance. Testing equivalences and testing preorders are particularly suited for formalizing the relationships holding in top-down hierarchical methodologies. The main deterrent to the widespread use of process algebras seems to be the lack of efficient tools. Very efficient algorithmic techniques, based on the adoption of binary decision diagrams, are now being used in different fields. This paper presents algorithms for the proof of testing preorders and equivalences that are, to the best of our knowledge, the first successful attempt to implement testing relations with BDDs. Experimental results show that the the implemented algorithms are able to deal with medium and large-size systems