Analyzing equivalences of UML statechart diagrams by structural congruence and open bisimulations

We illustrate how UML statechart diagrams as distinct from statecharts are formalized in the π-calculus as a number of processes which communicate via a channel-passing interaction paradigm. Different types of equivalences of statechart diagrams, including isomorphism, strong behavioural equivalence and weak behavioural equivalence are defined in terms of structural congruence, strong open bisimulation and weak open bisimulation of the π-calculus. Checking equivalence of any two statechart diagrams is transformed to a problem of verifying whether the corresponding π-calculus process expressions are equivalent.