Abstract
This article presents Pardinus, an extension of the popular Kodkod relational model finder with linear temporal logic (including past operators), to simplify the analysis of dynamic systems. Pardinus includes a SAT-based bounded-model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counter-examples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines.

Abstract
Label noise is omnipresent in the annotations process and has an impact on supervised learning algorithms. This work focuses on the impact of label noise on the performance of learning models by examining the effect of random and class-dependent label noise on a binary classification task: quality assessment for photoplethysmography (PPG). PPG signal is used to detect physiological changes and its quality can have a significant impact on the subsequent tasks, which makes PPG quality assessment a particularly good target for examining the impact of label noise in the field of biomedicine. Random and class-dependent label noise was introduced separately into the training set to emulate the errors associated with fatigue and bias in labeling data samples. We also tested different representations of the PPG, including features defined by domain experts, 1D raw signal and 2D image. Three different classifiers are tested on the noisy training data, including support vector machine (SVM), XGBoost, 1D Resnet and 2D Resnet, which handle three representations, respectively. The results showed that the two deep learning models were more robust than the two traditional machine learning models for both the random and class-dependent label noise. From the representation perspective, the 2D image shows better robustness compared to the 1D raw signal. The logits from three classifiers are also analyzed, the predicted probabilities intend to be more dispersed when more label noise is introduced. From this work, we investigated various factors related to label noise, including representations, label noise type, and data imbalance, which can be a good guidebook for designing more robust methods for label noise in future work.

Abstract
Production scheduling generates a direct impact on several aspects of manufacture, such as the number of delays in delivery to customers, total flow time, as well as the percentage of equipment used. It must, therefore, constitute a priority in production management, which should seek to implement scheduling techniques that will lead to positive results from the perspective of the quality of the solution. However, the methodology cannot overlook the functional aspect of the time which has elapsed until the solution is reached. This study is based on a real and specific module software improvement into a company devoted to the development of ERP software systems (Enterprise Resource Planning). It presents a solution for the production scheduling module focused on flow-shop operations, comprising a total of nine dispatching rules. An additional solution for scheduling is also proposed, which resorts to metaheuristic simulated annealing. Both solutions are compared to each other by using the quality-functionality binomial approach. These two environments are further contrasted with a third, where no effective solution for production scheduling exists. The environment which includes scheduling through dispatching rules was compared to the environment where no production scheduling was implemented. The results obtained from this analysis show an improvement of 13%. The simulated annealing solution presents an improvement of 3,6% when compared to a solution which uses dispatching rules. This improvement implies one extra minute in the calculation of the final solution.

Abstract
Energy management in buildings can be largely improved by considering adequate forecasting techniques to find load consumption patterns. While these forecasting techniques are relevant, decision making is needed to decide the forecasting technique that suits best each context, thus improving the accuracy of predictions. In this paper, two forecasting methods are used including artificial neural network and k-nearest neighbor. These algorithms are considered to predict the consumption of a building equipped with devices recording consumptions and sensors data. These forecasts are performed from five-to-five minutes and the forecasting technique decision is taken into account as an enhanced factor to improve the accuracy of predictions. This decision making is optimized with the support of the multi-armed bandit, the reinforcement learning algorithm that analyzes the best suitable method in each five minutes. Exploration alternatives are considered in trial and test studies as means to find the best suitable level of unexplored territory that results in higher accumulated rewards. In the case-study, four contexts have been considered to illustrate the application of the proposed methodology.

Abstract

Abstract
This paper proposes an innovative framework based on optimisation techniques that can support decision-making in water services. The proposed models estimate a Best-Practice frontier recurring to a ‘Benefit-of-the-Doubt’ formulation that enables benchmarking performance across decision-making units. We propose an innovative estimation of a pseudo-Malmquist index to compare the performance of groups. The framework’s relevance is illustrated using data of the Brazilian water and sanitation regulator, collected at the municipality level for the year 2019. The groups compared correspond to three Brazilian macro-regions. The results obtained show that the Southeast exhibits the best overall performance. The Northeast has a few municipalities with the best practices at a national level, but this macro-region has significant heterogeneity in performance levels. The South has a more homogeneous performance, but the best-performing municipalities in this macro-region are still far from Brazil’s best practices. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.