Abstract
Formal verification can be a complementary approach to UCD, offering a systematic and repeatable process to address the demands of designing safety and mission-critical interactive systems. However, the practical application of formal verification often encounters barriers to accessibility for non-technical stakeholders. In the case of model checking, although the verification step is fully automated, developing the required specifications and interpreting the verification results requires considerable technical expertise in formal methods. Recent developments in generative Artificial Intelligence (AI) have driven proposals for Large Language Models (LLMs) to be applied throughout various phases of software engineering. This begs the question of whether LLMs might be used to help bridge the gap between formal techniques and tools and stakeholders lacking technical expertise. This paper explores how these questions might be addressed in the context of an ongoing effort aimed at translating model-checking counter-examples into natural language explanations, making them accessible to designers and domain experts.

Abstract
Within the context applied to Virtual Reality research, the present work focuses on a literature review within the emerging field of Transformative Experience Design. The review focuses on studies that have adopted a strongly empirical, phenomenological and qualitative approach to the creation and evaluation of transformative experiences in VR, with the purpose of finding out not only how these are being created, but also which are the main factors that enable a transformative dimension in this type of experiences. The results present a number of possible stimuli regarding the most prominent dimensions of awe and the sublime found in the literature: perceptual vastness and need for accommodation. These results are then systematized and discussed, and further possibilities are then suggested within this context. © 2025. Published by AHFE Open Access. All rights reserved.

Abstract
The sustainable utilization of forest biomass for bioenergy production is increasingly challenged by the variability and unpredictability of raw material availability. These challenges are particularly critical in regions like Central Portugal, where seasonality, dispersed resources, and wildfire prevention policies disrupt procurement planning. This study investigates two flexibility strategies-dynamic network reconfiguration and operations postponement-as policy relevant tools to enhance resilience in forest-to-bioenergy supply chains. A novel mathematical model, the mobile Facility Location Problem with dynamic Operations Assignment (mFLP-dOA), is proposed and solved using a scalable matheuristic approach. Applying the model to a real case study, we demonstrate that incorporating temporary intermediate nodes and adaptable processing schedules can reduce costs by up to 17% while improving operational responsiveness and reducing non-productive machine time. The findings offer strategic insights for policymakers, biomass operators, and regional planners aiming to design more adaptive and cost-effective biomass supply systems, particularly under environmental risk scenarios such as summer operation bans. This work supports evidence-based planning and investment in flexible logistics infrastructure for cleaner and more resilient bioenergy supply chains.

Abstract
Interest in artificial intelligence (AI)-driven crowd work has increased during the last few years as a line of inquiry that expands upon prior research on microtasking to represent a means of scaling up complex tasks through AI mediation. Despite the increasing attention to the macrotask phenomenon in crowdsourcing, there is a need to understand the processes, elements, and constraints underlying the infrastructural and behavioral aspects in such form of crowd work when involving collaboration. To this end, this paper provides a first attempt to characterize some of the research conducted in this direction to identify important paths for an agenda comprising key drivers, challenges, and prospects for integrating human-centered AI in collaborative crowdsourcing environments.

Abstract
Community-based electricity markets, which are defined as groups of members that share common interests in renewable distributed generation, allow prosumers to embrace more active roles by opening up several opportunities for trading electricity. At the same time, such markets may favor conventional consumers by allowing them to choose cheaper electricity providers. Due to trends in power sector modernization, community-based electricity markets are of great research interest, and there are already some associated models. However, there is a research gap in searching for integrated and holistic approaches that go beyond economic aspects, consider social and environmental aspects, and assume the balanced co-existence of community-based and conventional markets. This work fills this critical research gap by adapting/applying the optimized tariff model, Bass diffusion model, life cycle assessment, and multi-objective optimization to the context of community-based markets. Results indicate that favoring conventional markets in the short term and community-based markets in the medium term is beneficial. Moreover, regulated tariffs should increase slightly in the short/medium-term to accommodate DG growth. Additionally, community-based markets can decrease electricity expenses by around 13.6 % considering the market participants. Thus, such markets can be significantly beneficial in mitigating energy poverty.

Abstract
Pruning consists on an agricultural trimming procedure that is crucial in some species of plants to promote healthy growth and increased yield. Generally, this task is done through manual labour, which is costly, physically demanding, and potentially dangerous for the worker. Robotic pruning is an automated alternative approach to manual labour on this task. This approach focuses on selective pruning and requires the existence of an end-effector capable of detecting and cutting the correct point on the branch to achieve efficient pruning. This paper reviews and analyses different end-effectors used in robotic pruning, which helped to understand the advantages and limitations of the different techniques used and, subsequently, clarified the work required to enable autonomous pruning.