Abstract
In the last decades, dynamic logics have been used in different domains as a suitable formalism to reason about and specify a wide range of systems. On the other hand, logics with many-valued semantics are emerging as an interesting tool to handle devices and scenarios where uncertainty is a prime concern. This paper contributes towards the combination of these two aspects through the development of a method for the systematic construction of many-valued dynamic logics. Technically, the method is parameterised by an action lattice that defines both the computational paradigm and the truth space (corresponding to the underlying Kleene algebra and residuated lattices, respectively).

Abstract
The wide number of languages and programming paradigms, as well as the heterogeneity of ‘programs’ and ‘executions’ require new generalisations of propositional dynamic logic. The dynamisation method, introduced in [20], contributed on this direction with a systematic parametric way to construct Many-valued Dynamic Logics able to handle systems where the uncertainty is a prime concern. The instantiation of this method with the Lukasiewicz arithmetic lattice over [0, 1], that we derive here, supports a general setting to design and to (fuzzy-) reason about systems with uncertainty degrees in their transitions. For the verification of real systems, however, there are no de facto methods to accommodate exact truth degrees or weights. Instead, the traditional approach within scientific community is to use different kinds of approximation techniques. Following this line, the current paper presents a framework where the representation values are given by means of intervals. Technically this is achieved by considering an ‘interval version’ of the Kleene algebra based on the [0, 1] Lukasiewicz lattice. We also discuss the ‘intervalisation’ of L action lattice (in the lines reported in [28]) and how this class of algebras behaves as an (interval) semantics of many-valued dynamic logic. © Springer International Publishing AG 2016.

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
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
On-line applications and services are now a critical part of our everyday life. Using these services typically requires us to trust our personal or company's information to a large number of third-party entities. These entities enforce several security measures to avoid unauthorized accesses but data is still stored on common database systems that are designed without data privacy concerns in mind. As a result, data is vulnerable against anyone with direct access to the database, which may be external attackers, malicious insiders, spies or even subpoenas. Building strong data privacy mechanisms on top of common database systems is possible but has a significant impact on the system's resources, computational capabilities and performance. Notably, the amount of useful computation that may be done over strongly encrypted data is close to none, which defeats the purpose of offloading computation to third-party services. In this paper, we propose to shift the need to trust in the honesty and security of service providers to simply trust that they will not collude. This is reasonable as cloud providers, being competitors, do not share data among themselves. We focus on NoSQL databases and present SafeRegions, a novel prototype of a distributed and secure NoSQL database that is built on top of HBase and that guarantees strong data privacy while still providing most of HBase's query capabilities. SafeRegions relies on secret sharing and multiparty computation techniques to provide a NoSQL database built on top of multiple, non-colluding service providers that appear as a single one to the user. Strikingly, service providers, individually, cannot disclose any of the user's data but, together, are able to offer data storage and processing capabilities. Additionally, we evaluate SafeRegions exposing performance trade-offs imposed by security mechanisms and provide useful insights for future research on performance optimization.

Abstract
In the pursuit of highly available systems, storage systems began offering eventually consistent data models. These models are suitable for a number of applications but not applicable for all. In this paper we discuss a system that can offer a eventually consistent data model but can also, when needed, offer a strong consistent one.