Abstract
Dynamic logic with binders D? has been introduced as an institution for the development of reactive systems based on model class semantics. The satisfaction relation of this logic was, however, not abstract enough to enjoy the modal invariance property (bisimilar models should satisfy the same sentences). We recently overcame this problem by proposing an observational satisfaction relation where the equality on states is interpreted by bisimilarity of states. This entailed, however, a price to pay - the satisfaction condition required for institutions was lost. This paper works on this limitation by establishing a behavioural semantics for D? parametric to behavioural structures - families of equivalence relations on the states of each model. Such structures are taken in consideration in the signature category and, in particular, for the definition of signature morphisms. We show that with these changes we get again an institution with a behavioural model class semantics. The framework is instantiated with specific behavioural structures, resulting in the novel Institution of Crucial Actions. © 2017, Springer International Publishing AG.

Abstract
The dynamic logic with binders D? was recently introduced as a suitable formalism to support a rigorous stepwise development method for reactive software. The commitment of this logic concerning bisimulation equivalence is, however, not satisfactory: the model class semantics of specifications in D? is not closed under bisimulation equivalence; there are D?-sentences that distinguish bisimulation equivalent models, i.e., D? does not enjoy the modal invariance property. This paper improves on these limitations by providing an observational semantics for dynamic logic with binders. This involves the definition of a new model category and of a more relaxed satisfaction relation. We show that the new logic D? ~ enjoys modal invariance and even the Hennessy-Milner property. Moreover, the new model category provides a categorical characterisation of bisimulation equivalence by observational isomorphism. Finally, we consider abstractor semantics obtained by closing the model class of a specification SP in D? under bisimulation equivalence. We show that, under mild conditions, abstractor semantics of SP in D? is the same as observational semantics of SP in D? ~.

Abstract

Abstract
D-down arrow is a new dynamic logic combining regular modalities with the binder constructor typical of hybrid logic, which provides a smooth framework for the stepwise development of reactive systems. Actually, the logic is able to capture system properties at different levels of abstraction, from high-level safety and liveness requirements, to constructive specifications representing concrete processes. The paper discusses its semantics, given in terms of reachable transition systems with initial states, its expressive power and a proof system. The methodological framework is in debt to the landmark work of D. Sannella and A. Tarlecki, instantiating the generic concepts of constructor and abstractor implementations by standard operators on reactive components, e.g. relabelling and parallel composition, as constructors, and bisimulation for abstraction.

Abstract
A 'hybridization' of a logic, referred to as the base logic, consists of developing the characteristic features of hybrid logic on top of the respective base logic, both at the level of syntax (i.e. modalities, nominals, etc.) and of the semantics (i.e. possible worlds). By 'hybridized institutions' we mean the result of this process when logics are treated abstractly as institutions (in the sense of the institution theory of Goguen and Burstall). This work develops encodings of hybridized institutions into (many-sorted) first-order logic (abbreviated FOL) as a 'hybridization' process of abstract encodings of institutions into FOL, which may be seen as an abstraction of the well-known standard translation of modal logic into FOL. The concept of encoding employed by our work is that of comorphism from institution theory, which is a rather comprehensive concept of encoding as it features encodings both of the syntax and of the semantics of logics/institutions. Moreover, we consider the so-called theoroidal version of comorphisms that encode signatures to theories, a feature that accommodates a wide range of concrete applications. Our theory is also general enough to accommodate various constraints on the possible worlds semantics as well a wide variety of quantifications. We also provide pragmatic sufficient conditions for the conservativity of the encodings to be preserved through the hybridization process, which provides the possibility to shift a formal verification process from the hybridized institution to FOL.

Abstract
Quantum algorithmics is emerging as a hot area of research, with the potential to have groundbreaking impacts on many different fields. The benefits come at a high price, however: quantum programming is hard and finding new quantum algorithms is far from straightforward. This area of research may greatly benefit from mathematical foundations and calculi, capable of supporting algorithm development and analysis. The Quantum Algorithmics Agenda at QuantaLab is contributing by seeking a suitable semantics-calculus-logic trilogy for quantum computation.