Abstract
This paper introduces a method to build dynamic logics with a graded semantics. The construction is parametrized by a structure to support both the spaces of truth and of the domain of computations. Possible instantiations of the method range from classical (assertional) dynamic logic to less common graded logics suitable to deal with programs whose transitional semantics exhibits fuzzy or weighted behaviour. This leads to the systematic derivation of program logics tailored to specific program classes.

Abstract
Dynamic logic combines logic with programs, which at a certain level of abstraction, can be regarded as behaviours changing the system state and, therefore, the truth value of formulas. This paper suggests a method for generating such logics for the domain of robot controllers and illustrates it with a logic for handling resource consumption.

Abstract
Reconfigurability, understood as the ability of a system to behave differently in different modes of operation and commute between them along its lifetime, is a cross-cutting concern in modern Software Engineering. This paper introduces a specification method for reconfigurable software based on a global transition structure to capture the system's reconfiguration space, and a local specification of each operation mode in whatever logic (equational, first-order, partial, fuzzy, probabilistic, etc.) is found expressive enough for handling its requirements. In the method these two levels are not only made explicit and juxtaposed, but formally interrelated. The key to achieve such a goal is a systematic process of hybridisation of logics through which the relationship between the local and global levels of a specification becomes internalised in the logic itself.

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
Adding to the modal description of transition structures the ability to refer to specific states, hybrid(ised) logics provide an interesting framework for the specification of reconfigurable systems. The qualifier 'hybrid(ised)' refers to a generic method of developing, on top of whatever specification logic is used to model software configurations, the elements of an hybrid language, including nominals and modalities. In such a context, this paper shows how a calculus for a hybrid(ised) logic can be generated from a calculus of the base logic and that, moreover, it preserves soundness and completeness. A second contribution establishes that hybridising a decidable logic also gives rise to a decidable hybrid(ised) one. These results pave the way to the development of dedicated proof tools for such logics used in the design of reconfigurable systems.

Abstract
Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. In a series of papers this process has been detailed and taken as a basis for a specification methodology for reconfigurable systems. The present paper extends this work by showing how a proof calculus (in both a Hilbert and a tableau based format) for the hybridised version of a logic can be systematically generated from a proof calculus for the latter. Such developments provide the basis for a complete proof theory for hybrid(ised) logics, and thus pave the way to the development of (dedicated) proof support.