Observational structures and their logic

AbstractA poweful paradigm is presented for defining semantics of data types which can assign sensible semantics also to data representing processes. Processes are abstractly viewed as elements of observable sort in an algebraic structure, independently of the language used for their description. In order to define process semantics depending on the observations we introduce observational structures, essentially first-order structures where we specify how processes are observed. Processes are observationally related by means of experiments considered similar depending on a similarity law and relations over processes are propagated to relations over elements of non-observable sort by a propagation law. Thus an observational equivalence is defined, as union of all observational relations, which can be seen as a very abstract generalization of bisimulation equivalences introduced by David Park.Though being general and abstract our construction allows to extend and improve interesting classical results. For example it is shown that for finitely observable structures the observational equivalence is obtainable as a limit of a denumerable chain of iterations; our conditions, which apply to algebraic structures in general, when instantiated in the case of labelled transition systems, are more liberal than the finitely branching condition. More importantly, we show how to associate with an observational structure various modal observational logics, related to sets of experiment schemas, that we call pattern sets. The main result of the paper proves that for any family of pattern sets representing the simulation law the corresponding modal observational logic is a Hennessy—Milner logic: two observable objects are observationally equivalent if and only if they satisfy the same set of modal observational formulas. Indeed observational logics generalize to first-order structures various modal logics for labelled transition systems. Applications are shown to multilevel parallelism, higher-order concurrent calculi, distributed and branching bisimulation.The theory presented in the paper is not at all confined to give semantics of processes. Indeed it provides a general semantic paradigm for abstract data type specifications, where some data are processes. In order to support this claim, in the final section we briefly consider algebraic specifications and give small examples of specifications integrating processes, data types and functions