We use History Dependent Automata (HD-automata) as a syntax-indepentend formalism to check compatibility of services at binding time in Service-Oriented Computing. Informally speaking, service requests are modelled as pairs of HD-auo, Cr ; Cr describes the (abstract) behaviour of the searched service and Co the (abstract) behaviour guaranteed by the invoker. Symmetrically, service publication consists of a pair of HD-automata So, Sr t So provides an (abstraction of) of the behaviour guaranteed by the service and Sr yields the requirement imposed to invokers. An invocation Co, Cr matches a published interface So, Sr when Co simulates Sr and So simulates Cr.