Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

2026

An Explosion of the Uses of Immersive Learning Environments: A Mapping of Reviews Update

Authors
Beck, D; Morgado, L; O'Shea, P;

Publication
IMMERSIVE LEARNING RESEARCH NETWORK, ILRN 2025

Abstract
Since the publication of the 2020 paper, Finding the Gaps About Uses of Immersive Learning Environments: A Survey of Surveys, the landscape of immersive learning environments (ILEs) has continued to evolve rapidly. This update aims to revisit the gaps identified in that previous research and explore emerging trends. We conducted an extensive review of new surveys published after that paper's cut date. Our findings reveal a significant amount of new published reviews (n = 64), more than doubling the original corpus (n = 47). The results highlighted novel themes of usage of immersive environments, helping bridge some 2020 research gaps. This paper discusses those developments and presents a consolidated perspective on the uses of immersive learning environments.

2026

Reconfiguring Staggered Quantum Walks with ZX

Authors
Jardim, B; Santos, J; Barbosa, LS;

Publication
SOFTWARE ENGINEERING AND FORMAL METHODS. SEFM 2024 COLLOCATED WORKSHOPS

Abstract
The staggered model is a recent, very general variant of discrete-time quantum walks which, avoiding the use of a coin to direct the walker evolution, explores the underlying graph structure to build an evolution operator based on local unitaries induced by adjacent vertices. Optimising their implementation to increase resilience to decoherence phenomena motivates their analysis with the ZX-calculus. The whole optimisation can be seen as a graph reconfiguration process along which the original circuit is rewrote, significantly reducing the number of (expensive) gates used. The exercise identified an underlying pattern leading to an alternative, potentially more efficient evolution operator.

2026

Paraconsistent Reactive Graphs

Authors
Cunha, J; Madeira, A; Barbosa, LS;

Publication
SOFTWARE ENGINEERING AND FORMAL METHODS. SEFM 2024 COLLOCATED WORKSHOPS

Abstract
This paper introduces Paraconsistent Reactive Graphs, as an extension of Reactive graphs that incorporates paraconsistency into the ground edges to address vagueness and inconsistency within dynamic systems. By assigning pairs of truth values to ground edges, this framework captures the uncertainty and contradictions stemming from incomplete or conflicting information. We explore the semantics of these graphs and provide a practical example to illustrate the proposed approach.

2026

Auto-active verification of distributed systems and specification refinements with Why3-do

Authors
Lourenço, CB; Pinto, JS;

Publication
SCIENCE OF COMPUTER PROGRAMMING

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.

2026

A subject-based association network defines new pediatric sleep apnea phenotypes with different odds of recovery after treatment

Authors
Gutiérrez-Tobal, GC; Gomez-Pilar, J; Ferreira-Santos, D; Pereira-Rodrigues, P; Alvarez, D; del Campo, F; Gozal, D; Hornero, R;

Publication
COMPUTER METHODS AND PROGRAMS IN BIOMEDICINE

Abstract
Background and objectives: Timely treatment of pediatric obstructive sleep apnea (OSA) can prevent or reverse neurocognitive and cardiovascular morbidities. However, whether distinct phenotypes exist and account for divergent treatment effectiveness remains unknown. In this study, our goal is threefold: i) to define new data-driven pediatric OSA phenotypes, ii) to evaluate possible treatment effectiveness differences among them, and iii) to assess phenotypic information in predicting OSA resolution. Methods: We involved 22 sociodemographic, anthropometric, and clinical data from 464 children (5-10 years old) from the Childhood Adenotonsillectomy Trial (CHAT) database. Baseline information was used to automatically define pediatric OSA phenotypes using a new unsupervised subject-based association network. Follow-up data (7 months later) were used to evaluate the effects of the therapeutic intervention in terms of changes in the obstructive apnea-hypopnea index (OAHI) and the resolution of OSA (OAHI < 1 event per hour). An explainable artificial intelligence (XAI) approach was also developed to assess phenotypic information as OSA resolution predictor at baseline. Results: Our approach identified three OSA phenotypes (PHOSA1-PHOSA3), with PHOSA2 showing significantly lower odds of OSA recovery than PHOSA1 and PHOSA3 when treatment information was not considered (odds ratios, OR: 1.64 and 1.66, 95 % confidence intervals, CI: 1.03-2.62 and 1.01-2.69, respectively). The odds of OSA recovery were also significantly lower in PHOSA2 than in PHOSA3 when adenotonsillectomy was adopted as treatment (OR: 2.60, 95 % CI: 1.26-5.39). Our XAI approach identified 79.4 % (CI: 69.9-88.0 %) of children reaching OSA resolution after adenotonsillectomy, with a positive predictive value of 77.8 % (CI: 70.3 %-86.0 %). Conclusions: Our new subject-based association network successfully identified three clinically useful pediatric OSA phenotypes with different odds of therapeutic intervention effectiveness. Specifically, we found that children of any sex, >6 years old, overweight or obese, and with enlarged neck and waist circumference (PHOSA2) have less odds of recovering from OSA. Similarly, younger female children with no enlarged neck (PHOSA3) have higher odds of benefiting from adenotonsillectomy.

2026

Video-based epileptic seizure classification: A novel multi-stage approach integrating vision and motion transformer deep learning models

Authors
Aslani, R; Karácsony, T; Fearns, N; Caldeiras, C; Vollmar, C; Rego, R; Rémi, J; Noachtar, S; Cunha, JPS;

Publication
BIOMEDICAL SIGNAL PROCESSING AND CONTROL

Abstract
Automated seizure quantification and classification are needed for semiology-based epileptic seizure diagnosis support. To the best of our knowledge, the 5-class (Hypermotor, Automotor, Complex Motor, Psychogenic Non-Epileptic Seizures, and Generalized Tonic-Clonic Seizures) seizure video dataset (198 seizures from 74 patients) studied in this paper is the largest 5-class dataset ever curated, composed of monocular RGB videos from two university hospital epilepsy monitoring units. 2D skeletons were estimated using ViTPose, a vision transformer deep learning (DL) architecture, and lifted to 3D space using MotionBERT, a multimodal motion transformer architecture. The movements were quantified based on the estimated 3D skeleton sequences. Two approaches were evaluated for seizure classification: (1) classical machine learning methods (Random Forest (RF) and XGBoost) applied to quantified movement parameters, and (2) 2D skeleton-based DL using MotionBERT action, an action recognition DL model, to which we perform transfer-learning. The best model achieved a promising, above literature, 5-fold cross-validated macro average F1-score of 0.84 +/- 0.09 (RF) for 5-class classification. The binary case (Automotor vs Hypermotor) resulted in 0.80 +/- 0.18 (MotionBERT action), and adding a 3rd class (Complex motor) lowered to 0.65 +/- 0.14 (RF). This novel multi-stage classification ensures that the included movement features are traceable, allowing interpretable AI exploration of this novel approach supporting future clinical diagnosis.

  • 18
  • 4383