The use of possibility mappings was originally proposed as a single complete method of refinement for I/O automata by Lynch in [151], and soundness and completeness for automata are discussed by Merrit in [157]. The use of possibility mappings in context of transition systems is given by Gerth in [96] where the resultant rule is called failure simulation and is in essence the same as the relational characterisation we derived above. Other complete refinement methods include Abadi and Lamport's history and prophesy variable approach [1], the relationship between this and possibility mappings is discussed in [157]. Lynch and Vaandrager, [152], provide an overview of simulation methods for untimed and timed automata which surveys the relationship between many of these approaches.
A single complete method can also be derived by using predicate transformers [94] in its formulation. In [94] Gardiner and Morgan show how upward and downward simulations are special cases of their method, which is therefore complete.
The use of possibility mappings in a relational context was discussed briefly in [60] and first appeared in the form given in this chapter in [61].