Personal tools
You are here: Home Events Abstract Archives 2005 A hierarchy of failures-based semantic models

A hierarchy of failures-based semantic models

Christie Bolton University of St Andrews 4pm Tuesday 14th June 2005 Room 2511, JCMB, King's Buildings

In this talk 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 talk 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.

Document Actions