Observational structures and their logic (Q1190494)

The authors present a general framework for defining semantics of datatypes which include higher-order objects and processes. Processes are viewed as elements of observable sorts in algebraic structures and their semantics is defined in terms of observational structures which specify how processes are observed. Various modal observational logics can be associated to an observational structure. The approach presented in this paper extends some classical results concerning observational equivalences and Hennessy-Milner logic for \(CCS\)-like processes [\textit{M. Hennessy} and \textit{R. Milner}, J. Assoc. Comput. Mach. 32, 137-161 (1985; Zbl 0629.68021)].