Abstract
Often in Software Engineering a modelling formalism has to support scenarios of inconsistency in which several requirements either reinforce or contradict each other. Paraconsistent transition systems are proposed in this paper as one such formalism: states evolve through two accessibility relations capturing weighted evidence of a transition or its absence, respectively. Their weights come from a specific residuated lattice. A category of these systems, and the corresponding algebra, is defined providing a formal setting to model different application scenarios. One of them, dealing with the effect of quantum decoherence in quantum programs, is used for illustration purposes.

Abstract
In the algebraic specification of software systems, it is desirable to have freedom in the implementation process, namely for the software reuse. In this paper we will discuss two issues in order to achieve this freedom: we study the observational stepwise refinement process and we propose an alternative formalization of the refinement concept based on the logical translation from the abstract algebraic logic. In the first topic, we go beyond the traditional assumption of maintaining the set of observable sorts during the refinement process by the possibility of changing it between the process steps, i.e., we analise the stepwise refinement with encapsulation and desencapsulation of sorts during the process. In the second topic, we suggest a formalization of the refinement concept where an equation may be mapped into a set of equations, against the refinements based on signature morphisms, where an equation is mapped into another one.

Abstract
The development of more flexible and robust models for reasoning about systems in environments with potentially conflicting information is becoming more and more relevant in different contexts. In this direction, we recently introduced paraconsistent transition systems, i.e. transition systems whose transitions are tagged with a pair of weights, one standing for the degree of evidence that the transition exists, another weighting its potential non existence. Moreover, these structures were endowed with a modal logic [3] that was further formalised as an institution in [5]. This paper goes a step further, proposing an approach for the structured specification of paraconsistent transition processes, i.e. paraconsistent transition systems with initial states. The proposed approach is developed along the lines of [12], which introduced a complete methodology for (standard) reactive systems development building on the Sannella and Tarlecki stepwise implementation process. For this, we enrich the logic with dynamic modalities and hybrid features, and provide a pallet of constructors and abstractors to support the development process of paraconsistent processes along the entire design cycle.

Abstract
Modal logics are successfully used as specification logics for reactive systems. However, they are not expressive enough to refer to individual states and reason about the local behaviour of such systems. This limitation is overcome in hybrid logics which introduce special symbols for naming states in models. Actually, hybrid logics have recently regained interest, resulting in a number of new results and techniques as well as applications to software specification. In this context, the first contribution of this paper is an attempt to 'universalize' the hybridization idea. Following the lines of [15], where a method to modalize arbitrary institutions is presented, the paper introduces a method to hybridize logics at the same institution-independent level. The method extends arbitrary institutions with Kripke semantics (for multi-modalities with arbitrary arities) and hybrid features. This paves the ground for a general result: any encoding (expressed as comorphism) from an arbitrary institution to first order logic (FOL ) determines a comorphism from its hybridization to FOL. This second contribution opens the possibility of effective tool support to specification languages based upon logics with hybrid features. © 2011 Springer-Verlag.

Abstract
Refinement by interpretation replaces signature morphisms by logic interpretations as a means to translate specifications and witness refinements. The approach was recently introduced by the authors [M. A. Martins, A. Madeira, and L. S. Barbosa. Refinement via interpretation. In Proc. of 7th IEEE Int. Conf. on Software Engineering and Formal Methods, Hanoi, Vietnam, November 2009. IEEE Computer Society Press] in the context of equational specifications, in order to capture a number of relevant transformations in software design, reuse and adaptation. This paper goes a step forward and discusses the generalization of this idea to deductive systems of arbitrary dimension. This makes possible, for example, to refine sentential into equational specifications and the latter into modal ones. Moreover, the restriction to logics with finitary consequence relations is dropped which results in increased flexibility along the software development process.

Abstract
Traditional notions of refinement of algebraic specifications, based on signature morphisms, art often too rigid to capture a number of relevant transformations in the context of software design, reuse and adaptation. This paper proposes an alternative notion of specification refinement, building on recent work on logic interpretation. The concept is discussed, its theory partially developed, its use illustrated through a number of examples.