Strong model matching for nite state machines with non-deterministic reference model