zbMATH — the first resource for mathematics

Synchronous and asynchronous experiments on processes. (English) Zbl 0544.68028
Summary: A language for processes is defined in which there are two methods of synchronising subprocesses called loose synchronisation and tight synchronisation. A notion of experimenting on processes is introduced which leads to definitions of when a process may pass an experiment and when it must pass an experiment. By connecting the experimenter to the process using the tight synchronisation then three preorders on processes called the synchronous preorders are defined. By using the loose synchronisation primitive, the asynchronous preorders are defined. For each of these preorders it is proved that there exists a fully abstract model in the sense of Scott. These models are defined using sets of equations and lead automatically to complete proof systems. Moreover the proof of full abstractness uses an alternative characterisation of these preorders which gives an intuitive understanding for the denotations in the model.

68Q65 Abstract data types; algebraic specification
68N25 Theory of operating systems
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI