Showing 1–50 of 115 results for author: Sánchez, C

Preserving Russek's "Summermood" Using Reality Check and a DeltaLab DL-4 Approximation

Authors: Jeremy Hyrkas, Pablo Dodero Carrillo, Teresa Díaz de Cossio Sánchez

Abstract: As a contribution towards ongoing efforts to maintain electroacoustic compositions for live performance, we present a collection of Pure Data patches to preserve and perform Antonio Russek's piece "Summermood" for bass flute and live electronics. The piece, originally written for the DeltaLab DL-4 delay rack unit, contains score markings specific to the DL-4. Here, we approximate the sound and uni… ▽ More As a contribution towards ongoing efforts to maintain electroacoustic compositions for live performance, we present a collection of Pure Data patches to preserve and perform Antonio Russek's piece "Summermood" for bass flute and live electronics. The piece, originally written for the DeltaLab DL-4 delay rack unit, contains score markings specific to the DL-4. Here, we approximate the sound and unique functionality of the DL-4 in Pure Data, then refine our implementation to better match the unit on which the piece was performed by comparing settings from the score to two official recordings of the piece. The DL-4 emulation is integrated into a patch for live performance based on the Null Piece, and regression tested using the Reality Check framework for Pure Data. Using this library of patches, Summermood can be brought back into live rotation without the use of the now discontinued DL-4. The patches will be continuously tested to ensure that the piece is playable across computer environments and as the Pure Data programming language is updated. △ Less

Submitted 25 September, 2025; originally announced September 2025.

Comments: 6 pages, 10 figures, Pure Data Max Conference 2025

Journal ref: Proceedings and Programs of PdMaxCon25~ (2025) 55-60

Setchain Algorithms for Blockchain Scalability

Authors: Arivarasan Karmegam, Gabina Luz Bianchi, Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, César Sánchez

Abstract: Setchain has been proposed to increase blockchain scalability by relaxing the strict total order requirement among transactions. Setchain organizes elements into a sequence of sets, referred to as epochs, so that elements within each epoch are unordered. In this paper, we propose and evaluate three distinct Setchain algorithms, that leverage an underlying block-based ledger. Vanilla is a basic imp… ▽ More Setchain has been proposed to increase blockchain scalability by relaxing the strict total order requirement among transactions. Setchain organizes elements into a sequence of sets, referred to as epochs, so that elements within each epoch are unordered. In this paper, we propose and evaluate three distinct Setchain algorithms, that leverage an underlying block-based ledger. Vanilla is a basic implementation that serves as a reference point. Compresschain aggregates elements into batches, and compresses these batches before appending them as epochs in the ledger. Hashchain converts batches into fixed-length hashes which are appended as epochs in the ledger. This requires Hashchain to use a distributed service to obtain the batch contents from its hash. To allow light clients to safely interact with only one server, the proposed algorithms maintain, as part of the Setchain, proofs for the epochs. An epoch-proof is the hash of the epoch, cryptographically signed by a server. A client can verify the correctness of an epoch with $f+1$ epoch-proofs (where $f$ is the maximum number of Byzantine servers assumed). All three Setchain algorithms are implemented on top of the CometBFT blockchain application platform. We conducted performance evaluations across various configurations, using clusters of four, seven, and ten servers. Our results show that the Setchain algorithms reach orders of magnitude higher throughput than the underlying blockchain, and achieve finality with latency below 4 seconds. △ Less

Submitted 11 September, 2025; originally announced September 2025.

A Secure Sequencer and Data Availability Committee for Rollups (Extended Version)

Authors: Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sanchez, César Sánchez

Abstract: Blockchains face a scalability limitation, partly due to the throughput limitations of consensus protocols, especially when aiming to obtain a high degree of decentralization. Layer 2 Rollups (L2s) are a faster alternative to conventional blockchains. L2s perform most computations offchain using minimally blockchains (L1) under-the-hood to guarantee correctness. A sequencer is a service that recei… ▽ More Blockchains face a scalability limitation, partly due to the throughput limitations of consensus protocols, especially when aiming to obtain a high degree of decentralization. Layer 2 Rollups (L2s) are a faster alternative to conventional blockchains. L2s perform most computations offchain using minimally blockchains (L1) under-the-hood to guarantee correctness. A sequencer is a service that receives offchain L2 transaction requests, batches these transactions, and commits compressed or hashed batches to L1. Using hashing needs less L1 space, which is beneficial for gas cost, but requires a data availability committee (DAC) service to translate hashes into their corresponding batches of transaction requests. The behavior of sequencers and DACs influence the evolution of the L2 blockchain, presenting a potential security threat and delaying L2 adoption. We propose in this paper fraud-proof mechanisms, arbitrated by L1 contracts, to detect and generate evidence of dishonest behavior of the sequencer and DAC. We study how these fraud-proofs limit the power of adversaries that control different number of sequencer and DACs members, and provide incentives for their honest behavior. We designed these fraud-proof mechanisms as two player games. Unlike the generic fraud-proofs in current L2s (designed to guarantee the correct execution of transactions), our fraud-proofs are over pred-etermined algorithms that verify the properties that determine the correctness of the DAC. Arbitrating over concrete algorithms makes our fraud-proofs more efficient, easier to understand, and simpler to prove correct. We provide as an artifact a mechanization in LEAN4 of our fraud-proof games, including (1) the verified strategies that honest players should play to win all games as well as (2) mechanisms to detect dishonest claims. △ Less

Submitted 9 September, 2025; v1 submitted 8 September, 2025; originally announced September 2025.

Understanding Demand for Shared Autonomous Micro-Mobility

Authors: Naroa Coretti Sanchez, Kent Larson

Abstract: This study examines the behavioral and environmental implications of shared autonomous micro-mobility systems, focusing on autonomous bicycles and their integration with transit in the U.S. While prior research has addressed operational and lifecycle aspects, a critical gap remains in understanding which modes these services are likely to substitute, who is most inclined to adopt them, and how ser… ▽ More This study examines the behavioral and environmental implications of shared autonomous micro-mobility systems, focusing on autonomous bicycles and their integration with transit in the U.S. While prior research has addressed operational and lifecycle aspects, a critical gap remains in understanding which modes these services are likely to substitute, who is most inclined to adopt them, and how service attributes influence user decisions. We design a context-aware stated preference survey grounded in real-world trips and estimate discrete choice models, including a hybrid model incorporating latent attitudes. Findings indicate that adoption, mode shift, and environmental impacts are highly sensitive to service design. Scenarios with minimal wait and cost yield high adoption but increase emissions, while moderate waits are more likely to reduce impacts. Adoption likelihood varies with demographic characteristics, and outcomes depend on city type, context, and infrastructure assumptions. These insights can inform the development of more sustainable and equitable mobility systems. △ Less

Submitted 5 August, 2025; originally announced August 2025.

Explanations for Unrealizability of Infinite-State Safety Shields

Authors: Andoni Rodriguez, Irfansha Shaik, Davide Corsi, Roy Fox, Cesar Sanchez

Abstract: Safe Reinforcement Learning focuses on developing optimal policies while ensuring safety. A popular method to address such task is shielding, in which a correct-by-construction safety component is synthesized from logical specifications. Recently, shield synthesis has been extended to infinite-state domains, such as continuous environments. This makes shielding more applicable to realistic scenari… ▽ More Safe Reinforcement Learning focuses on developing optimal policies while ensuring safety. A popular method to address such task is shielding, in which a correct-by-construction safety component is synthesized from logical specifications. Recently, shield synthesis has been extended to infinite-state domains, such as continuous environments. This makes shielding more applicable to realistic scenarios. However, often shields might be unrealizable because the specification is inconsistent (e.g., contradictory). In order to address this gap, we present a method to obtain simple unconditional and conditional explanations that witness unrealizability, which goes by temporal formula unrolling. In this paper, we show different variants of the technique and its applicability. △ Less

Submitted 31 July, 2025; originally announced July 2025.

Foundation Models in Medical Imaging -- A Review and Outlook

Authors: Vivien van Veldhuizen, Vanessa Botha, Chunyao Lu, Melis Erdal Cesur, Kevin Groot Lipman, Edwin D. de Jong, Hugo Horlings, Clárisa I. Sanchez, Cees G. M. Snoek, Lodewyk Wessels, Ritse Mann, Eric Marcus, Jonas Teuwen

Abstract: Foundation models (FMs) are changing the way medical images are analyzed by learning from large collections of unlabeled data. Instead of relying on manually annotated examples, FMs are pre-trained to learn general-purpose visual features that can later be adapted to specific clinical tasks with little additional supervision. In this review, we examine how FMs are being developed and applied in pa… ▽ More Foundation models (FMs) are changing the way medical images are analyzed by learning from large collections of unlabeled data. Instead of relying on manually annotated examples, FMs are pre-trained to learn general-purpose visual features that can later be adapted to specific clinical tasks with little additional supervision. In this review, we examine how FMs are being developed and applied in pathology, radiology, and ophthalmology, drawing on evidence from over 150 studies. We explain the core components of FM pipelines, including model architectures, self-supervised learning methods, and strategies for downstream adaptation. We also review how FMs are being used in each imaging domain and compare design choices across applications. Finally, we discuss key challenges and open questions to guide future research. △ Less

Submitted 16 June, 2025; v1 submitted 10 June, 2025; originally announced June 2025.

XAI-Units: Benchmarking Explainability Methods with Unit Tests

Authors: Jun Rui Lee, Sadegh Emami, Michael David Hollins, Timothy C. H. Wong, Carlos Ignacio Villalobos Sánchez, Francesca Toni, Dekai Zhang, Adam Dejl

Abstract: Feature attribution (FA) methods are widely used in explainable AI (XAI) to help users understand how the inputs of a machine learning model contribute to its outputs. However, different FA models often provide disagreeing importance scores for the same model. In the absence of ground truth or in-depth knowledge about the inner workings of the model, it is often difficult to meaningfully determine… ▽ More Feature attribution (FA) methods are widely used in explainable AI (XAI) to help users understand how the inputs of a machine learning model contribute to its outputs. However, different FA models often provide disagreeing importance scores for the same model. In the absence of ground truth or in-depth knowledge about the inner workings of the model, it is often difficult to meaningfully determine which of the different FA methods produce more suitable explanations in different contexts. As a step towards addressing this issue, we introduce the open-source XAI-Units benchmark, specifically designed to evaluate FA methods against diverse types of model behaviours, such as feature interactions, cancellations, and discontinuous outputs. Our benchmark provides a set of paired datasets and models with known internal mechanisms, establishing clear expectations for desirable attribution scores. Accompanied by a suite of built-in evaluation metrics, XAI-Units streamlines systematic experimentation and reveals how FA methods perform against distinct, atomic kinds of model reasoning, similar to unit tests in software engineering. Crucially, by using procedurally generated models tied to synthetic datasets, we pave the way towards an objective and reliable comparison of FA methods. △ Less

Submitted 1 June, 2025; originally announced June 2025.

Comments: Accepted at FAccT 2025

Efficient Dynamic Shielding for Parametric Safety Specifications

Authors: Davide Corsi, Kaushik Mallik, Andoni Rodriguez, Cesar Sanchez

Abstract: Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller's actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety… ▽ More Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller's actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety requirement changes at runtime due to changing operating conditions, the shield needs to be recomputed from scratch, causing delays that could be fatal. We introduce dynamic shields for parametric safety specifications, which are succinctly represented sets of all possible safety specifications that may be encountered at runtime. Our dynamic shields are statically designed for a given safety parameter set, and are able to dynamically adapt as the true safety specification (permissible by the parameters) is revealed at runtime. The main algorithmic novelty lies in the dynamic adaptation procedure, which is a simple and fast algorithm that utilizes known features of standard safety shields, like maximal permissiveness. We report experimental results for a robot navigation problem in unknown territories, where the safety specification evolves as new obstacles are discovered at runtime. In our experiments, the dynamic shields took a few minutes for their offline design, and took between a fraction of a second and a few seconds for online adaptation at each step, whereas the brute-force online recomputation approach was up to 5 times slower. △ Less

Submitted 28 May, 2025; originally announced May 2025.

QMIO: A tightly integrated hybrid HPCQC system

Authors: Javier Cacheiro, Álvaro C Sánchez, Russell Rundle, George B Long, Gavin Dold, Jamie Friel, Andrés Gómez

Abstract: High-Performance Computing (HPC) systems are the most powerful tools that we currently have to solve complex scientific simulations. Quantum computing (QC) has the potential to enhance HPC systems by accelerating the execution of specific kernels that can be offloaded to a Quantum Processing Unit (QPU), granting them new capabilities, improving the speed of computation, or reducing energy consumpt… ▽ More High-Performance Computing (HPC) systems are the most powerful tools that we currently have to solve complex scientific simulations. Quantum computing (QC) has the potential to enhance HPC systems by accelerating the execution of specific kernels that can be offloaded to a Quantum Processing Unit (QPU), granting them new capabilities, improving the speed of computation, or reducing energy consumption. In this paper, we present QMIO: a state-of-the-art hybrid HPCQC system, which tightly integrates HPC and QC. We describe its hardware and software components, the integration middleware, and the lessons learned during the design, implementation, and operation of the system. △ Less

Submitted 25 May, 2025; originally announced May 2025.

Comments: 25 pages, 8 figures

What Needs Attention? Prioritizing Drivers of Developers' Trust and Adoption of Generative AI

Authors: Rudrajit Choudhuri, Bianca Trinkenreich, Rahul Pandita, Eirini Kalliamvakou, Igor Steinmacher, Marco Gerosa, Christopher Sanchez, Anita Sarma

Abstract: Generative AI (genAI) tools are advertised as productivity aids. Yet, issues related to miscalibrated trust and usage friction continue to hinder their adoption. Additionally, AI can be exclusionary, failing to support diverse users adequately, further exacerbating these concerns. One such aspect of diversity is cognitive diversity -- variations in users' cognitive styles -- that leads to divergen… ▽ More Generative AI (genAI) tools are advertised as productivity aids. Yet, issues related to miscalibrated trust and usage friction continue to hinder their adoption. Additionally, AI can be exclusionary, failing to support diverse users adequately, further exacerbating these concerns. One such aspect of diversity is cognitive diversity -- variations in users' cognitive styles -- that leads to divergence in interaction styles. When an individual's cognitive styles are unsupported, it creates additional barriers to technology adoption. Thus, to design tools that developers trust, we must first understand what factors affect their trust and intentions to use these tools in practice? We developed a theoretical model of factors influencing trust and adoption intentions towards genAI through a large-scale survey with developers (N=238) at GitHub and Microsoft. Using Partial Least Squares-Structural Equation Modeling (PLS-SEM), we found that genAI's system/output quality, functional value, and goal maintenance significantly influence developers' trust, which along with their cognitive styles, affects their intentions to use these tools in work. An Importance-Performance Matrix Analysis (IPMA) identified factors that, despite their strong influence, underperform, revealing specific genAI aspects that need design prioritization. We bolster these findings by qualitatively analyzing developers' perceived challenges and risks of genAI usage to uncover why these gaps persist in development contexts. For genAI to indeed be a true productivity aid rather than a disguised productivity sink, it must align with developers' goals, maintain contextual transparency, reduce cognitive burden, and provide equitable interaction support. We provide practical suggestions to guide future genAI tool design for effective, trustworthy, and inclusive human-genAI interactions. △ Less

Submitted 28 May, 2025; v1 submitted 22 May, 2025; originally announced May 2025.

Comments: Journal extension of ICSE 2025 paper (arXiv:2409.04099)

A Decentralized Sequencer and Data Availability Committee for Rollups Using Set Consensus

Authors: Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sánchez, César Sánchez

Abstract: Blockchains face a scalability challenge due to the intrinsic throughput limitations of consensus protocols and the limitation in block sizes due to decentralization. An alternative to improve the number of transactions per second is to use Layer 2 (L2) rollups. L2s perform most computations offchain using blockchains (L1) minimally under-the-hood to guarantee correctness. A sequencer receives off… ▽ More Blockchains face a scalability challenge due to the intrinsic throughput limitations of consensus protocols and the limitation in block sizes due to decentralization. An alternative to improve the number of transactions per second is to use Layer 2 (L2) rollups. L2s perform most computations offchain using blockchains (L1) minimally under-the-hood to guarantee correctness. A sequencer receives offchain L2 transaction requests, batches them, and commits compressed or hashed batches to L1. Hashing offers much better compression but requires a data availability committee (DAC) to translate hashes back into their corresponding batches. Current L2s consist of a centralized sequencer which receives and serializes all transactions and an optional DAC. Centralized sequencers can undesirably influence L2s evolution. We propose in this paper a fully decentralized implementation of a service that combines (1) a sequencer that posts hashes to the L1 blockchain and (2) the data availability committee that reverses the hashes. We call the resulting service a (decentralized) arranger. Our decentralized arranger is based on Set Byzantine Consensus (SBC), a service where participants can propose sets of values and consensus is reached on a subset of the union of the values proposed. We extend SBC for our fully decentralized arranger. Our main contributions are (1) a formal definition of arrangers; (2) two implementations, one with a centralized sequencer and another with a fully decentralized algorithm, with their proof of correctness; and (3) empirical evidence that our solution scales by implementing all building blocks necessary to implement a correct server. △ Less

Submitted 7 March, 2025; originally announced March 2025.

Comments: arXiv admin note: substantial text overlap with arXiv:2406.02316

Attenuation artifact detection and severity classification in intracoronary OCT using mixed image representations

Authors: Pierandrea Cancian, Simone Saitta, Xiaojin Gu, Rudolf L. M. van Herten, Thijs J. Luttikholt, Jos Thannhauser, Rick H. J. A. Volleberg, Ruben G. A. van der Waerden, Joske L. van der Zande, Clarisa I. Sánchez, Bram van Ginneken, Niels van Royen, Ivana Išgum

Abstract: In intracoronary optical coherence tomography (OCT), blood residues and gas bubbles cause attenuation artifacts that can obscure critical vessel structures. The presence and severity of these artifacts may warrant re-acquisition, prolonging procedure time and increasing use of contrast agent. Accurate detection of these artifacts can guide targeted re-acquisition, reducing the amount of repeated s… ▽ More In intracoronary optical coherence tomography (OCT), blood residues and gas bubbles cause attenuation artifacts that can obscure critical vessel structures. The presence and severity of these artifacts may warrant re-acquisition, prolonging procedure time and increasing use of contrast agent. Accurate detection of these artifacts can guide targeted re-acquisition, reducing the amount of repeated scans needed to achieve diagnostically viable images. However, the highly heterogeneous appearance of these artifacts poses a challenge for the automated detection of the affected image regions. To enable automatic detection of the attenuation artifacts caused by blood residues and gas bubbles based on their severity, we propose a convolutional neural network that performs classification of the attenuation lines (A-lines) into three classes: no artifact, mild artifact and severe artifact. Our model extracts and merges features from OCT images in both Cartesian and polar coordinates, where each column of the image represents an A-line. Our method detects the presence of attenuation artifacts in OCT frames reaching F-scores of 0.77 and 0.94 for mild and severe artifacts, respectively. The inference time over a full OCT scan is approximately 6 seconds. Our experiments show that analysis of images represented in both Cartesian and polar coordinate systems outperforms the analysis in polar coordinates only, suggesting that these representations contain complementary features. This work lays the foundation for automated artifact assessment and image acquisition guidance in intracoronary OCT imaging. △ Less

Submitted 7 March, 2025; originally announced March 2025.

Let's Talk Futures: A Literature Review of HCI's Future-Orientation

Authors: Camilo Sanchez, Sui Wang, Kaisa Savolainen, Felix Anand Epp, Antti Salovaara

Abstract: HCI is future-oriented by nature: it explores new human--technology interactions and applies the findings to promote and shape vital visions of society. Still, the visions of futures in HCI publications seem largely implicit, techno-deterministic, narrow, and lacking in roadmaps and attention to uncertainties. A literature review centered on this problem examined futuring and its forms in the ACM… ▽ More HCI is future-oriented by nature: it explores new human--technology interactions and applies the findings to promote and shape vital visions of society. Still, the visions of futures in HCI publications seem largely implicit, techno-deterministic, narrow, and lacking in roadmaps and attention to uncertainties. A literature review centered on this problem examined futuring and its forms in the ACM Digital Library's most frequently cited HCI publications. This analysis entailed developing the four-category framework SPIN, informed by futures studies literature. The results confirm that, while technology indeed drives futuring in HCI, a growing body of HCI research is coming to challenge techno-centric visions. Emerging foci of HCI futuring demonstrate active exploration of uncertainty, a focus on human experience, and contestation of dominant narratives. The paper concludes with insight illuminating factors behind techno-centrism's continued dominance of HCI discourse, as grounding for five opportunities for the field to expand its contribution to futures and anticipation research. △ Less

Submitted 13 February, 2025; originally announced February 2025.

Comments: CHI Conference on Human Factors in Computing Systems (CHI '25), April 26-May 1, 2025, Yokohama, Japan

ACM Class: H.5.0

Virtual airways heatmaps to optimize point of entry location in lung biopsy planning systems

Authors: Debora Gil, Pere Lloret, Marta Diez-Ferrer, Carles Sanchez

Abstract: Purpose: We present a virtual model to optimize point of entry (POE) in lung biopsy planning systems. Our model allows to compute the quality of a biopsy sample taken from potential POE, taking into account the margin of error that arises from discrepancies between the orientation in the planning simulation and the actual orientation during the operation. Additionally, the study examines the impac… ▽ More Purpose: We present a virtual model to optimize point of entry (POE) in lung biopsy planning systems. Our model allows to compute the quality of a biopsy sample taken from potential POE, taking into account the margin of error that arises from discrepancies between the orientation in the planning simulation and the actual orientation during the operation. Additionally, the study examines the impact of the characteristics of the lesion. Methods: The quality of the biopsy is given by a heatmap projected onto the skeleton of a patient-specific model of airways. The skeleton provides a 3D representation of airways structure, while the heatmap intensity represents the potential amount of tissue that it could be extracted from each POE. This amount of tissue is determined by the intersection of the lesion with a cone that represents the uncertainty area in the introduction of biopsy instruments. The cone, lesion, and skeleton are modelled as graphical objects that define a 3D scene of the intervention. Results: We have simulated different settings of the intervention scene from a single anatomy extracted from a CT scan and two lesions with regular and irregular shapes. The different scenarios are simulated by systematic rotation of each lesion placed at different distances from airways. Analysis of the heatmaps for the different settings show a strong impact of lesion orientation for irregular shape and the distance for both shapes. Conclusion: The proposed heatmaps help to visually assess the optimal POE and identify whether multiple optimal POEs exist in different zones of the bronchi. They also allow us to model the maximum allowable error in navigation systems and study which variables have the greatest influence on the success of the operation. Additionally, they help determine at what point this influence could potentially jeopardize the operation. △ Less

Submitted 31 January, 2025; originally announced January 2025.

Journal ref: International Journal of Computer Assisted Radiology and Surgery (2024): 1-6

Towards HRTF Personalization using Denoising Diffusion Models

Authors: Juan Camilo Albarracín Sánchez, Luca Comanducci, Mirco Pezzoli, Fabio Antonacci

Abstract: Head-Related Transfer Functions (HRTFs) have fundamental applications for realistic rendering in immersive audio scenarios. However, they are strongly subject-dependent as they vary considerably depending on the shape of the ears, head and torso. Thus, personalization procedures are required for accurate binaural rendering. Recently, Denoising Diffusion Probabilistic Models (DDPMs), a class of gen… ▽ More Head-Related Transfer Functions (HRTFs) have fundamental applications for realistic rendering in immersive audio scenarios. However, they are strongly subject-dependent as they vary considerably depending on the shape of the ears, head and torso. Thus, personalization procedures are required for accurate binaural rendering. Recently, Denoising Diffusion Probabilistic Models (DDPMs), a class of generative learning techniques, have been applied to solve a variety of signal processing-related problems. In this paper, we propose a first approach for using DDPM conditioned on anthropometric measurements to generate personalized Head-Related Impulse Response (HRIR), the time-domain representation of HRTF. The results show the feasibility of DDPMs for HRTF personalization obtaining performance in line with state-of-the-art models. △ Less

Submitted 6 January, 2025; originally announced January 2025.

Comments: to appear in ICASSP 2025

Uncertainty-aware retinal layer segmentation in OCT through probabilistic signed distance functions

Authors: Mohammad Mohaiminul Islam, Coen de Vente, Bart Liefers, Caroline Klaver, Erik J Bekkers, Clara I. Sánchez

Abstract: In this paper, we present a new approach for uncertainty-aware retinal layer segmentation in Optical Coherence Tomography (OCT) scans using probabilistic signed distance functions (SDF). Traditional pixel-wise and regression-based methods primarily encounter difficulties in precise segmentation and lack of geometrical grounding respectively. To address these shortcomings, our methodology refines t… ▽ More In this paper, we present a new approach for uncertainty-aware retinal layer segmentation in Optical Coherence Tomography (OCT) scans using probabilistic signed distance functions (SDF). Traditional pixel-wise and regression-based methods primarily encounter difficulties in precise segmentation and lack of geometrical grounding respectively. To address these shortcomings, our methodology refines the segmentation by predicting a signed distance function (SDF) that effectively parameterizes the retinal layer shape via level set. We further enhance the framework by integrating probabilistic modeling, applying Gaussian distributions to encapsulate the uncertainty in the shape parameterization. This ensures a robust representation of the retinal layer morphology even in the presence of ambiguous input, imaging noise, and unreliable segmentations. Both quantitative and qualitative evaluations demonstrate superior performance when compared to other methods. Additionally, we conducted experiments on artificially distorted datasets with various noise types-shadowing, blinking, speckle, and motion-common in OCT scans to showcase the effectiveness of our uncertainty estimation. Our findings demonstrate the possibility to obtain reliable segmentation of retinal layers, as well as an initial step towards the characterization of layer integrity, a key biomarker for disease progression. Our code is available at \url{https://github.com/niazoys/RLS_PSDF}. △ Less

Submitted 6 December, 2024; originally announced December 2024.

OSU-Wing PIC Phase I Evaluation: Baseline Workload and Situation Awareness Results

Authors: Julie A. Adams, Christopher A. Sanchez, Vivek Mallampati, Joshua Bhagat Smith, Emily Burgess, Andrew Dassonville

Abstract: The common theory is that human pilot's performance degrades when responsible for an increased number of uncrewed aircraft systems (UAS). This theory was developed in the early 2010's for ground robots and not highly autonomous UAS. It has been shown that increasing autonomy can mitigate some performance impacts associated with increasing the number of UAS. Overall, the Oregon State University-Win… ▽ More The common theory is that human pilot's performance degrades when responsible for an increased number of uncrewed aircraft systems (UAS). This theory was developed in the early 2010's for ground robots and not highly autonomous UAS. It has been shown that increasing autonomy can mitigate some performance impacts associated with increasing the number of UAS. Overall, the Oregon State University-Wing collaboration seeks to understand what factors negatively impact a pilot's ability to maintain responsibility and control over an assigned set of active UAS. The Phase I evaluation establishes baseline data focused on the number of UAS and the number of nests increase. This evaluation focuses on nominal operations as well as crewed aircraft encounters and adverse weather changes. The results demonstrate that the pilots were actively engaged and had very good situation awareness. Manipulation of the conditions did not result in any significant differences in overall workload. The overall results debunk the theory that increasing the number of UAS is detrimental to pilot's performance. △ Less

Submitted 27 November, 2024; originally announced November 2024.

Comments: 45 pages, 10 figures, 21 tables

Zero-shot capability of SAM-family models for bone segmentation in CT scans

Authors: Caroline Magg, Hoel Kervadec, Clara I. Sánchez

Abstract: The Segment Anything Model (SAM) and similar models build a family of promptable foundation models (FMs) for image and video segmentation. The object of interest is identified using prompts, such as bounding boxes or points. With these FMs becoming part of medical image segmentation, extensive evaluation studies are required to assess their strengths and weaknesses in clinical setting. Since the p… ▽ More The Segment Anything Model (SAM) and similar models build a family of promptable foundation models (FMs) for image and video segmentation. The object of interest is identified using prompts, such as bounding boxes or points. With these FMs becoming part of medical image segmentation, extensive evaluation studies are required to assess their strengths and weaknesses in clinical setting. Since the performance is highly dependent on the chosen prompting strategy, it is important to investigate different prompting techniques to define optimal guidelines that ensure effective use in medical image segmentation. Currently, no dedicated evaluation studies exist specifically for bone segmentation in CT scans, leaving a gap in understanding the performance for this task. Thus, we use non-iterative, ``optimal'' prompting strategies composed of bounding box, points and combinations to test the zero-shot capability of SAM-family models for bone CT segmentation on three different skeletal regions. Our results show that the best settings depend on the model type and size, dataset characteristics and objective to optimize. Overall, SAM and SAM2 prompted with a bounding box in combination with the center point for all the components of an object yield the best results across all tested settings. As the results depend on multiple factors, we provide a guideline for informed decision-making in 2D prompting with non-interactive, ''optimal'' prompts. △ Less

Submitted 13 November, 2024; originally announced November 2024.

Water quality polluted by total suspended solids classified within an Artificial Neural Network approach

Authors: I. Luviano Soto, Y. Concha Sánchez, A. Raya

Abstract: This study investigates the application of an artificial neural network framework for analysing water pollution caused by solids. Water pollution by suspended solids poses significant environmental and health risks. Traditional methods for assessing and predicting pollution levels are often time-consuming and resource-intensive. To address these challenges, we developed a model that leverages a co… ▽ More This study investigates the application of an artificial neural network framework for analysing water pollution caused by solids. Water pollution by suspended solids poses significant environmental and health risks. Traditional methods for assessing and predicting pollution levels are often time-consuming and resource-intensive. To address these challenges, we developed a model that leverages a comprehensive dataset of water quality from total suspended solids. A convolutional neural network was trained under a transfer learning approach using data corresponding to different total suspended solids concentrations, with the goal of accurately predicting low, medium and high pollution levels based on various input variables. Our model demonstrated high predictive accuracy, outperforming conventional statistical methods in terms of both speed and reliability. The results suggest that the artificial neural network framework can serve as an effective tool for real-time monitoring and management of water pollution, facilitating proactive decision-making and policy formulation. This approach not only enhances our understanding of pollution dynamics but also underscores the potential of machine learning techniques in environmental science. △ Less

Submitted 18 October, 2024; originally announced October 2024.

Comments: 42 pages, 8 figures and 2 tables

MSC Class: Machine Learning

Temporal Hyperproperties for Population Protocols

Authors: Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty, César Sánchez

Abstract: Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since, in particular via an extension of the temporal logic LTL called HyperLTL. Most verification efforts for HyperLTL are restricted to finite-state systems, usually defined as Kripke structures. In this paper we study hyper… ▽ More Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since, in particular via an extension of the temporal logic LTL called HyperLTL. Most verification efforts for HyperLTL are restricted to finite-state systems, usually defined as Kripke structures. In this paper we study hyperproperties for an important class of infinite-state systems. We consider population protocols, a popular distributed computing model in which arbitrarily many identical finite-state agents interact in pairs. Population protocols are a good candidate for studying hyperproperties because the main decidable verification problem, well-specification, is a hyperproperty. We first show that even for simple (monadic) formulas, HyperLTL verification for population protocols is undecidable. We then turn our attention to immediate observation population protocols, a simpler and well-studied subclass of population protocols. We show that verification of monadic HyperLTL formulas without the next operator is decidable in 2-EXPSPACE, but that all extensions make the problem undecidable. △ Less

Submitted 15 October, 2024; originally announced October 2024.

Comments: 42 pages, 5 figures

Realizable Continuous-Space Shields for Safe Reinforcement Learning

Authors: Kyungmin Kim, Davide Corsi, Andoni Rodriguez, JB Lanier, Benjami Parellada, Pierre Baldi, Cesar Sanchez, Roy Fox

Abstract: While Deep Reinforcement Learning (DRL) has achieved remarkable success across various domains, it remains vulnerable to occasional catastrophic failures without additional safeguards. An effective solution to prevent these failures is to use a shield that validates and adjusts the agent's actions to ensure compliance with a provided set of safety specifications. For real-world robotic domains, it… ▽ More While Deep Reinforcement Learning (DRL) has achieved remarkable success across various domains, it remains vulnerable to occasional catastrophic failures without additional safeguards. An effective solution to prevent these failures is to use a shield that validates and adjusts the agent's actions to ensure compliance with a provided set of safety specifications. For real-world robotic domains, it is essential to define safety specifications over continuous state and action spaces to accurately account for system dynamics and compute new actions that minimally deviate from the agent's original decision. In this paper, we present the first shielding approach specifically designed to ensure the satisfaction of safety requirements in continuous state and action spaces, making it suitable for practical robotic applications. Our method builds upon realizability, an essential property that confirms the shield will always be able to generate a safe action for any state in the environment. We formally prove that realizability can be verified for stateful shields, enabling the incorporation of non-Markovian safety requirements, such as loop avoidance. Finally, we demonstrate the effectiveness of our approach in ensuring safety without compromising the policy's success rate by applying it to a navigation problem and a multi-agent particle environment. △ Less

Submitted 1 December, 2024; v1 submitted 2 October, 2024; originally announced October 2024.

Comments: Kim, Corsi, and Rodriguez contributed equally

Exploring AI Futures Through Fictional News Articles

Authors: Martin Lindstam, Elin Sporrong, Camilo Sanchez, Petra Jääskeläinen

Abstract: The aim of this workshop was to enable critical discussion on AI futures using fictional news articles and discussion groups. By collaboratively imagining and presenting future scenarios in a journalistic news article format, participants explored the socio-political, ethical and sustainability factors of AI through an accessible narrative form. Participants engaged in further anticipatory work by… ▽ More The aim of this workshop was to enable critical discussion on AI futures using fictional news articles and discussion groups. By collaboratively imagining and presenting future scenarios in a journalistic news article format, participants explored the socio-political, ethical and sustainability factors of AI through an accessible narrative form. Participants engaged in further anticipatory work by analyzing the issues raised by the articles in a group discussion, emphasizing the underlying motivations, assumptions and expectations conveyed within the news articles. △ Less

Submitted 10 September, 2024; originally announced September 2024.

Comments: Part of the Proceedings of WASP-HS Workshop Living with AI. Critical Questions for the Social Sciences and Humanities 2023 WASP-HS Conference

Journal ref: Part of the Proceedings of WASP-HS Workshop Living with AI. Critical Questions for the Social Sciences and Humanities 2023 WASP-HS Conference

What Guides Our Choices? Modeling Developers' Trust and Behavioral Intentions Towards GenAI

Authors: Rudrajit Choudhuri, Bianca Trinkenreich, Rahul Pandita, Eirini Kalliamvakou, Igor Steinmacher, Marco Gerosa, Christopher Sanchez, Anita Sarma

Abstract: Generative AI (genAI) tools, such as ChatGPT or Copilot, are advertised to improve developer productivity and are being integrated into software development. However, misaligned trust, skepticism, and usability concerns can impede the adoption of such tools. Research also indicates that AI can be exclusionary, failing to support diverse users adequately. One such aspect of diversity is cognitive d… ▽ More Generative AI (genAI) tools, such as ChatGPT or Copilot, are advertised to improve developer productivity and are being integrated into software development. However, misaligned trust, skepticism, and usability concerns can impede the adoption of such tools. Research also indicates that AI can be exclusionary, failing to support diverse users adequately. One such aspect of diversity is cognitive diversity -- variations in users' cognitive styles -- that leads to divergence in perspectives and interaction styles. When an individual's cognitive style is unsupported, it creates barriers to technology adoption. Therefore, to understand how to effectively integrate genAI tools into software development, it is first important to model what factors affect developers' trust and intentions to adopt genAI tools in practice? We developed a theoretically grounded statistical model to (1) identify factors that influence developers' trust in genAI tools and (2) examine the relationship between developers' trust, cognitive styles, and their intentions to use these tools in their work. We surveyed software developers (N=238) at two major global tech organizations: GitHub Inc. and Microsoft; and employed Partial Least Squares-Structural Equation Modeling (PLS-SEM) to evaluate our model. Our findings reveal that genAI's system/output quality, functional value, and goal maintenance significantly influence developers' trust in these tools. Furthermore, developers' trust and cognitive styles influence their intentions to use these tools in their work. We offer practical suggestions for designing genAI tools for effective use and inclusive user experience. △ Less

Submitted 2 December, 2024; v1 submitted 6 September, 2024; originally announced September 2024.

Comments: 13 pages, Accepted by 47th IEEE/ACM International Conference on Software Engineering (ICSE 2025)

Journal ref: 47th IEEE/ACM International Conference on Software Engineering (ICSE 2025)

Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

Authors: Andoni Rodríguez, Felipe Gorostiaga, César Sánchez

Abstract: Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLt specifications (i.e., LTL with propositions replaced by literals from a theory calT), into equi-realizable LTL specifications. In this paper we extend these results… ▽ More Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLt specifications (i.e., LTL with propositions replaced by literals from a theory calT), into equi-realizable LTL specifications. In this paper we extend these results into a full static synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory calT and outputs valuations of system variables from calT. We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLt specification. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full static synthesis method for LTLt, which is a deterministic program (hence predictable and efficient). △ Less

Submitted 12 July, 2024; originally announced July 2024.

Feelings about Bodies: Emotions on Diet and Fitness Forums Reveal Gendered Stereotypes and Body Image Concerns

Authors: Cinthia Sánchez, Minh Duc Chu, Zihao He, Rebecca Dorn, Stuart Murray, Kristina Lerman

Abstract: The gendered expectations about ideal body types can lead to body image concerns, dissatisfaction, and in extreme cases, disordered eating and other psychopathologies across the gender spectrum. While research has focused on pro-anorexia online communities that glorify the 'thin ideal', less attention has been given to the broader spectrum of body image concerns or how emerging disorders like musc… ▽ More The gendered expectations about ideal body types can lead to body image concerns, dissatisfaction, and in extreme cases, disordered eating and other psychopathologies across the gender spectrum. While research has focused on pro-anorexia online communities that glorify the 'thin ideal', less attention has been given to the broader spectrum of body image concerns or how emerging disorders like muscle dysmorphia ('bigorexia') present in online discussions. To address these gaps, we analyze 46 Reddit discussion forums related to diet, fitness, and associated mental health challenges. Using membership structure analysis and transformer-based language models, we project these communities along gender and body ideal axes, revealing complex interactions between gender, body ideals, and emotional expression. Our findings show that feminine-oriented communities generally express more negative emotions, particularly in thinness-promoting forums. Conversely, communities focused on the muscular ideal exhibit less negativity, regardless of gender orientation. We also uncover a gendered pattern in emotional indicators of mental health challenges, with communities discussing serious issues aligning more closely with thinness-oriented, predominantly feminine-leaning communities. By revealing the gendered emotional dynamics of online communities, our findings can inform the development of more effective content moderation approaches that facilitate supportive interactions, while minimizing exposure to potentially harmful content. △ Less

Submitted 3 July, 2024; originally announced July 2024.

Assessment of Sentinel-2 spatial and temporal coverage based on the scene classification layer

Authors: Cristhian Sanchez, Francisco Mena, Marcela Charfuelan, Marlon Nuske, Andreas Dengel

Abstract: Since the launch of the Sentinel-2 (S2) satellites, many ML models have used the data for diverse applications. The scene classification layer (SCL) inside the S2 product provides rich information for training, such as filtering images with high cloud coverage. However, there is more potential in this. We propose a technique to assess the clean optical coverage of a region, expressed by a SITS and… ▽ More Since the launch of the Sentinel-2 (S2) satellites, many ML models have used the data for diverse applications. The scene classification layer (SCL) inside the S2 product provides rich information for training, such as filtering images with high cloud coverage. However, there is more potential in this. We propose a technique to assess the clean optical coverage of a region, expressed by a SITS and calculated with the S2-based SCL data. With a manual threshold and specific labels in the SCL, the proposed technique assigns a percentage of spatial and temporal coverage across the time series and a high/low assessment. By evaluating the AI4EO challenge for Enhanced Agriculture, we show that the assessment is correlated to the predictive results of ML models. The classification results in a region with low spatial and temporal coverage is worse than in a region with high coverage. Finally, we applied the technique across all continents of the global dataset LandCoverNet. △ Less

Submitted 28 June, 2024; v1 submitted 6 June, 2024; originally announced June 2024.

Comments: Accepted at IEEE International Geoscience and Remote Sensing Symposium 2024

Threat analysis and adversarial model for Smart Grids

Authors: Javier Sande Ríos, Jesús Canal Sánchez, Carmen Manzano Hernandez, Sergio Pastrana

Abstract: The power grid is a critical infrastructure that allows for the efficient and robust generation, transmission, delivery and consumption of electricity. In the recent years, the physical components have been equipped with computing and network devices, which optimizes the operation and maintenance of the grid. The cyber domain of this smart power grid opens a new plethora of threats, which adds to… ▽ More The power grid is a critical infrastructure that allows for the efficient and robust generation, transmission, delivery and consumption of electricity. In the recent years, the physical components have been equipped with computing and network devices, which optimizes the operation and maintenance of the grid. The cyber domain of this smart power grid opens a new plethora of threats, which adds to classical threats on the physical domain. Accordingly, different stakeholders including regulation bodies, industry and academy, are making increasing efforts to provide security mechanisms to mitigate and reduce cyber-risks. Despite these efforts, there have been various cyberattacks that have affected the smart grid, leading in some cases to catastrophic consequences, showcasing that the industry might not be prepared for attacks from high profile adversaries. At the same time, recent work shows a lack of agreement among grid practitioners and academic experts on the feasibility and consequences of academic-proposed threats. This is in part due to inadequate simulation models which do not evaluate threats based on attackers full capabilities and goals. To address this gap, in this work we first analyze the main attack surfaces of the smart grid, and then conduct a threat analysis from the adversarial model perspective, including different levels of knowledge, goals, motivations and capabilities. To validate the model, we provide real-world examples of the potential capabilities by studying known vulnerabilities in critical components, and then analyzing existing cyber-attacks that have affected the smart grid, either directly or indirectly. △ Less

Submitted 17 June, 2024; originally announced June 2024.

Comments: Presented at the Workshop on Attackers and Cyber-Crime Operations (WACCO). More details available at https://wacco-workshop.org

Verification-Guided Shielding for Deep Reinforcement Learning

Authors: Davide Corsi, Guy Amir, Andoni Rodriguez, Cesar Sanchez, Guy Katz, Roy Fox

Abstract: In recent years, Deep Reinforcement Learning (DRL) has emerged as an effective approach to solving real-world tasks. However, despite their successes, DRL-based policies suffer from poor reliability, which limits their deployment in safety-critical domains. Various methods have been put forth to address this issue by providing formal safety guarantees. Two main approaches include shielding and ver… ▽ More In recent years, Deep Reinforcement Learning (DRL) has emerged as an effective approach to solving real-world tasks. However, despite their successes, DRL-based policies suffer from poor reliability, which limits their deployment in safety-critical domains. Various methods have been put forth to address this issue by providing formal safety guarantees. Two main approaches include shielding and verification. While shielding ensures the safe behavior of the policy by employing an external online component (i.e., a ``shield'') that overrides potentially dangerous actions, this approach has a significant computational cost as the shield must be invoked at runtime to validate every decision. On the other hand, verification is an offline process that can identify policies that are unsafe, prior to their deployment, yet, without providing alternative actions when such a policy is deemed unsafe. In this work, we present verification-guided shielding -- a novel approach that bridges the DRL reliability gap by integrating these two methods. Our approach combines both formal and probabilistic verification tools to partition the input domain into safe and unsafe regions. In addition, we employ clustering and symbolic representation procedures that compress the unsafe regions into a compact representation. This, in turn, allows to temporarily activate the shield solely in (potentially) unsafe regions, in an efficient manner. Our novel approach allows to significantly reduce runtime overhead while still preserving formal safety guarantees. We extensively evaluate our approach on two benchmarks from the robotic navigation domain, as well as provide an in-depth analysis of its scalability and completeness. △ Less

Submitted 20 June, 2024; v1 submitted 10 June, 2024; originally announced June 2024.

Comments: Accepted in the 1st Reinforcement Learning Conference (RLC), 2024. [Corsi and Amir contributed equally]

Shield Synthesis for LTL Modulo Theories

Authors: Andoni Rodriguez, Guy Amir, Davide Corsi, Cesar Sanchez, Guy Katz

Abstract: In recent years, Machine Learning (ML) models have achieved remarkable success in various domains. However, these models also tend to demonstrate unsafe behaviors, precluding their deployment in safety-critical systems. To cope with this issue, ample research focuses on developing methods that guarantee the safe behaviour of a given ML model. A prominent example is shielding which incorporates an… ▽ More In recent years, Machine Learning (ML) models have achieved remarkable success in various domains. However, these models also tend to demonstrate unsafe behaviors, precluding their deployment in safety-critical systems. To cope with this issue, ample research focuses on developing methods that guarantee the safe behaviour of a given ML model. A prominent example is shielding which incorporates an external component (a ``shield'') that blocks unwanted behavior. Despite significant progress, shielding suffers from a main setback: it is currently geared towards properties encoded solely in propositional logics (e.g., LTL) and is unsuitable for richer logics. This, in turn, limits the widespread applicability of shielding in many real-world systems. In this work, we address this gap, and extend shielding to LTL modulo theories, by building upon recent advances in reactive synthesis modulo theories. This allowed us to develop a novel approach for generating shields conforming to complex safety specifications in these more expressive, logics. We evaluated our shields and demonstrate their ability to handle rich data with temporal dynamics. To the best of our knowledge, this is the first approach for synthesizing shields for such expressivity. △ Less

Submitted 14 February, 2025; v1 submitted 6 June, 2024; originally announced June 2024.

Comments: To appear in AAAI 2025

Fast and Secure Decentralized Optimistic Rollups Using Setchain

Authors: Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sánchez, César Sánchez

Abstract: Modern blockchains face a scalability challenge due to the intrinsic throughput limitations of consensus protocols. Layer 2 optimistic rollups (L2) are a faster alternative that offer the same interface in terms of smart contract development and user interaction. Optimistic rollups perform most computations offchain and make light use of an underlying blockchain (L1) to guarantee correct behavior,… ▽ More Modern blockchains face a scalability challenge due to the intrinsic throughput limitations of consensus protocols. Layer 2 optimistic rollups (L2) are a faster alternative that offer the same interface in terms of smart contract development and user interaction. Optimistic rollups perform most computations offchain and make light use of an underlying blockchain (L1) to guarantee correct behavior, implementing a cheaper blockchain on a blockchain solution. With optimistic rollups, a sequencer calculates offchain batches of L2 transactions and commits batches (compressed or hashed) to the L1 blockchain. The use of hashes requires a data service to translate hashes into their corresponding batches. Current L2 implementations consist of a centralized sequencer (central authority) and an optional data availability committee (DAC). In this paper, we propose a decentralized L2 optimistic rollup based on Setchain, a decentralized Byzantine-tolerant implementation of sets. The main contribution is a fully decentralized "arranger" where arrangers are a formal definition combining sequencers and DACs. We prove our implementation correct and show empirical evidence that our solution scales. A final contribution is a system of incentives (payments) for servers that implement the sequencer and data availability committee protocols correctly, and a fraud-proof mechanism to detect violations of the protocol. △ Less

Submitted 4 June, 2024; originally announced June 2024.

Unifying Asynchronous Logics for Hyperproperties

Authors: Alberto Bombardelli, Laura Bozzelli, César Sánchez, Stefano Tonetta

Abstract: We introduce and investigate a powerful hyper logical framework in the linear-time setting, we call generalized HyperLTL with stuttering and contexts (GHyperLTL_SC for short). GHyperLTL_SC unifies known asynchronous extensions of HyperLTL and the well-known extension KLTL of LTL with knowledge modalities under both the synchronous and asynchronous perfect recall semantics. As a main contribution,… ▽ More We introduce and investigate a powerful hyper logical framework in the linear-time setting, we call generalized HyperLTL with stuttering and contexts (GHyperLTL_SC for short). GHyperLTL_SC unifies known asynchronous extensions of HyperLTL and the well-known extension KLTL of LTL with knowledge modalities under both the synchronous and asynchronous perfect recall semantics. As a main contribution, we individuate a meaningful fragment of GHyperLTL_SC, we call simple GHyperLTL_SC, with a decidable model-checking problem, which is more expressive than HyperLTL and known fragments of asynchronous extensions of HyperLTL with a decidable model-checking problem. Simple GHyperLTL_SC subsumes KLTL under the synchronous semantics and the one-agent fragment of KLTL under the asynchronous semantics, and to the best of our knowledge, it represents the unique hyper logic with a decidable model-checking problem which can express powerful non-regular trace properties when interpreted on singleton sets of traces. We justify the relevance of simple GHyperLTL_SC by showing that it can express diagnosability properties, interesting classes of information-flow security policies, both in the synchronous and asynchronous settings, and bounded termination (more in general, global promptness in the style of Prompt LTL). △ Less

Submitted 2 October, 2024; v1 submitted 25 April, 2024; originally announced April 2024.

Shared lightweight autonomous vehicles for urban food deliveries: A simulation study

Authors: Ainhoa Genua Cerviño, Naroa Coretti Sanchez, Elaine Liu Wang, Arnaud Grignard, Kent Larson

Abstract: In recent years, the rapid growth of on-demand deliveries, especially in food deliveries, has spurred the exploration of innovative mobility solutions. In this context, lightweight autonomous vehicles have emerged as a potential alternative. However, their fleet-level behavior remains largely unexplored. To address this gap, we have developed an agent-based model and an environmental impact study… ▽ More In recent years, the rapid growth of on-demand deliveries, especially in food deliveries, has spurred the exploration of innovative mobility solutions. In this context, lightweight autonomous vehicles have emerged as a potential alternative. However, their fleet-level behavior remains largely unexplored. To address this gap, we have developed an agent-based model and an environmental impact study assessing the fleet performance of lightweight autonomous food delivery vehicles. This model explores critical factors such as fleet sizing, service level, operational strategies, and environmental impacts. We have applied this model to a case study in Cambridge, MA, USA, where results indicate that there could be environmental benefits in replacing traditional car-based deliveries with shared lightweight autonomous vehicle fleets. Lastly, we introduce an interactive platform that offers a user-friendly means of comprehending the model's performance and potential trade-offs, which can help inform decision-makers in the evolving landscape of food delivery innovation. △ Less

Submitted 29 February, 2024; originally announced February 2024.

Comments: 17 pages, 25 including abstract, 16 figures, journal paper

The socialisation of the adolescent who carries out team sports: a transversal study of centrality with a social network analysis

Authors: Pilar Marqués-Sánchez, José Alberto Benítez-Andrades, María Dolores Calvo Sánchez, Natalia Arias

Abstract: Objectives: This study analyzed adolescent physical activity, its link to overweight, and the social network structure in group sports participants, focusing on centrality measures. Setting: Conducted in 11 classrooms across 5 schools in Ponferrada, Spain. Participants: Included 235 adolescents (49.4% female), categorized as normal weight or overweight. Methods: The Physical Activity Questio… ▽ More Objectives: This study analyzed adolescent physical activity, its link to overweight, and the social network structure in group sports participants, focusing on centrality measures. Setting: Conducted in 11 classrooms across 5 schools in Ponferrada, Spain. Participants: Included 235 adolescents (49.4% female), categorized as normal weight or overweight. Methods: The Physical Activity Questionnaire for Adolescents (PAQ-A) assessed physical activity levels. Social network analysis evaluated centrality in varying contact degrees. Results: 30.2% were overweight. Males scored higher in PAQ-A and were more likely to engage in group sports. No significant correlation was found between physical activity and weight in the total sample. However, overweight females reported higher exercise levels. Centrality analysis showed gender differences; women in group sports had lower centrality, whereas men had higher. Conclusions: The study highlights the importance of gender and social network centrality in designing future strategies, considering peer interaction intensity △ Less

Submitted 14 February, 2024; originally announced February 2024.

Journal ref: BMJ Open, 2021, Volume 11, ID e042773

Monitoring the Future of Smart Contracts

Authors: Margarita Capretto, Martin Ceresa, Cesar Sanchez

Abstract: Blockchains are decentralized systems that provide trustable execution guarantees. Smart contracts are programs written in specialized programming languages running on blockchains that govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other smart contracts during the execution of transactions always initiated by external users. Once deployed, smart contracts… ▽ More Blockchains are decentralized systems that provide trustable execution guarantees. Smart contracts are programs written in specialized programming languages running on blockchains that govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other smart contracts during the execution of transactions always initiated by external users. Once deployed, smart contracts cannot be modified, so techniques like runtime verification are very appealing for improving their reliability. However, the conventional model of computation of smart contracts is transactional: once operations commit, their effects are permanent and cannot be undone. In this paper, we proposed the concept of future monitors which allows monitors to remain waiting for future transactions to occur before committing or aborting. This is inspired by optimistic rollups, which are modern blockchain implementations that increase efficiency (and reduce cost) by delaying transaction effects. We exploit this delay to propose a model of computation that allows (bounded) future monitors. We show our monitors correct respect of legacy transactions, how they implement future bounded monitors and how they guarantee progress. We illustrate the use of future bounded monitors to implement correctly multi-transaction flash loans. △ Less

Submitted 22 January, 2024; originally announced January 2024.

Adaptive Fusion of Multi-view Remote Sensing data for Optimal Sub-field Crop Yield Prediction

Authors: Francisco Mena, Deepak Pathak, Hiba Najjar, Cristhian Sanchez, Patrick Helber, Benjamin Bischke, Peter Habelitz, Miro Miranda, Jayanth Siddamsetty, Marlon Nuske, Marcela Charfuelan, Diego Arenas, Michaela Vollmer, Andreas Dengel

Abstract: Accurate crop yield prediction is of utmost importance for informed decision-making in agriculture, aiding farmers, and industry stakeholders. However, this task is complex and depends on multiple factors, such as environmental conditions, soil properties, and management practices. Combining heterogeneous data views poses a fusion challenge, like identifying the view-specific contribution to the p… ▽ More Accurate crop yield prediction is of utmost importance for informed decision-making in agriculture, aiding farmers, and industry stakeholders. However, this task is complex and depends on multiple factors, such as environmental conditions, soil properties, and management practices. Combining heterogeneous data views poses a fusion challenge, like identifying the view-specific contribution to the predictive task. We present a novel multi-view learning approach to predict crop yield for different crops (soybean, wheat, rapeseed) and regions (Argentina, Uruguay, and Germany). Our multi-view input data includes multi-spectral optical images from Sentinel-2 satellites and weather data as dynamic features during the crop growing season, complemented by static features like soil properties and topographic information. To effectively fuse the data, we introduce a Multi-view Gated Fusion (MVGF) model, comprising dedicated view-encoders and a Gated Unit (GU) module. The view-encoders handle the heterogeneity of data sources with varying temporal resolutions by learning a view-specific representation. These representations are adaptively fused via a weighted sum. The fusion weights are computed for each sample by the GU using a concatenation of the view-representations. The MVGF model is trained at sub-field level with 10 m resolution pixels. Our evaluations show that the MVGF outperforms conventional models on the same task, achieving the best results by incorporating all the data sources, unlike the usual fusion results in the literature. For Argentina, the MVGF model achieves an R2 value of 0.68 at sub-field yield prediction, while at field level evaluation (comparing field averages), it reaches around 0.80 across different countries. The GU module learned different weights based on the country and crop-type, aligning with the variable significance of each data source to the prediction task. △ Less

Submitted 22 January, 2024; originally announced January 2024.

Journal ref: Remote Sensing of Environment, Volume 318, 2025

Nodule detection and generation on chest X-rays: NODE21 Challenge

Authors: Ecem Sogancioglu, Bram van Ginneken, Finn Behrendt, Marcel Bengs, Alexander Schlaefer, Miron Radu, Di Xu, Ke Sheng, Fabien Scalzo, Eric Marcus, Samuele Papa, Jonas Teuwen, Ernst Th. Scholten, Steven Schalekamp, Nils Hendrix, Colin Jacobs, Ward Hendrix, Clara I Sánchez, Keelin Murphy

Abstract: Pulmonary nodules may be an early manifestation of lung cancer, the leading cause of cancer-related deaths among both men and women. Numerous studies have established that deep learning methods can yield high-performance levels in the detection of lung nodules in chest X-rays. However, the lack of gold-standard public datasets slows down the progression of the research and prevents benchmarking of… ▽ More Pulmonary nodules may be an early manifestation of lung cancer, the leading cause of cancer-related deaths among both men and women. Numerous studies have established that deep learning methods can yield high-performance levels in the detection of lung nodules in chest X-rays. However, the lack of gold-standard public datasets slows down the progression of the research and prevents benchmarking of methods for this task. To address this, we organized a public research challenge, NODE21, aimed at the detection and generation of lung nodules in chest X-rays. While the detection track assesses state-of-the-art nodule detection systems, the generation track determines the utility of nodule generation algorithms to augment training data and hence improve the performance of the detection systems. This paper summarizes the results of the NODE21 challenge and performs extensive additional experiments to examine the impact of the synthetically generated nodule training images on the detection algorithm performance. △ Less

Submitted 4 January, 2024; originally announced January 2024.

Comments: 15 pages, 5 figures

Efficient Reactive Synthesis Using Mode Decomposition

Authors: Matías Brizzio, César Sánchez

Abstract: Developing critical components, such as mission controllers or embedded systems, is a challenging task. Reactive synthesis is a technique to automatically produce correct controllers. Given a high-level specification written in LTL, reactive synthesis consists of computing a system that satisfies the specification as long as the environment respects the assumptions. Unfortunately, LTL synthesis su… ▽ More Developing critical components, such as mission controllers or embedded systems, is a challenging task. Reactive synthesis is a technique to automatically produce correct controllers. Given a high-level specification written in LTL, reactive synthesis consists of computing a system that satisfies the specification as long as the environment respects the assumptions. Unfortunately, LTL synthesis suffers from high computational complexity which precludes its use for many large cases. A promising approach to improve synthesis scalability consists of decomposing a safety specification into smaller specifications, that can be processed independently and composed into a solution for the original specification. Previous decomposition methods focus on identifying independent parts of the specification whose systems are combined via simultaneous execution. In this work, we propose a novel decomposition algorithm based on modes, which consists of decomposing a complex safety specification into smaller problems whose solution is then composed sequentially (instead of simultaneously). The input to our algorithm is the original specification and the description of the modes. We show how to generate sub-specifications automatically and we prove that if all sub-problems are realizable then the full specification is realizable. Moreover, we show how to construct a system for the original specification from sub-systems for the decomposed specifications. We finally illustrate the feasibility of our approach with multiple case studies using off-the-self synthesis tools to process the obtained sub-problems. △ Less

Submitted 14 December, 2023; originally announced December 2023.

Comments: 19 pages

Spectrophotometers for Labs: a Cost-efficient Solution based on Smartphones

Authors: Carlos Balado Sánchez, Rebeca P. Díaz Redondo, Ana Fernández Vilas, Angel M. Sánchez Bermúdez

Abstract: In this paper we introduce a proposal to provide students in labs with an alternative to the traditional visible range spectrophotometers, whose acquisition and maintenance entails high costs, based on smartphones. Our solution faced two aspects. On the one hand, the software for the smartphone, able to perform the typical functionalities of the traditional spectrophotometers. On the other hand, t… ▽ More In this paper we introduce a proposal to provide students in labs with an alternative to the traditional visible range spectrophotometers, whose acquisition and maintenance entails high costs, based on smartphones. Our solution faced two aspects. On the one hand, the software for the smartphone, able to perform the typical functionalities of the traditional spectrophotometers. On the other hand, the portable peripheral support needed to capture the images to be analyzed in the smartphone. The promising results allow this solution to be applied in Bring Your Own Devices (BYOD) contexts. △ Less

Submitted 13 December, 2023; originally announced December 2023.

Journal ref: Computer Applications in Engineering Education, 2019, vol. 27, no 2, p. 371-379

Joint Supervised and Self-supervised Learning for MRI Reconstruction

Authors: George Yiasemis, Nikita Moriakov, Clara I. Sánchez, Jan-Jakob Sonke, Jonas Teuwen

Abstract: Magnetic Resonance Imaging (MRI) represents an important diagnostic modality; however, its inherently slow acquisition process poses challenges in obtaining fully-sampled $k$-space data under motion. In the absence of fully-sampled acquisitions, serving as ground truths, training deep learning algorithms in a supervised manner to predict the underlying ground truth image becomes challenging. To ad… ▽ More Magnetic Resonance Imaging (MRI) represents an important diagnostic modality; however, its inherently slow acquisition process poses challenges in obtaining fully-sampled $k$-space data under motion. In the absence of fully-sampled acquisitions, serving as ground truths, training deep learning algorithms in a supervised manner to predict the underlying ground truth image becomes challenging. To address this limitation, self-supervised methods have emerged as a viable alternative, leveraging available subsampled $k$-space data to train deep neural networks for MRI reconstruction. Nevertheless, these approaches often fall short when compared to supervised methods. We propose Joint Supervised and Self-supervised Learning (JSSL), a novel training approach for deep learning-based MRI reconstruction algorithms aimed at enhancing reconstruction quality in cases where target datasets containing fully-sampled $k$-space measurements are unavailable. JSSL operates by simultaneously training a model in a self-supervised learning setting, using subsampled data from the target dataset(s), and in a supervised learning manner, utilizing datasets with fully-sampled $k$-space data, referred to as proxy datasets. We demonstrate JSSL's efficacy using subsampled prostate or cardiac MRI data as the target datasets, with fully-sampled brain and knee, or brain, knee and prostate $k$-space acquisitions, respectively, as proxy datasets. Our results showcase substantial improvements over conventional self-supervised methods, validated using common image quality metrics. Furthermore, we provide theoretical motivations for JSSL and establish "rule-of-thumb" guidelines for training MRI reconstruction models. JSSL effectively enhances MRI reconstruction quality in scenarios where fully-sampled $k$-space data is not available, leveraging the strengths of supervised learning by incorporating proxy datasets. △ Less

Submitted 20 December, 2024; v1 submitted 27 November, 2023; originally announced November 2023.

Comments: pages, 14 figures, 6 tables

Boolean Abstractions for Realizability Modulo Theories (Extended version)

Authors: Andoni Rodriguez, Cesar Sanchez

Abstract: In this paper, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1) substituting theory literals by Boolean variables, and (2) computing an additional Boolean requirement that captures the dependencies between the new variables… ▽ More In this paper, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1) substituting theory literals by Boolean variables, and (2) computing an additional Boolean requirement that captures the dependencies between the new variables imposed by the literals. The resulting specification can be passed to existing Boolean off-the-shelf realizability tools, and is realizable if and only if the original specification is realizable. The first contribution is a brute-force version of our method, which requires a number of SMT queries that is doubly exponential in the number of input literals. Then, we present a faster method that exploits a nested encoding of the search for the extra requirement and uses SAT solving for faster traversing the search space and uses SMT queries internally. Another contribution is a prototype in Z3-Python. Finally, we report an empirical evaluation using specifications inspired in real industrial cases. To the best of our knowledge, this is the first method that succeeds in non-Boolean LTL realizability. △ Less

Submitted 26 October, 2023; originally announced October 2023.

From Realizability Modulo Theories to Synthesis Modulo Theories Part 1: Dynamic approach

Authors: Andoni Rodríguez, Cesar Sanchez

Abstract: Reactive synthesis is the process of using temporal logic specifications in LTL to generate correct controllers, but its use has been restricted to Boolean specifications. Recently, a Boolean abstraction technique allows to translate LTL T specifications that contain literals in theories into equi-realizable LTL specifications. However, no synthesis procedure exists yet. In synthesis modulo theori… ▽ More Reactive synthesis is the process of using temporal logic specifications in LTL to generate correct controllers, but its use has been restricted to Boolean specifications. Recently, a Boolean abstraction technique allows to translate LTL T specifications that contain literals in theories into equi-realizable LTL specifications. However, no synthesis procedure exists yet. In synthesis modulo theories, the system to synthesize receives valuations of environment variables in a first-order theory T and outputs valuations of system variables from T . In this paper, we address how to syntheize a full controller using a combination of the static Boolean controller obtained from the Booleanized LTL specification together with dynamic queries to a solver that produces models of a satisfiable existential formulae from T . This is the first method that realizes reactive synthesis modulo theories. △ Less

Submitted 11 October, 2023; originally announced October 2023.

Comparing Performance and Portability between CUDA and SYCL for Protein Database Search on NVIDIA, AMD, and Intel GPUs

Authors: Manuel Costanzo, Enzo Rucci, Carlos García Sánchez, Marcelo Naiouf, Manuel Prieto-Matías

Abstract: The heterogeneous computing paradigm has led to the need for portable and efficient programming solutions that can leverage the capabilities of various hardware devices, such as NVIDIA, Intel, and AMD GPUs. This study evaluates the portability and performance of the SYCL and CUDA languages for one fundamental bioinformatics application (Smith-Waterman protein database search) across different GPU… ▽ More The heterogeneous computing paradigm has led to the need for portable and efficient programming solutions that can leverage the capabilities of various hardware devices, such as NVIDIA, Intel, and AMD GPUs. This study evaluates the portability and performance of the SYCL and CUDA languages for one fundamental bioinformatics application (Smith-Waterman protein database search) across different GPU architectures, considering single and multi-GPU configurations from different vendors. The experimental work showed that, while both CUDA and SYCL versions achieve similar performance on NVIDIA devices, the latter demonstrated remarkable code portability to other GPU architectures, such as AMD and Intel. Furthermore, the architectural efficiency rates achieved on these devices were superior in 3 of the 4 cases tested. This brief study highlights the potential of SYCL as a viable solution for achieving both performance and portability in the heterogeneous computing ecosystem. △ Less

Submitted 10 November, 2023; v1 submitted 18 September, 2023; originally announced September 2023.

Comments: This article was accepted for publication in 2023 IEEE 35th International Symposium on Computer Architecture and High Performance Computing (SBAC-PAD)

Predicting Crop Yield With Machine Learning: An Extensive Analysis Of Input Modalities And Models On a Field and sub-field Level

Authors: Deepak Pathak, Miro Miranda, Francisco Mena, Cristhian Sanchez, Patrick Helber, Benjamin Bischke, Peter Habelitz, Hiba Najjar, Jayanth Siddamsetty, Diego Arenas, Michaela Vollmer, Marcela Charfuelan, Marlon Nuske, Andreas Dengel

Abstract: We introduce a simple yet effective early fusion method for crop yield prediction that handles multiple input modalities with different temporal and spatial resolutions. We use high-resolution crop yield maps as ground truth data to train crop and machine learning model agnostic methods at the sub-field level. We use Sentinel-2 satellite imagery as the primary modality for input data with other co… ▽ More We introduce a simple yet effective early fusion method for crop yield prediction that handles multiple input modalities with different temporal and spatial resolutions. We use high-resolution crop yield maps as ground truth data to train crop and machine learning model agnostic methods at the sub-field level. We use Sentinel-2 satellite imagery as the primary modality for input data with other complementary modalities, including weather, soil, and DEM data. The proposed method uses input modalities available with global coverage, making the framework globally scalable. We explicitly highlight the importance of input modalities for crop yield prediction and emphasize that the best-performing combination of input modalities depends on region, crop, and chosen model. △ Less

Submitted 17 August, 2023; originally announced August 2023.

Comments: 4 pages, 1 figure, 3 tables, IEEE IGARSS 2023

MSC Class: ACM-class: J.2

Retroactive Parametrized Monitoring

Authors: Paloma Pedregal, Felipe Gorostiaga, Cesar Sanchez

Abstract: In online monitoring, we first synthesize a monitor from a formal specification, which later runs in tandem with the system under study, incrementally receiving its progress and evolving with the system. In offline monitoring the trace is logged as the system progresses to later do post-mortem analysis after the system has finished executing. In this paper we propose retroactive dynamic parametr… ▽ More In online monitoring, we first synthesize a monitor from a formal specification, which later runs in tandem with the system under study, incrementally receiving its progress and evolving with the system. In offline monitoring the trace is logged as the system progresses to later do post-mortem analysis after the system has finished executing. In this paper we propose retroactive dynamic parametrization, a technique that allows a monitor to revisit the past log as it progresses, while still executing in an online manner. This feature allows new monitors to be incorporated into a running system and to revisit the past for particular behaviors based on new information discovered. Retroactive parametrization also allows a monitor to lazily ignore events and revisit and process them later, when it discovers that it should have followed those events. We showcase the use of retroactive dynamic parametrization to monitor denial of service attacks on a network using network logs. △ Less

Submitted 13 July, 2023; originally announced July 2023.

Experiential Futures In-the-wild to Inform Policy Design

Authors: Camilo Sanchez, Felix A. Epp

Abstract: As technological innovation continues to shape our world at an accelerating pace, policy makers struggle to keep up with the unintended consequences of these new technologies. To address this policy-novelty gap, Responsible Research Innovation (RRI) has been proposed as a way to drive science and technology innovation towards socially desirable goals. This work suggests a more active HCI's positio… ▽ More As technological innovation continues to shape our world at an accelerating pace, policy makers struggle to keep up with the unintended consequences of these new technologies. To address this policy-novelty gap, Responsible Research Innovation (RRI) has been proposed as a way to drive science and technology innovation towards socially desirable goals. This work suggests a more active HCI's position in the materialisation of pluralistic future visions and emphasizes the engagement between policy design and HCI for more agile and responsive evaluation environments. It calls for both fields to engage in questioning which and how futures are constructed, who they are benefiting, and how the findings of these interventions are interpreted towards other futures. △ Less

Submitted 24 March, 2023; originally announced March 2023.

Improving Blockchain Scalability with the Setchain Data-type

Authors: Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, Antonio Russo, César Sánchez

Abstract: Blockchain technologies are facing a scalability challenge, which must be overcome to guarantee a wider adoption of the technology. This scalability issue is due to the use of consensus algorithms to guarantee the total order of the chain of blocks and of the transactions within each block. However, total order is often not fully necessary, since important advanced applications of smart-contracts… ▽ More Blockchain technologies are facing a scalability challenge, which must be overcome to guarantee a wider adoption of the technology. This scalability issue is due to the use of consensus algorithms to guarantee the total order of the chain of blocks and of the transactions within each block. However, total order is often not fully necessary, since important advanced applications of smart-contracts do not require a total order among all operations. A much higher scalability can potentially be achieved if a more relaxed order can be exploited. In this paper, we propose a novel distributed concurrent data type, called Setchain, which improves scalability significantly. A Setchain implements a grow-only set whose elements are not ordered, unlike conventional blockchain operations. When convenient, the Setchain allows forcing a synchronization barrier that assigns permanently an epoch number to a subset of the latest elements added, agreed by consensus. Therefore, two operations in the same epoch are not ordered, while two operations in different epochs are ordered by their respective epoch number. We present different Byzantine-tolerant implementations of Setchain, prove their correctness and report on an empirical evaluation of a prototype implementation. Our results show that Setchain is orders of magnitude faster than consensus-based ledgers, since it implements grow-only sets with epoch synchronization instead of total order. Since Setchain barriers can be synchronized with the underlying blockchain, Setchain objects can be used as a sidechain to implement many decentralized solutions with much faster operations than direct implementations on top of blockchains. Finally, we also present an algorithm that encompasses in a single process the combined behavior of Byzantine servers, which simplifies correctness proofs by encoding the general attacker in a concrete implementation. △ Less

Submitted 9 February, 2023; originally announced February 2023.

Comments: 32 pages 6 figures. arXiv admin note: substantial text overlap with arXiv:2206.11845

Understanding metric-related pitfalls in image analysis validation

Authors: Annika Reinke, Minu D. Tizabi, Michael Baumgartner, Matthias Eisenmann, Doreen Heckmann-Nötzel, A. Emre Kavur, Tim Rädsch, Carole H. Sudre, Laura Acion, Michela Antonelli, Tal Arbel, Spyridon Bakas, Arriel Benis, Matthew Blaschko, Florian Buettner, M. Jorge Cardoso, Veronika Cheplygina, Jianxu Chen, Evangelia Christodoulou, Beth A. Cimini, Gary S. Collins, Keyvan Farahani, Luciana Ferrer, Adrian Galdran, Bram van Ginneken , et al. (53 additional authors not shown)

Abstract: Validation metrics are key for the reliable tracking of scientific progress and for bridging the current chasm between artificial intelligence (AI) research and its translation into practice. However, increasing evidence shows that particularly in image analysis, metrics are often chosen inadequately in relation to the underlying research problem. This could be attributed to a lack of accessibilit… ▽ More Validation metrics are key for the reliable tracking of scientific progress and for bridging the current chasm between artificial intelligence (AI) research and its translation into practice. However, increasing evidence shows that particularly in image analysis, metrics are often chosen inadequately in relation to the underlying research problem. This could be attributed to a lack of accessibility of metric-related knowledge: While taking into account the individual strengths, weaknesses, and limitations of validation metrics is a critical prerequisite to making educated choices, the relevant knowledge is currently scattered and poorly accessible to individual researchers. Based on a multi-stage Delphi process conducted by a multidisciplinary expert consortium as well as extensive community feedback, the present work provides the first reliable and comprehensive common point of access to information on pitfalls related to validation metrics in image analysis. Focusing on biomedical image analysis but with the potential of transfer to other fields, the addressed pitfalls generalize across application domains and are categorized according to a newly created, domain-agnostic taxonomy. To facilitate comprehension, illustrations and specific examples accompany each pitfall. As a structured body of information accessible to researchers of all levels of expertise, this work enhances global comprehension of a key topic in image analysis validation. △ Less

Submitted 23 February, 2024; v1 submitted 3 February, 2023; originally announced February 2023.

Comments: Shared first authors: Annika Reinke and Minu D. Tizabi; shared senior authors: Lena Maier-Hein and Paul F. Jäger. Published in Nature Methods. arXiv admin note: text overlap with arXiv:2206.01653

Journal ref: Nature methods, 1-13 (2024)

AIROGS: Artificial Intelligence for RObust Glaucoma Screening Challenge

Authors: Coen de Vente, Koenraad A. Vermeer, Nicolas Jaccard, He Wang, Hongyi Sun, Firas Khader, Daniel Truhn, Temirgali Aimyshev, Yerkebulan Zhanibekuly, Tien-Dung Le, Adrian Galdran, Miguel Ángel González Ballester, Gustavo Carneiro, Devika R G, Hrishikesh P S, Densen Puthussery, Hong Liu, Zekang Yang, Satoshi Kondo, Satoshi Kasai, Edward Wang, Ashritha Durvasula, Jónathan Heras, Miguel Ángel Zapata, Teresa Araújo , et al. (11 additional authors not shown)

Abstract: The early detection of glaucoma is essential in preventing visual impairment. Artificial intelligence (AI) can be used to analyze color fundus photographs (CFPs) in a cost-effective manner, making glaucoma screening more accessible. While AI models for glaucoma screening from CFPs have shown promising results in laboratory settings, their performance decreases significantly in real-world scenarios… ▽ More The early detection of glaucoma is essential in preventing visual impairment. Artificial intelligence (AI) can be used to analyze color fundus photographs (CFPs) in a cost-effective manner, making glaucoma screening more accessible. While AI models for glaucoma screening from CFPs have shown promising results in laboratory settings, their performance decreases significantly in real-world scenarios due to the presence of out-of-distribution and low-quality images. To address this issue, we propose the Artificial Intelligence for Robust Glaucoma Screening (AIROGS) challenge. This challenge includes a large dataset of around 113,000 images from about 60,000 patients and 500 different screening centers, and encourages the development of algorithms that are robust to ungradable and unexpected input data. We evaluated solutions from 14 teams in this paper, and found that the best teams performed similarly to a set of 20 expert ophthalmologists and optometrists. The highest-scoring team achieved an area under the receiver operating characteristic curve of 0.99 (95% CI: 0.98-0.99) for detecting ungradable images on-the-fly. Additionally, many of the algorithms showed robust performance when tested on three other publicly available datasets. These results demonstrate the feasibility of robust AI-enabled glaucoma screening. △ Less

Submitted 10 February, 2023; v1 submitted 3 February, 2023; originally announced February 2023.

Comments: 19 pages, 8 figures, 3 tables

Decentralized Stream Runtime Verification for Timed Asynchronous Networks

Authors: Luis Miguel Danielsson, César Sánchez

Abstract: We study the problem of monitoring distributed systems where computers communicate using message passing and share an almost synchronized clock. This is a realistic scenario for networks where the speed of the monitoring is sufficiently slow (at the human scale) to permit efficient clock synchronization, where the clock deviations is small compared to the monitoring cycles. This is the case when m… ▽ More We study the problem of monitoring distributed systems where computers communicate using message passing and share an almost synchronized clock. This is a realistic scenario for networks where the speed of the monitoring is sufficiently slow (at the human scale) to permit efficient clock synchronization, where the clock deviations is small compared to the monitoring cycles. This is the case when monitoring human systems in wide area networks, the Internet or including large deployments. More concretely, we study how to monitor decentralized systems where monitors are expressed as stream runtime verification specifications, under a timed asynchronous network. Our monitors communicate using the network, where messages can take arbitrarily long but cannot be duplicated or lost. This communication setting is common in many cyber-physical systems like smart buildings and ambient living. Previous approaches to decentralized monitoring were limited to synchronous networks, which are not easily implemented in practice because of network failures. Even when networks failures are unusual, they can require several monitoring cycles to be repaired. In this work we propose a solution to the timed asynchronous monitoring problem and show that this problem generalizes the synchronous case. We study the specifications and conditions on the network behavior that allow the monitoring to take place with bounded resources, independently of the trace length. Finally, we report the results of an empirical evaluation of an implementation and verify the theoretical results in terms of effectiveness and efficiency. △ Less

Submitted 3 February, 2023; v1 submitted 1 February, 2023; originally announced February 2023.

On Retrospective k-space Subsampling schemes For Deep MRI Reconstruction

Authors: George Yiasemis, Clara I. Sánchez, Jan-Jakob Sonke, Jonas Teuwen

Abstract: Acquiring fully-sampled MRI $k$-space data is time-consuming, and collecting accelerated data can reduce the acquisition time. Employing 2D Cartesian-rectilinear subsampling schemes is a conventional approach for accelerated acquisitions; however, this often results in imprecise reconstructions, even with the use of Deep Learning (DL), especially at high acceleration factors. Non-rectilinear or no… ▽ More Acquiring fully-sampled MRI $k$-space data is time-consuming, and collecting accelerated data can reduce the acquisition time. Employing 2D Cartesian-rectilinear subsampling schemes is a conventional approach for accelerated acquisitions; however, this often results in imprecise reconstructions, even with the use of Deep Learning (DL), especially at high acceleration factors. Non-rectilinear or non-Cartesian trajectories can be implemented in MRI scanners as alternative subsampling options. This work investigates the impact of the $k$-space subsampling scheme on the quality of reconstructed accelerated MRI measurements produced by trained DL models. The Recurrent Variational Network (RecurrentVarNet) was used as the DL-based MRI-reconstruction architecture. Cartesian, fully-sampled multi-coil $k$-space measurements from three datasets were retrospectively subsampled with different accelerations using eight distinct subsampling schemes: four Cartesian-rectilinear, two Cartesian non-rectilinear, and two non-Cartesian. Experiments were conducted in two frameworks: scheme-specific, where a distinct model was trained and evaluated for each dataset-subsampling scheme pair, and multi-scheme, where for each dataset a single model was trained on data randomly subsampled by any of the eight schemes and evaluated on data subsampled by all schemes. In both frameworks, RecurrentVarNets trained and evaluated on non-rectilinearly subsampled data demonstrated superior performance, particularly for high accelerations. In the multi-scheme setting, reconstruction performance on rectilinearly subsampled data improved when compared to the scheme-specific experiments. Our findings demonstrate the potential for using DL-based methods, trained on non-rectilinearly subsampled measurements, to optimize scan time and image quality. △ Less

Submitted 9 August, 2023; v1 submitted 19 January, 2023; originally announced January 2023.

Comments: 22 pages, 12 figures, 5 tables