Deriving failures models for nonuniform concurrency from structured operational semantics

Semantic models are studied for concurrent languages which are nonuniform in that they involve individual variables which store values, and possible actions of an agent depend on its current state. First, an operational model O-L(T) based on a failures domain is defined from a labeled transition system L(T) which is in turn specified by a set I of rules for deriving transitions. A method is then introduced for deriving a denotational failures model D-T from T when T fits a certain syntactical format, called the Nonuniform Non-Blocking Copy-Free SOS format (NU-NB-CF-SOS format), which is based on the format due to De Simone with certain additional restrictions specific to the nonuniform setting. Both O-L(T) and D-T are constructed by applying the methodology of metric semantics, and the equivalence between D-T and O-L(T) is established by showing that both O-L(T) and D-T are fixed-points of a higher-order mapping, which has a unique fixed-point by Banach's fixed-point theorem.