Full-abstraction for client testing preorders

Abstract

Client testing preorders relate tests (clients) instead of processes (servers), and are usually defined using either must testing or a compliance relation. Existing characterisations of these preorders are unsatisfactory for they rely on the notion of usable clients which, in turn, are defined using an existential quantification over the servers that ensure client satisfaction. In this paper we characterise the set of usable clients wrt must testing for finite-branching LTSs, and give a sound and complete decision procedure for it. We also provide novel coinductive characterisations of the client preorders due to must and compliance, which we use to show that these preorders are decidable, thus positively answering the question opened in.