Abstract
Cardiovascular diseases remain the leading cause of morbidity and mortality worldwide. Continuous electrocardiographic (ECG) monitoring is essential for prevention and treatment, but conventional approaches based on the need for some voluntary action often limit comfort and adherence in long-term use. This study investigates the feasibility of acquiring ECG signals from a toilet seat interface embedding dry electrodes in the posterior thighs. A total of 30 hospitalised patients with diverse cardiovascular conditions-including arrhythmias, ischemic heart disease, heart failure, structural abnormalities, and aneurysms-were enrolled. Thigh-acquired ECGs were recorded simultaneously with conventional limb-lead signals and analysed for morphology, heart rate variability (HRV), and disease-related clustering. Thigh-based ECGs demonstrated clear P-QRS-T complexes with preserved morphology, allowing reliable extraction of mean templates and HRV metrics. The comparison between pathological and normal groups showed that post-surgical aortic repair patients had ECG profiles closest to the normal cluster; in contrast, aortic stenosis (AS) appeared most distant. HRV analysis revealed disease-specific autonomic patterns: patients with tricuspid or mitral involvement exhibited higher variability (SDNN up to 140 ms), whereas those with aortic valve disease presented markedly reduced parasympathetic indices (RMSSD and pNN50). Principal component analysis of multi-feature ECG data identified overlapping groups of Acute Coronary Syndrome, Unstable Angina and Ascending Aortic Aneurysm. At the same time, hierarchical clustering confirmed the distinct separation of conditions with severe hemodynamic disruption, such as PS and AS. These findings support the feasibility of unobtrusive thigh-based ECG monitoring via a toilet-seat interface, enabling reliable signal acquisition, HRV analysis, and preliminary patient stratification. This approach may lay the groundwork for future home-based cardiovascular screening and telemedicine applications.

Abstract
This special issue showcases state-of-the-art research at the intersection of analytics and retail operations. As the retail landscape becomes increasingly complex - driven by omnichannel strategies, evolving customer expectations, and a surge in data availability - analytics has emerged as a critical enabler of operational efficiency, customer experience, responsiveness, and sustainability and ethics. Collectively, these contributions demonstrate how advanced analytics can support retailers in navigating uncertainty, personalizing services, and scaling up innovation across formats and channels. The articles featured in this issue address a diverse set of decision domains, including warehousing, inventory and assortment planning, and distribution and last-mile delivery. Methodologically, they span descriptive, prescriptive, and hybrid approaches, leveraging tools such as machine learning, stochastic modeling, and dynamic optimization. By grounding models in real-world data and focusing on practical implementation, the issue provides actionable insights for both scholars and practitioners. It also highlights emerging opportunities for future research on behavioral integration, human-machine collaboration, and the ethical dimensions of retail analytics.

Abstract
In this paper, we introduce a novel approach for rigorously verifying safety properties of state machine specifications. Our method leverages an auto-active verifier and centers around the use of action functions annotated with contracts. These contracts facilitate inductive invariant checking, ensuring correctness during system execution. Our approach is further supported by the Why3-do library, which extends the Why3 tool's capabilities to verify concurrent and distributed algorithms using state machines. Two distinctive features of Why3-do are: (i) it supports specification refinement through refinement mappings, enabling hierarchical reasoning about distributed algorithms; and (ii) it can be easily extended to make verifying specific classes of systems more convenient. In particular, the library contains models allowing for message-passing algorithms to be described with programmed handlers, assuming different network semantics. A gallery of examples, all verified with Why3 using SMT solvers as proof tools, is also described in the paper. It contains several auto-actively verified concurrent and distributed algorithms, including the Paxos consensus algorithm.

Abstract
Ambient intelligence (AmI) refers to environments where smart devices, sensors, and AI-driven systems work seamlessly to enhance human interactions with their surroundings. Through the combination of real-time data, context-awareness, and adaptive learning, AmI enables environments to respond proactively to user needs, improving efficiency, comfort, and decision-making. However, since AmI systems are inherently human-centric and often operate autonomously, they must be designed with robust ethical, privacy, and safety considerations. Ensuring that these systems function reliably, fairly, and without harm is crucial, especially in sensitive domains like healthcare, security, and smart infrastructure. This work introduces a novel tool, conceptualized as an AmI Digital Twin, which allows developers to simulate or monitor AmI data streams, and develop and thoroughly test AmI applications before and during their real use. Built on a modular architecture leveraging technologies like React.js, Node.js, Kafka, Faust, MongoDB, InfluxDB, Grafana, and Docker, the platform ensures adaptability to different application environments, scalability, and ease of deployment. Besides the description of the tool itself, we provide some early validation results in common AmI tasks such as anomaly and concept drift detection. The tool is available in a public repository, and comes pre-packaged with a set of applications for AmI use-cases. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

Abstract
The increasing energy demand in seaport operations, driven by electrification and decarbonisation targets, requires enhanced tools for operational planning and flexibility management. This paper proposes a novel centralised Energy Management System designed for seaports, which, unlike previous approaches that mainly focused on cost minimisation jointly optimises Battery Energy Storage System scheduling, energy and reserve market participation, and carbon-intensity reduction. A key contribution of this work is the integration of CO\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$_2$$\end{document} emission forecasts and day-ahead market data into a multi-objective formulation, allowing the Energy Management System not only to minimise operational costs but also to reduce indirect emissions. Additionally, a Traffic Light system is proposed to support operators' decision-making by providing actionable flexibility guidelines. A case study based on real-world data from the Port of Sines shows that this method achieves at least an 17% reduction on an annual basis compared to baseline operations, while ensuring cost efficiency. Results highlight the Energy Management System's potential as a decision-support tool for port authorities seeking to align operational efficiency with sustainability goals.

Abstract
When the available data for a target domain is limited, transfer learning (TL) methods leverage related data-rich source domains to train and evaluate models, before deploying them on the target domain. However, most TL methods assume fixed levels of labeled and unlabeled target data, which contrasts with real-world scenarios where both data and labels arrive progressively over time. As a result, evaluations based on these static assumptions may not reflect how methods perform in practice. To support a more realistic assessment of TL methods in dynamic settings, we propose an evaluation framework that (1) simulates varying data availability over time, (2) creates multiple domains via resampling of a given dataset and (3) introduces inter-domain variability through controlled transformations, e.g., including time-dependent covariate and concept shifts. These capabilities enable the systematic simulation of a large number of variants of the experiments, providing deeper insights into how algorithms may behave when deployed. We demonstrate the usefulness of the proposed framework by performing a case study on a proprietary real-world suite of card payment datasets. To support reproducibility, we also apply the framework on the publicly available Bank Account Fraud (BAF) dataset. By providing a methodology for evaluating TL methods over time and in different data availability conditions, our framework supports a better understanding of model behavior in real-world environments, which enables more informed decisions when deploying models in new domains.