Model independent order relations for processes

Abstract

Semantic preorders between processes are usually applied in practice to model approximation or implementation relationships. For interactive models these preorders depend crucially on the observational behaviours of processes as well as on the observing power of environments. The paper aims at a model independent observational theory of the semantic preorders for interactive models. Depending on whether environments change dynamically or not, two classes of model independent preorders are formalized. These formalizations are intensively studied in the framework of CCS. Operational characterizations of these preorders are investigated, and the relationships between them are revealed. Several new preorders for CCS are proposed along the way. Behavioural properties are discussed in a model independent manner as far as possible. © 2010 Springer-Verlag.