A Hierarchy of Failures-Based Models

AbstractIn this paper we identify the failures class, a class of semantic models for describing concurrent systems. Each such model records all possible sequences of interaction, and gives some information about subsequent availability. Each model is associated with a predicate that determines how much availability information is recorded.The general contribution of the paper is three-fold: we identify the relative strengths of models in terms of their defining predicates; we identify the maximal subset of the language over which each model induces a congruence; and we show how refinement in each model can be automatically tested.More concretely, we apply these general results to specific instances of the class. In particular we construct a spectrum showing the relative strengths of four established models and three interesting new models, and we prove that only Roscoe's stable failures and traces models define congruences over the whole language