arXiv subjects

Matteo Rossi

Publications and source records attributed to Matteo Rossi.

At least 19 recordsLinked to original sources

arXiv2026

FormIDEAble: Safe and Socially-aware Autonomous Systems

Autonomous agents operating in socio-critical settings must coordinate with humans under uncertainty while respecting explicit safety constraints. Existing approaches either account for social dynamics without formal guarantees or provide formal assurance while abstracting away human behaviour. We introduce FormIDEAble, a formally grounded approach for synthesising socially-aware cooperation strategies with safety guarantees. The cooperation between humans and the autonomous agent is modelled as a Priced Timed Markov Decision Process, and decision-making is formulated as a cost-bounded reachability problem. We illustrate the approach using an emergency evacuation scenario. Initial experimental evidence demonstrates the effectiveness of the approach and highlights the trade-offs between optimisation and safety guarantees. FormIDEAble provides a principled foundation for formally assured, socially-aware decision-making in socio-critical systems.

cs.SE↗

arXiv2026

Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications

Early-stage specifications of safety-critical systems are typically expressed in natural language, making it difficult to derive formal properties suitable for verification and needed to guarantee safety. While recent Large Language Model (LLM)-based approaches can generate formal artifacts from text, they mainly focus on syntactic correctness and do not ensure semantic alignment between informal requirements and formally verifiable properties. We propose an agentic methodology that automatically extracts verification-ready properties from unstructured specifications. The modular pipeline combines requirement extraction, compatibility filtering with respect to a target formalism, and translation into formal properties. Experimental results across three scenarios show that the pipeline generates syntactically and semantically aligned formal properties with a 77.8% accuracy. By explicitly accounting for modeling and verification constraints, the approach is a paving step towards exploiting Artificial Intelligence (AI) to bridge the gap between informal descriptions and semantically meaningful formal verification.

cs.SE↗

arXiv2026

A Deformable Attention-Based Detection Transformer with Cross-Scale Feature Fusion for Industrial Coil Spring Inspection

Automated visual inspection of locomotive coil springs presents significant challenges due to the morphological diversity of surface defects, substantial scale variations, and complex industrial backgrounds. This paper proposes MSD-DETR (Multi-Scale Deformable Detection Transformer), a novel detection framework that addresses these challenges through three key innovations: (1) a structural re-parameterization strategy that decouples training-time multi-branch topology from inference-time efficiency, enhancing feature extraction while maintaining real-time performance; (2) a deformable attention mechanism that enables content-adaptive spatial sampling, allowing dynamic focus on defect-relevant regions regardless of morphological irregularity; and (3) a cross-scale feature fusion architecture incorporating GSConv modules and VoVGSCSP blocks for effective multi-resolution information aggregation. Comprehensive experiments on a real-world locomotive coil spring dataset demonstrate that MSD-DETR achieves 92.4\% mAP@0.5 at 98 FPS, outperforming state-of-the-art detectors including YOLOv8 (+3.1\% mAP) and the baseline RT-DETR (+2.8\% mAP) while maintaining comparable inference speed, establishing a new benchmark for industrial coil spring quality inspection.

cs.CV↗

arXiv2026

TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version)

The zone abstraction, widely adopted for its notable practical efficiency, is the de facto standard in the verification of Timed Automata (TA). Nonetheless, region-based abstractions have been shown to outperform zones in specific subclasses of TA. To complement and support mature zone-based tools, we introduce TARZAN, a C++ region-based verification library for TA. The algorithms implemented in TARZAN use a novel region abstraction that tracks the order in which clocks become unbounded. This additional ordering induces a finer partitioning of the state space, enabling backward algorithms to avoid the combinatorial explosion associated with enumerating all ordered partitions of unbounded clocks, when computing immediate delay predecessor regions. We validate TARZAN by comparing forward reachability results against the state-of-the-art tools Uppaal and TChecker. The experiments confirm that zones excel when TA have large constants and strict guards. In contrast, TARZAN exhibits superior performance on closed TA and TA with punctual guards. Finally, we demonstrate the efficacy of our backward algorithms, establishing a foundation for region-based analysis in domains like Timed Games, where backward exploration is essential.

cs.FL↗

arXiv2026

TerraBind: Fast and Accurate Binding Affinity Prediction through Coarse Structural Representations

We present TerraBind, a foundation model for protein-ligand structure and binding affinity prediction that achieves 26-fold faster inference than state-of-the-art methods while improving affinity prediction accuracy by $\sim$20\%. Current deep learning approaches to structure-based drug design rely on expensive all-atom diffusion to generate 3D coordinates, creating inference bottlenecks that render large-scale compound screening computationally intractable. We challenge this paradigm with a critical hypothesis: full all-atom resolution is unnecessary for accurate small molecule pose and binding affinity prediction. TerraBind tests this hypothesis through a coarse pocket-level representation (protein C$_\beta$ atoms and ligand heavy atoms only) within a multimodal architecture combining COATI-3 molecular encodings and ESM-2 protein embeddings that learns rich structural representations, which are used in a diffusion-free optimization module for pose generation and a binding affinity likelihood prediction module. On structure prediction benchmarks (FoldBench, PoseBusters, Runs N' Poses), TerraBind matches diffusion-based baselines in ligand pose accuracy. Crucially, TerraBind outperforms Boltz-2 by $\sim$20\% in Pearson correlation for binding affinity prediction on both a public benchmark (CASP16) and a diverse proprietary dataset (18 biochemical/cell assays). We show that the affinity prediction module also provides well-calibrated affinity uncertainty estimates, addressing a critical gap in reliable compound prioritization for drug discovery. Furthermore, this module enables a continual learning framework and a hedged batch selection strategy that, in simulated drug discovery cycles, achieves 6$\times$ greater affinity improvement of selected molecules over greedy-based approaches.

cs.LG↗

arXiv2026

MA-LipNet: Multi-Dimensional Attention Networks for Robust Lipreading

Lipreading, the technology of decoding spoken content from silent videos of lip movements, holds significant application value in fields such as public security. However, due to the subtle nature of articulatory gestures, existing lipreading methods often suffer from limited feature discriminability and poor generalization capabilities. To address these challenges, this paper delves into the purification of visual features from temporal, spatial, and channel dimensions. We propose a novel method named Multi-Attention Lipreading Network(MA-LipNet). The core of MA-LipNet lies in its sequential application of three dedicated attention modules. Firstly, a \textit{Channel Attention (CA)} module is employed to adaptively recalibrate channel-wise features, thereby mitigating interference from less informative channels. Subsequently, two spatio-temporal attention modules with distinct granularities-\textit{Joint Spatial-Temporal Attention (JSTA)} and \textit{Separate Spatial-Temporal Attention (SSTA)}-are leveraged to suppress the influence of irrelevant pixels and video frames. The JSTA module performs a coarse-grained filtering by computing a unified weight map across the spatio-temporal dimensions, while the SSTA module conducts a more fine-grained refinement by separately modeling temporal and spatial attentions. Extensive experiments conducted on the CMLR and GRID datasets demonstrate that MA-LipNet significantly reduces the Character Error Rate (CER) and Word Error Rate (WER), validating its effectiveness and superiority over several state-of-the-art methods. Our work highlights the importance of multi-dimensional feature refinement for robust visual speech recognition.

cs.CV↗

arXiv2025

Pretrained Joint Predictions for Scalable Batch Bayesian Optimization of Molecular Designs

Batched synthesis and testing of molecular designs is the key bottleneck of drug development. There has been great interest in leveraging biomolecular foundation models as surrogates to accelerate this process. In this work, we show how to obtain scalable probabilistic surrogates of binding affinity for use in Batch Bayesian Optimization (Batch BO). This demands parallel acquisition functions that hedge between designs and the ability to rapidly sample from a joint predictive density to approximate them. Through the framework of Epistemic Neural Networks (ENNs), we obtain scalable joint predictive distributions of binding affinity on top of representations taken from large structure-informed models. Key to this work is an investigation into the importance of prior networks in ENNs and how to pretrain them on synthetic data to improve downstream performance in Batch BO. Their utility is demonstrated by rediscovering known potent EGFR inhibitors on a semi-synthetic benchmark in up to 5x fewer iterations, as well as potent inhibitors from a real-world small-molecule library in up to 10x fewer iterations, offering a promising solution for large-scale drug discovery applications.

cs.LG↗

arXiv2025

Finger-to-Chest Style Transfer-assisted Deep Learning Method For Photoplethysmogram Waveform Restoration with Timing Preservation

Wearable measurements, such as those obtained by photoplethysmogram (PPG) sensors are highly susceptible to motion artifacts and noise, affecting cardiovascular measures. Chest-acquired PPG signals are especially vulnerable, with signal degradation primarily resulting from lower perfusion, breathing-induced motion, and mechanical interference from chest movements. Traditional restoration methods often degrade the signal, and supervised deep learning (DL) struggles with random and systematic distortions, requiring very large datasets for successful training. To efficiently restore chest PPG waveform, we propose a style transfer-assisted cycle-consistent generative adversarial network, called starGAN, whose performance is evaluated on a three-channel PPG signal (red, green,and infrared) acquired by a chest-worn multi-modal sensor, called Soundi. Two identical devices are adopted, one sensor to collect the PPG signal on the chest, considered to feature low quality and undergoing restoration, and another sensor to obtain a high-quality PPG signal measured on the finger, considered the reference signal. Extensive validation over some 8,000 5-second chunks collected from 40 subjects showed about 90% correlation of the restored chest PPG with the reference finger PPG, with a 30% improvement over raw chest PPG. Likewise, the signal-to-noise ratio improved on average of about 125%, over the three channels. The agreement with heart-rate computed from concurrent ECG was extremely high, overcoming 84% on average. These results demonstrate effective signal restoration, comparable with findings in recent literature papers. Significance: PPG signals collected from wearable devices are highly susceptible to artifacts, making innovative AI-based techniques fundamental towards holistic health assessments in a single device.

eess.SP↗

arXiv2025

On Decidability Timed Automata with 2 Parametric Clocks

In this paper, we introduce a restriction of Timed Automata (TA), called non-resetting test Timed Automata (nrtTA). An nrtTA does not allow to test and reset the same clock on the same transition. The model has the same expressive power of TA, but it may require one more clock than an TA to recognize the same language. We consider the parametric version of nrtTA, where one parameter can appear in clock guards of transitions. The focus of this draft is to prove that the $\omega$-language emptiness problem for 2-clock parametric nrtTA is decidable. This result can be compared with the parametric version of TA, where the emptiness problem for 2-clock TA with one parameter is not known to be decidable. Our result, however, extends the known decidability of the case of TA with one clock and one parameter from finite words to infinite words.

cs.FL↗

arXiv2025

Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation

A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult to detect, yet a high level of confidence in the outcome is expected. Indeed, these tools are frequently novel and may not have been thoroughly tested. When standard benchmarks may be insufficient or unavailable, random test case generation offers a promising approach. To scale up, random testing requires comparing actual versus expected results, i.e., solving the oracle problem. To address this challenge, this work introduces a novel theoretical framework based on a modular variant of Timed Automata (TA), called Tiled Timed Automata (TTA), for testing model checkers operating with variations of TA, by building oracles based on Weighted Automata. The framework is initially applied to verify model checkers solving the emptiness problem for Parametric TA and it is validated, in this specific scenario, by our tool, TABEC, which randomly generates tests predicting their expected outcome through automated oracle generation. Furthermore, the general nature of TTA facilitates the framework adaptation to model checkers solving other decidable problems on TA, as detailed for the minimum-cost reachability problem of Priced TA.

cs.FL↗

arXiv2025

The influence of phonon symmetry and electronic structure on the electron-phonon coupling momentum dependence in cuprates

The experimental determination of the magnitude and momentum dependence of electron-phonon coupling (EPC) is an outstanding problem in condensed matter physics. The intensity of phonon peaks in Resonant Inelastic X-ray Scattering (RIXS) spectra can be related to the underlying EPC strength under significant approximations whose validity deserves careful verification. We measured the Cu L$_3$ RIXS phonon intensity as function of incident photon energy and of momentum transfer in several layered cuprates. For CaCuO$_2$, La$_{2-x}$Sr$_{x}$CuO$_{4+\delta}$, and \ch{YBa_2Cu_3O_{6}}, using a generally accepted theoretical model, we estimate quantitatively the EPC for the bond-stretching mode along the high-symmetry directions ($\zeta$,0) and ($\zeta$,$\zeta$), and as a function of the azimuthal angle $\varphi$ at fixed $q_\parallel$. We compare our results with theoretical predictions and we find that the $\mathbf{q}_\parallel$-dependence of the phonon RIXS intensity can be largely ascribed to the phonon symmetry. However, a more satisfactory prediction of the experimental results requires an accurate description of the electronic structure close to the Fermi level. Our extensive investigation indicates that Cu L$_3$ RIXS can be reliably used to determine the momentum dependence of EPC for the bond-stretching modes of cuprates. Moreover, the large experimental basis provided in this article can serve as stringent test for advanced theoretical predictions on the EPC.

cond-mat.str-el↗

arXiv2024

Cascade learning in multi-task encoder-decoder networks for concurrent bone segmentation and glenohumeral joint assessment in shoulder CT scans

Osteoarthritis is a degenerative condition affecting bones and cartilage, often leading to osteophyte formation, bone density loss, and joint space narrowing. Treatment options to restore normal joint function vary depending on the severity of the condition. This work introduces an innovative deep-learning framework processing shoulder CT scans. It features the semantic segmentation of the proximal humerus and scapula, the 3D reconstruction of bone surfaces, the identification of the glenohumeral (GH) joint region, and the staging of three common osteoarthritic-related pathologies: osteophyte formation (OS), GH space reduction (JS), and humeroscapular alignment (HSA). The pipeline comprises two cascaded CNN architectures: 3D CEL-UNet for segmentation and 3D Arthro-Net for threefold classification. A retrospective dataset of 571 CT scans featuring patients with various degrees of GH osteoarthritic-related pathologies was used to train, validate, and test the pipeline. Root mean squared error and Hausdorff distance median values for 3D reconstruction were 0.22mm and 1.48mm for the humerus and 0.24mm and 1.48mm for the scapula, outperforming state-of-the-art architectures and making it potentially suitable for a PSI-based shoulder arthroplasty preoperative plan context. The classification accuracy for OS, JS, and HSA consistently reached around 90% across all three categories. The computational time for the inference pipeline was less than 15s, showcasing the framework's efficiency and compatibility with orthopedic radiology practice. The outcomes represent a promising advancement toward the medical translation of artificial intelligence tools. This progress aims to streamline the preoperative planning pipeline delivering high-quality bone surfaces and supporting surgeons in selecting the most suitable surgical approach according to the unique patient joint conditions.

eess.IV↗

arXiv2024

Orbital inversion and emergent lattice dynamics in infinite layer CaCoO$_2$

The layered cobaltate CaCoO$_2$ exhibits a unique herringbone-like structure. Serving as a potential prototype for a new class of complex lattice patterns, we study the properties of CaCoO$_2$ using X-ray absorption spectroscopy (XAS) and resonant inelastic X-ray scattering (RIXS). Our results reveal a significant inter-plane hybridization between the Ca $4s-$ and Co $3d-$orbitals, leading to an inversion of the textbook orbital occupation of a square planar geometry. Further, our RIXS data reveal a strong low energy mode, with anomalous intensity modulations as a function of momentum transfer close to a quasi-static response suggestive of electronic and/or orbital ordering. These findings indicate that the newly discovered herringbone structure exhibited in CaCoO$_2$ may serve as a promising laboratory for the design of materials having strong electronic, orbital and lattice correlations.

cond-mat.str-el↗

arXiv2023

Quantum-centric Supercomputing for Materials Science: A Perspective on Challenges and Future Directions

Computational models are an essential tool for the design, characterization, and discovery of novel materials. Hard computational tasks in materials science stretch the limits of existing high-performance supercomputing centers, consuming much of their simulation, analysis, and data resources. Quantum computing, on the other hand, is an emerging technology with the potential to accelerate many of the computational tasks needed for materials science. In order to do that, the quantum technology must interact with conventional high-performance computing in several ways: approximate results validation, identification of hard problems, and synergies in quantum-centric supercomputing. In this paper, we provide a perspective on how quantum-centric supercomputing can help address critical computational problems in materials science, the challenges to face in order to solve representative use cases, and new suggested directions.

quant-ph↗

arXiv2023

Low temperature dynamic polaron liquid in a manganite exhibiting colossal magnetoresistance

Polarons - fermionic charge carriers bearing a strong companion lattice deformation - exhibit a natural tendency for self-localization due to the recursive interaction between electrons and the lattice. While polarons are ubiquitous in insulators, how they evolve in transitions to metallic and superconducting states in quantum materials remains an open question. Here, we use resonant inelastic x-ray scattering (RIXS) to track the electron-lattice coupling in the colossal magneto-resistive bi-layer manganite La$_{1.2}$Sr$_{1.8}$Mn$_2$O$_7$ across its metal-to-insulator transition. The response in the insulating high-temperature state features harmonic emissions of a dispersionless oxygen phonon at small energy transfer. Upon cooling into the metallic state, we observe a drastic redistribution of spectral weight from the region of these harmonic emissions to a broad high energy continuum. In concert with theoretical calculations, we show that this evolution implies a shift in electron-lattice coupling from static to dynamic lattice distortions that leads to a distinct polaronic ground state in the low temperature metallic phase - a dynamic polaron liquid.

cond-mat.str-el↗

arXiv2023

Lecture Notes on Monadic First- and Second-Order Logic on Strings

These notes present the essentials of first- and second-order monadic logics on strings with introductory purposes. We discuss Monadic First-Order logic and show that it is strictly less expressive than Finite-State Automata, in that it only captures a strict subset of Regular Languages -- the non-counting ones. We then introduce Monadic Second-Order logic; such a logic is, syntactically, a superset of Monadic First-Order logic and captures Regular Languages exactly. We also show how to transform an automaton into a corresponding formula and vice versa. Finally, we discuss the use of logical characterizations of classes of languages as the basis for automatic verification techniques.

cs.LO↗

arXiv2022

SPRINT: Semantics for PerfoRmant and scalable INteroperability of multimodal Transport

Interoperability is a long-standing challenge slowing down the digitalization of mobility systems and the provision of full mobility-as-a-service offerings. This paper presents early results achieved by the SPRINT project (Semantics for PerfoRmant and scalable INteroperability of multimodal Transport), an integral part of the Shift2Rail IP4 work programme, in meeting the challenge. It introduces the conceptual architecture and describes the demonstrator implementation of the Interoperability Framework (IF), a solution designed to support servitization in the mobility domain in two directions: From the Travel Application perspective, the IF provides semantically-consistent abstractions of distributed ICT resources offered by Service Provider Companies, insulating them from the "mechanics" of operating remotely over networks and across multiple communication protocols and/or data formats; from the Service Provider Companies perspective, the IF allows leveraging their native ICT computing environment and resources as elements of an end-to-end integrated intermodal mobility solution, insulating them from the specifics of the customer front-end applications.

cs.SE↗

arXiv2021

A Broken Translational Symmetry State in an Infinite-Layer Nickelate

A defining signature of strongly correlated electronic systems is the existence of competing phases with similar ground state energies, resulting in a rich phase diagram. While in the recently discovered nickelate superconductors, a high antiferromagnetic exchange energy has been reported, which implies the existence of strong electronic correlations, signatures of competing phases have not yet been observed. Here, we uncover a charge order (CO) in infinite-layer nickelates La1-xSrxNiO2 using resonant x-ray scattering across the Ni L-edge. In the parent compound, the CO arranges along the Ni-O bond direction with an incommensurate wave vector (0.344+/-0.002, 0) r.l.u., distinct from the stripe order in other nickelates which propagates along a direction 45 degree to the Ni-O bond. The CO resonance profile indicates that CO originates from the Ni 3d states and induces a parasitic charge modulation of La electrons. Upon doping, the CO diminishes and the ordering wave vector shifts toward a commensurate value of 1/3 r.l.u., indicating that the CO likely arises from strong correlation effects and not from Fermi surface nesting.

cond-mat.supr-con↗