Abstract
A key feature of model finding techniques allows users to enumerate and explore alternative solutions. However, it is challenging to guarantee that the generated instances are relevant to the user, representing effectively different scenarios. This challenge is exacerbated in quantitative modelling, where one must consider both the qualitative, structural part of a model, and the quantitative data on top of it. This results in a search space of possibly infinite candidate solutions, often infinitesimally similar to one another. Thus, research on instance enumeration in qualitative model finding is not directly applicable to the quantitative context, which requires more sophisticated methods to navigate the solution space effectively. The main goal of this paper is to explore a generic approach for navigating quantitative solution spaces and showcase different iteration operations, aiming to generate instances that differ considerably from those previously seen and promote a larger coverage of the search space. Such operations are implemented in QAlloy - a quantitative extension to Alloy - on top of Max-SMT solvers, and are evaluated against several examples ranging, in particular, over the integer and fuzzy domains.

Abstract
The rapid advancement of wireless technologies, particularly Wi-Fi, has spurred significant research into indoor human activity detection across various domains (e.g., healthcare, security, and industry). This work explores the non-invasive and cost-effective Wi-Fi paradigm and the application of deep learning for human activity recognition using Wi-Fi signals. Focusing on the challenges in machine interpretability, motivated by the increase in data availability and computational power, this paper uses explainable artificial intelligence to understand the inner workings of transformer-based deep neural networks designed to estimate human pose (i.e., human skeleton key points) from Wi-Fi channel state information. Using different strategies to assess the most relevant sub-carriers (i.e., rollout attention and masking attention) for the model predictions, we evaluate the performance of the model when it uses a given number of sub-carriers as input, selected randomly or by ascending (high-attention) or descending (low-attention) order. We concluded that the models trained with fewer (but relevant) sub-carriers are competitive with the baseline (trained with all sub-carriers) but better in terms of computational efficiency (i.e., processing more data per second).

Abstract
Background: Online psychological interventions like behavioural activation (BA) can be provided with or without human support. Unguided online interventions require no human contact and are therefore easier to implement on a large scale than guided interventions. However, effectiveness and adherence rates to these interventions are generally lower. One way to increase adherence to unguided online interventions is to offer automated motivational support. Objective: This pilot randomized controlled trial (RCT) examined whether adherence to unguided online BA for low mood could be improved by adding automated support in the form of smartphone-delivered personalized motivational messages or a motivational virtual coach. Methods: A three-arm pilot RCT (n = 106) was conducted that compared an online intervention delivered with automated motivational support by a virtual coach (n = 35), or by automated personalized messages on their smartphone (n = 35), to the same intervention without support (control condition; n = 36). The primary outcome was level of adherence, operationalized as (1) the number of webpages of the intervention visited, and (2) the number of mood ratings completed on the smartphone application, both retrieved from participants' logfiles. Secondary outcomes were satisfaction with the intervention (CSQ-I), usability (SUS) depression scores (HADS), and motivation for treatment (SMFL), measured through online questionnaires administered at baseline or after 4 weeks. Results: Adherence was moderate overall, with participants visiting on average 23 pages of 55 webpages and completing on average 50 of 84 requested mood ratings. No evidence for differences in adherence rates were observed between the intervention conditions and the control condition. Satisfaction with the intervention was moderate to high. Usability scores were below the desirable threshold of 68. Depression symptoms did not change significantly across all participants (p = .053). No significant changes in motivation were found over time or between groups. Conclusions: Adding automated support to unguided online BA for depression did not improve overall adherence. The limited effectiveness may reflect a misalignment between the motivational strategies and the needs of the target population, who reported mild symptoms and high intrinsic motivation. The findings highlight the need to further improve both the quality of automated support and the usability of online platforms. Future research should explore additional adherence-related factors and investigate how personalization can better address different symptom severities in unguided mental health interventions. Trial registration: International Clinical Trials Registry Platform: trialsearch.who.int/Trial2.aspx?TrialID=NL8110. © 2025 The Authors

Abstract
In 2023, global kiwifruit production reached over 4.4 million tonnes, highlighting the crop's significant economic importance. However, achieving high yields depends on adequate pollination. In Actinidia species, pollen is transferred by insects from male to female flowers on separate plants. Natural pollination faces increasing challenges due to the decline in pollinator populations and climate variability, driving the adoption of assisted pollination methods. This study examines the Portuguese kiwifruit sector, one of the world's top 12 producers, using a novel mixed-methods approach that integrates both qualitative and quantitative analyses to assess the feasibility of robotic pollination. The qualitative study identifies the benefits and challenges of current methods and explores how robotic pollination could address these challenges. The quantitative analysis explores the cost-effectiveness and practicality of implementing robotic pollination as a product and service. Findings indicate that most farmers use handheld pollination devices but face pollen wastage and application timing challenges. Economic analysis establishes a break-even point of €685 per hectare for an annual single application, with a first robotic pollination of €17 146 becoming cost-effective for orchards of at least 3.5 hectares and a second robotic solution of €34 293 becoming cost-effective for orchards up to 7 hectares. A robotic pollination service priced at €685 per hectare per application presents a low-risk and a viable alternative for growers. This study provides robust economic insights supporting the adoption of robotic pollination technologies. This study is crucial to make informed decisions to enhance kiwifruit production's productivity and sustainability through precise robotic-assisted pollination. © 2025 Elsevier B.V., All rights reserved.

Abstract
Developing information retrieval (IR) systems that enable access across multiple languages is crucial in multilingual contexts. In Timor-Leste, where Tetun, Portuguese, English, and Indonesian are official and working languages, no cross-lingual information retrieval (CLIR) solutions currently exist to support information access across these languages. This study addresses that gap by investigating CLIR approaches tailored to the linguistic landscape of Timor-Leste. Leveraging an existing monolingual Tetun document collection and ad-hoc text retrieval baselines, we explore the feasibility of CLIR for Tetun. Queries were manually translated into Portuguese, English, and Indonesian to create a multilingual query set. These were then automatically translated back into Tetun using Google Translate and several large language models, and used to retrieve documents in Tetun. Results show that Google Translate is the most reliable tool for Tetun CLIR overall, and the Hiemstra LM consistently outperforms BM25 and DFR BM25 in cross-lingual retrieval performance. However, overall effectiveness remains up to 26.95% points lower than that of the monolingual baseline, underscoring the limitations of current translation tools and the challenges of developing an effective CLIR for Tetun. Despite these challenges, this work establishes the first CLIR baseline for Tetun ad-hoc text retrieval, providing a foundation for future research in this under-resourced setting. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

Abstract
Cancer is a leading cause of mortality worldwide, with breast and lung cancer being the most prevalent globally. Early and accurate diagnosis is crucial for successful treatment, and medical imaging techniques play a pivotal role in achieving this. This paper proposes a novel pipeline that leverages generative artificial intelligence to enhance medical images by combining synthetic image generation and super-resolution techniques. The framework is validated in two medical use cases (breast and lung cancers), demonstrating its potential to improve the quality and quantity of medical imaging data, ultimately contributing to more precise and effective cancer diagnosis and treatment. Overall, although some limitations do exist, this paper achieved satisfactory results for an image size which is conductive to specialist analysis, and further expands upon this field's capabilities.