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
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
Event/data-based systems are controlled by events, their local data state may change in reaction to events. Numerous methods and notations for specifying such reactive systems have been designed, though with varying focus on the different development steps and their refinement relations. We first briefly review some of such methods, like temporal/modal logic, TLA, UML state machines, symbolic transition systems, CSP, synchronous languages, and Event-B with their support for parallel composition and refinement. We then present E. -logic for covering a broad range of abstraction levels of event/data-based systems from abstract requirements to constructive specifications in a uniform foundation. E. -logic uses diamond and box modalities over structured events adopted from dynamic logic, for recursive process specifications it offers (control) state variables and binders from hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. Constructive operational specifications given by state transition graphs can be characterised by a single E. -sentence. Also a variety of implementation constructors is available in E. -logic to support, among others, event refinement and parallel composition. Thus the whole development process can rely on E. -logic and its semantics as a common basis.

Abstract
A wide range of methods from computer science are being applied to many modern engineering domains, such as synthetic biology. Most behaviors described in synthetic biology have a hybrid nature, in the sense that both discrete or continuous dynamics are observed. Differential Dynamic Logic (dL) is a well-known formalism used for the rigorous treatment of these systems by considering formalisms comprising both differential equations and discrete assignments. Since the many systems often consider a range of values rather than exact values, due to errors and perturbations of observed quantities, recent work within the team proposed an interval version of dL, where variables are interpreted as intervals. This paper presents the first steps in the development of computational support for this formalism by introducing a tool designed to models based on intervals, prepared to translate them into specifications ready to be processed by the KeYmaera X tool.

Abstract