Integrating observational and computational features in the specification of state-based, dynamical systems (Q2747940)

State-based, dynamical systems comprise a computational aspect, concerned with the computations yielding new systems states and with the reachability of states under computations, and an observational aspect, concerned with the observations that can be made about existing system states and with the indistinguishability of states by observations. These two aspects overlap, in that features concerned with the evolution of system states can be regarded both as a means to compose new states and as a means to observe existing states. There exist, however, system features whose nature is either purely computational or purely observational, with the construction of initial states and respectively the extraction of visible information from system states being instances of such features. NEWLINENEWLINENEWLINEExisting approaches to system specification typically exploit the overlap between computational and observational features to employ either algebraic or coalgebraic techniques for specification and reasoning. Such a choice limits the expressiveness of these formalisms w.r.t. either observational or computational features. In particular, observers with structured result types cannot be accommodated by algebraic approaches, whereas constructors with structured argument types cannot be accommodated by coalgebraic approaches. Furthermore, in the presence of constructors with multiple arguments, additional constraints are needed to guarantee that observational equivalence relations are preserved by such constructors. Finally, existing approaches to system specification do not consider ensuring that the system observers preserve the reachability of states under computations. The present paper aims to fully exploit the expressive power of algebra and coalgebra when specifying purely computational and respectively purely observational structures, and to combine their complementary contributions when specifying structures that have both computational and observational features, in a manner which guarantees a certain compatibility between the two categories of features. NEWLINENEWLINENEWLINESection 1 of the paper introduces a coalgebraic equational framework for the specification of observational structures. Section 2 derives an (essentially dual) algebraic framework for the specification of computational structures. Section 3 integrates the two frameworks in order to account for structures having both an observational and a computational component.