Behaviour specifications of heterogeneously structured interacting system components in a distributed software architecture are coalgebras based on different endofunctors, whose interaction scenarios must be algebraically specified. We propose to formalise the concrete interaction rules as natural transformations, called coordination laws, and embed these specifications into a bialgebraic representation based on multi-sorted algebraic signatures. If the coordination laws can be transformed into an abstract GSOS format, the approach is compositional, i.e. syntactical operations on the individual components are fully abstract w.r.t. bisimilarity. We obtain resulting operational semantics as a holistic coalgebra, which comprises the behaviour of the individual components and the resulting global behaviour. This guarantees non-intrusiveness for the individual components and, furthermore, enables successive coordination steps building on each other by taking the individual components as initial input and yielding an ultimate compound behaviour as final output.
The recent development of quantum communication protocols calls for adequate modelling and verification techniques, which requires abstracting and focusing on the basic features of quantum concurrent systems, like process algebras have done for their classical counterparts. However, recovering the peculiar observational limitations prescribed by quantum theory has proven to be a challenging task in quantum systems expressing communication and non-determinism. The problem has been found to be in the interaction between quantum and non-determinism. We address it by resorting to schedulers, and we give behavioural equivalences for both branching and linear-time semantics that adheres to the prescriptions of quantum theory. Moreover, we show that the aforementioned difficulties occur also in simple systems that do not allow exchanging qubits via quantum channels.
Approaching reconfigurable systems as structured transition systems, where the states are models in a given institution, is a methodological approach pursued in [17]. The versatility of this approach lies in the assumption that the logic used for configurations can be chosen based on the nature of the system configurations to be developed. Technically, this is supported by using parametric methods to build modal logics on-demand (e.g. [12, 18]). In this paper, we go a step further by assuming that configurations can be governed by different logics, even within the same reconfigurable system. We operationalize this principle for the formal specification of systems by enriching and reshaping the formalism many-logics modal logic [10] within the theory of institutions and by introducing a number of relations between models that preserve logical properties.
We survey one branch of algebraic logic, namely modal semirings. They provide compact algebraic definitions of actions, with choice + and sequential composition · , together with modal operators box and diamond, parametrised by actions, that allow reasoning about successors and predecessors of states/worlds. Particular instances are homogeneous binary relations or sets of finite and infinite non-empty traces under fusing concatenation. As main examples of applications we present obstacle analysis for geographic wayfinders, Hoare Logic, O’Hearn’s Incorrectness Logic, General Correctness Logic, as well as the temporal logic ^* and its sublogics and . We also give glimpses at Epistemic Logics of belief and knowledge, pointer structures plus Separation Logic and preference database queries. Finally, we briefly discuss some related algebraic approaches.
Formal learning theory poses the question of how agents should use observations about their environment to arrive at accurate and true conclusions. To answer this question, empirical and formal inquiries have been provided with topological models in Domain Theory [1,16], Formal Learning Theory [3], Epistemology and Philosophy of Science [2,7,15]. The goal of our work is to present the initial steps of how precisely the topological formalization of empirical inquiry may be expressed in terms of abstract model theory. In this framework, following Genin and Kelly [5,6], we define what is a method, as well as verifiability, refutability, decidability and limiting verifiability of a proposition. Furthermore, we define what is an abstract empirical problem, and its solvability. We prove that verifiability, refutability, decidability, and limiting verifiability of a proposition and solvability of a problem are invariant under change of notation.
