Proving Testing Preorders for Process Algebra Descriptions. Politecnico di

Process Algebras are rapidly becoming a mathe-matical 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 Test-ing Preorders are particularly suited for formalizing the relationships holding in top-down hierarchical meth-odologies. The main deterrent to the widespread use of Process Algebras seems to be the lack of eficient tools. Very eficient 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. Ex-perimental results show that the the implemented al-gorithms are able to deal with medium- and large-size systems. 1