Behavioral equivalence of hidden k-logics: an abstract algebraic approach

This work advances a research agenda which has as its main aim the application of Abstract Algebraic Logic (AAL) methods and tools to the specification and verification of software systems. It uses a generalization of the notion of an abstract deductive system to handle multi-sorted deductive systems which differentiate visible and hidden sorts. Two main results of the paper are obtained by generalizing properties of the Leibniz congruence — the central notion in AAL. In this paper we discuss a question we posed in [1] about the relationship between the behavioral equivalences of equivalent hidden logics. We also present a necessary and sufficient intrinsic condition for two hidden logics to be equivalent.

Reuse and integration of specification logics: the hybridisation perspective

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. It also captures the construction of first-order encodings of such hybridised institutions into theories in first-order logic. The method was originally developed to build suitable logics for the specification of reconfigurable software systems on top of whatever logic is used to describe local requirements of each system’s configuration. Hybridisation has, however, a broader scope, providing a fresh example of yet another development in combining and reusing logics driven by a problem from Computer Science. This paper offers an overview of this method, proposes some new extensions, namely the introduction of full quantification leading to the specification of dynamic modalities, and exemplifies its potential through a didactical application. It is discussed how hybridisation can be successfully used in a formal specification course in which students progress from equational to hybrid specifications in a uniform setting, integrating paradigms, combining data and behaviour, and dealing appropriately with systems evolution and reconfiguration.

Energy systems analysis of transboundary river basins in a nexus approach: the Sava river basin study case

Resource management policies are frequently designed and planned to target specific needs of particular sectors, without taking into account the interests of other sectors who share the same resources. In a climate of resource depletion, population growth, increase in energy demand and climate change awareness, it is of great importance to promote the assessment of intersectoral linkages and, by doing so, understand their effects and implications. This need is further augmented when common use of resources might not be solely relevant at national level, but also when the distribution of resources ranges over different nations. This dissertation focuses on the study of the energy systems of five south eastern European countries, which share the Sava River Basin, using a water-food(agriculture)-energy nexus approach. In the case of the electricity generation sector, the use of water is essential for the integrity of the energy systems, as the electricity production in the riparian countries relies on two major technologies dependent on water resources: hydro and thermal power plants. For example, in 2012, an average of 37% of the electricity production in the SRB countries was generated by hydropower and 61% in thermal power plants. Focusing on the SRB, in terms of existing installed capacities, the basin accommodates close to a tenth of all hydropower capacity while providing water for cooling to 42% of the net capacity of thermal power currently in operation in the basin. This energy-oriented nexus study explores the dependency on the basin’s water resources of the energy systems in the region for the period between 2015 and 2030. To do so, a multi-country electricity model was developed to provide a quantification ground to the analysis, using the open-source software modelling tool OSeMOSYS. Three main areas are subject to analysis: first, the impact of energy efficiency and renewable energy strategies in the electricity generation mix; secondly, the potential impacts of climate change under a moderate climate change projection scenario; and finally, deriving from the latter point, the cumulative impact of an increase in water demand in the agriculture sector, for irrigation. Additionally, electricity trade dynamics are compared across the different scenarios under scrutiny, as an effort to investigate the implications of the aforementioned factors in the electricity markets in the region.