Abstract
Predictive Maintenance applications are increasingly complex, with interactions between many components. Black-box models are popular approaches based on deep-learning techniques due to their predictive accuracy. This paper proposes a neural-symbolic architecture that uses an online rule-learning algorithm to explain when the black-box model predicts failures. The proposed system solves two problems in parallel: (i) anomaly detection and (ii) explanation of the anomaly. For the first problem, we use an unsupervised state-of-the-art autoencoder. For the second problem, we train a rule learning system that learns a mapping from the input features to the autoencoder's reconstruction error. Both systems run online and in parallel. The autoencoder signals an alarm for the examples with a reconstruction error that exceeds a threshold. The causes of the signal alarm are hard for humans to understand because they result from a non-linear combination of sensor data. The rule that triggers that example describes the relationship between the input features and the autoencoder's reconstruction error. The rule explains the failure signal by indicating which sensors contribute to the alarm and allowing the identification of the component involved in the failure. The system can present global explanations for the black box model and local explanations for why the black box model predicts a failure. We evaluate the proposed system in a real-world case study of Metro do Porto and provide explanations that illustrate its benefits. © 2024

Abstract
This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-Aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step.In this paper, we describe preliminary work on using LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, we attempt to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-Aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties. © 2024 Copyright held by the owner/author(s).

Abstract
At a time when European countries try to cope with escalating energy prices while decarbonizing their economies, waste heat recovery and reuse arises as part of the solution for sustainable energy transitions. The lack of appropriate assessment tools has been pointed out as one of the main barriers to the wider deployment of waste heat recovery projects and as a reason why its potential remains largely untapped. The EMB3Rs platform emerges as an online, open-source, comprehensive and novel tool that provides an integrated assessment of different types of waste heat recovery solutions, (e.g. internal or external) and comprises several analysis dimensions (e.g. physical, geographical, technical, market, and business models). It has been developed together with stakeholders, and tested in a number of representative contexts, covering both industrial and heat network applications. This has demonstrated the enormous potential of the tool in dealing with complex simulations, while delivering accurate results within a significantly lower time-frame than traditional analysis. The EMB3Rs tool removes important barriers such as analysis costs, time and complexity for the user, and aims at supporting a wider investment in waste heat recovery and reuse by providing an integrated estimation of the costs and benefits of such projects. This paper describes the tool and illustrates how it can be applied to help unlock the potential of waste heat recovery across European countries. © 2024 Elsevier Ltd

Abstract
Nearest neighbor search (NNS) is one of the main concerns in data stream applications since similarity queries can be used in multiple scenarios. Online NNS is usually performed on a sliding window by lazily scanning every element currently stored in the window. This paper proposes Sliding Window-based Incremental Nearest Neighbors (SWINN), a graph-based online search index algorithm for speeding up NNS in potentially never-ending and dynamic data stream tasks. Our proposal broadens the application of online NNS-based solutions, as even moderately large data buffers become impractical to handle when a naive NNS strategy is selected. SWINN enables efficient handling of large data buffers by using an incremental strategy to build and update a search graph supporting any distance metric. Vertices can be added and removed from the search graph. To keep the graph reliable for search queries, lightweight graph maintenance routines are run. According to experimental results, SWINN is significantly faster than performing a naive complete scan of the data buffer while keeping competitive search recall values. We also apply SWINN to online classification and regression tasks and show that our proposal is effective against popular online machine learning algorithms.

Abstract
Despite the ubiquitous term climate neutral cities, there is a distinct lack of quantifiable and meaningful municipal decarbonization goals in terms of the targeted energy balance and composition that collectively connect to national scenarios. In this paper we present a simple but useful allocation approach to derive municipal targets for energy demand reduction and renewable expansion based on national energy transition strategies in combination with local potential estimators. The allocation uses local and regional potential estimates for demand reduction and the expansion of renewables and differentiates resulting municipal needs of action accordingly. The resulting targets are visualized and opened as a decision support system (DSS) on a web-platform to facilitate the discussion on effort sharing and potential realization in the decarbonization of society. With the proposed framework, different national scenarios, and their implications for municipal needs for action can be compared and their implications made explicit.

Abstract