Showing 1–50 of 90 results for author: Sanchez, C

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 develo** 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 develo** 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 6 June, 2024; originally announced June 2024.

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 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.

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: Develo** 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 Develo** 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

JSSL: 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 represents an important diagnostic modality; however, its inherently slow acquisition process poses challenges in obtaining fully sampled k-space data under motion in clinical scenarios such as abdominal, cardiac, and prostate imaging. In the absence of fully sampled acquisitions, which can serve as ground truth data, training deep learning algorithms in a supervised man… ▽ More Magnetic Resonance Imaging represents an important diagnostic modality; however, its inherently slow acquisition process poses challenges in obtaining fully sampled k-space data under motion in clinical scenarios such as abdominal, cardiac, and prostate imaging. In the absence of fully sampled acquisitions, which can serve as ground truth data, training deep learning algorithms in a supervised manner to predict the underlying ground truth image becomes an impossible task. To address this limitation, self-supervised methods have emerged as a viable alternative, leveraging available subsampled k-space data to train deep learning networks for MRI reconstruction. Nevertheless, these self-supervised approaches often fall short when compared to supervised methodologies. In this paper, we introduce JSSL (Joint Supervised and Self-supervised Learning), a novel training approach for deep learning-based MRI reconstruction algorithms aimed at enhancing reconstruction quality in scenarios where target dataset(s) containing fully sampled k-space measurements are unavailable. Our proposed method 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 data from other datasets, referred to as proxy datasets, where fully sampled k-space data is accessible. To demonstrate the efficacy of JSSL, we utilized subsampled prostate parallel MRI measurements as the target dataset, while employing fully sampled brain and knee k-space acquisitions as proxy datasets. Our results showcase a substantial improvement over conventional self-supervised training methods, thereby underscoring the effectiveness of our joint approach. We provide a theoretical motivation for JSSL and establish a practical "rule-of-thumb" for selecting the most appropriate training approach for deep MRI reconstruction. △ Less

Submitted 27 November, 2023; originally announced November 2023.

Comments: 26 pages, 11 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

Bounded Model Checking for Asynchronous Hyperproperties

Authors: Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez

Abstract: Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in (e.g., schedulers and asynchronous communication channels). In this paper, we focus on verification of confidentiality in nondeterministic environments by reasoning about asynchronous hyperproperties. First, we generalize the temporal logic A-HLTL to allow nested traj… ▽ More Many types of attacks on confidentiality stem from the nondeterministic nature of the environment that computer programs operate in (e.g., schedulers and asynchronous communication channels). In this paper, we focus on verification of confidentiality in nondeterministic environments by reasoning about asynchronous hyperproperties. First, we generalize the temporal logic A-HLTL to allow nested trajectory quantification, where a trajectory determines how different execution traces may advance and stutter. We propose a bounded model checking algorithm for A-HLTL based on QBF-solving for a fragment of the generalized A-HLTL and evaluate it by various case studies on concurrent programs, scheduling attacks, compiler optimization, speculative execution, and cache timing attacks. We also rigorously analyze the complexity of model checking for different fragments of A-HLTL. △ Less

Submitted 25 January, 2023; v1 submitted 17 January, 2023; originally announced January 2023.

Comments: 34 pages

Efficient Loop Conditions for Bounded Model Checking Hyperproperties

Authors: Tzu-Han Hsu, César Sánchez, Sarai Sheinvald, Borzoo Bonakdarpour

Abstract: Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC incorporates loop conditions that revisit previously observed states. This paper focuses on develo** loop conditions for BMC of HyperLTL- a temporal logic for hyperprop… ▽ More Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC incorporates loop conditions that revisit previously observed states. This paper focuses on develo** loop conditions for BMC of HyperLTL- a temporal logic for hyperproperties that allows expressing important policies for security and consistency in concurrent systems, etc. Loop conditions for HyperLTL are more complicated than for LTL, as different traces may loop inconsistently in unrelated moments. Existing BMC approaches for HyperLTL only considered linear unrollings without any loo** capability, which precludes both finding small infinite traces and obtaining a complete technique. We investigate loop conditions for HyperLTL BMC, where the HyperLTL formula can contain up to one quantifier alternation. We first present a general complete automata-based technique which is based on bounds of maximum unrollings. Then, we introduce alternative simulation-based algorithms that allow exploiting short loops effectively, generating SAT queries whose satisfiability guarantees the outcome of the original model checking problem. We also report empirical evaluation of the prototype implementation of our BMC techniques using Z3py. △ Less

Submitted 26 January, 2023; v1 submitted 15 January, 2023; originally announced January 2023.

Comments: 20 pages

The Effects of In-domain Corpus Size on pre-training BERT

Authors: Chris Sanchez, Zheyuan Zhang

Abstract: Many prior language modeling efforts have shown that pre-training on an in-domain corpus can significantly improve performance on downstream domain-specific NLP tasks. However, the difficulties associated with collecting enough in-domain data might discourage researchers from approaching this pre-training task. In this paper, we conducted a series of experiments by pre-training Bidirectional Encod… ▽ More Many prior language modeling efforts have shown that pre-training on an in-domain corpus can significantly improve performance on downstream domain-specific NLP tasks. However, the difficulties associated with collecting enough in-domain data might discourage researchers from approaching this pre-training task. In this paper, we conducted a series of experiments by pre-training Bidirectional Encoder Representations from Transformers (BERT) with different sizes of biomedical corpora. The results demonstrate that pre-training on a relatively small amount of in-domain data (4GB) with limited training steps, can lead to better performance on downstream domain-specific NLP tasks compared with fine-tuning models pre-trained on general corpora. △ Less

Submitted 15 December, 2022; originally announced December 2022.

Comments: 6 pages

Assessing Opportunities of SYCL for Biological Sequence Alignment on GPU-based Systems

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

Abstract: Bioinformatics and Computational Biology are two fields that have been exploiting GPUs for more than two decades, being CUDA the most used programming language for them. However, as CUDA is an NVIDIA proprietary language, it implies a strong portability restriction to a wide range of heterogeneous architectures, like AMD or Intel GPUs. To face this issue, the Khronos Group has recently proposed th… ▽ More Bioinformatics and Computational Biology are two fields that have been exploiting GPUs for more than two decades, being CUDA the most used programming language for them. However, as CUDA is an NVIDIA proprietary language, it implies a strong portability restriction to a wide range of heterogeneous architectures, like AMD or Intel GPUs. To face this issue, the Khronos Group has recently proposed the SYCL standard, which is an open, royalty-free, cross-platform abstraction layer, that enables the programming of a heterogeneous system to be written using standard, single-source C++ code. Over the past few years, several implementations of this SYCL standard have emerged, being oneAPI the one from Intel. This paper presents the migration process of the SW\# suite, a biological sequence alignment tool developed in CUDA, to SYCL using Intel's oneAPI ecosystem. The experimental results show that SW\# was completely migrated with a small programmer intervention in terms of hand-coding. In addition, it was possible to port the migrated code between different architectures (considering multiple vendor GPUs and also CPUs), with no noticeable performance degradation on 5 different NVIDIA GPUs. Moreover, performance remained stable when switching to another SYCL implementation. As a consequence, SYCL and its implementations can offer attractive opportunities for the Bioinformatics community, especially considering the vast existence of CUDA-based legacy codes. △ Less

Submitted 23 February, 2024; v1 submitted 19 November, 2022; originally announced November 2022.

Journal ref: J Supercomput (2024)

Zero-Knowledge Optimal Monetary Policy under Stochastic Dominance

Authors: David Cerezo Sánchez

Abstract: Optimal simple rules for the monetary policy of the first stochastically dominant crypto-currency are derived in a Dynamic Stochastic General Equilibrium (DSGE) model, in order to provide optimal responses to changes in inflation, output, and other sources of uncertainty. The optimal monetary policy stochastically dominates all the previous crypto-currencies, thus the efficient portfolio is to go… ▽ More Optimal simple rules for the monetary policy of the first stochastically dominant crypto-currency are derived in a Dynamic Stochastic General Equilibrium (DSGE) model, in order to provide optimal responses to changes in inflation, output, and other sources of uncertainty. The optimal monetary policy stochastically dominates all the previous crypto-currencies, thus the efficient portfolio is to go long on the stochastically dominant crypto-currency: a strategy-proof arbitrage featuring a higher Omega ratio with higher expected returns, inducing an investment-efficient Nash equilibrium over the crypto-market. Zero-knowledge proofs of the monetary policy are committed on the blockchain: an implementation is provided. △ Less

Submitted 12 October, 2022; originally announced October 2022.

Comments: Implementation available at: https://github.com/Calctopia-OpenSource/cothority/tree/zkmonpolicy

Revisiting Syllables in Language Modelling and their Application on Low-Resource Machine Translation

Authors: Arturo Oncevay, Kervy Dante Rivas Rojas, Liz Karen Chavez Sanchez, Roberto Zariquiey

Abstract: Language modelling and machine translation tasks mostly use subword or character inputs, but syllables are seldom used. Syllables provide shorter sequences than characters, require less-specialised extracting rules than morphemes, and their segmentation is not impacted by the corpus size. In this study, we first explore the potential of syllables for open-vocabulary language modelling in 21 langua… ▽ More Language modelling and machine translation tasks mostly use subword or character inputs, but syllables are seldom used. Syllables provide shorter sequences than characters, require less-specialised extracting rules than morphemes, and their segmentation is not impacted by the corpus size. In this study, we first explore the potential of syllables for open-vocabulary language modelling in 21 languages. We use rule-based syllabification methods for six languages and address the rest with hyphenation, which works as a syllabification proxy. With a comparable perplexity, we show that syllables outperform characters and other subwords. Moreover, we study the importance of syllables on neural machine translation for a non-related and low-resource language-pair (Spanish--Shipibo-Konibo). In pairwise and multilingual systems, syllables outperform unsupervised subwords, and further morphological segmentation methods, when translating into a highly synthetic language with a transparent orthography (Shipibo-Konibo). Finally, we perform some human evaluation, and discuss limitations and opportunities. △ Less

Submitted 5 October, 2022; originally announced October 2022.

Comments: COLING 2022, short-paper

Cross-Lingual and Cross-Domain Crisis Classification for Low-Resource Scenarios

Authors: Cinthia Sánchez, Hernan Sarmiento, Andres Abeliuk, Jorge Pérez, Barbara Poblete

Abstract: Social media data has emerged as a useful source of timely information about real-world crisis events. One of the main tasks related to the use of social media for disaster management is the automatic identification of crisis-related messages. Most of the studies on this topic have focused on the analysis of data for a particular type of event in a specific language. This limits the possibility of… ▽ More Social media data has emerged as a useful source of timely information about real-world crisis events. One of the main tasks related to the use of social media for disaster management is the automatic identification of crisis-related messages. Most of the studies on this topic have focused on the analysis of data for a particular type of event in a specific language. This limits the possibility of generalizing existing approaches because models cannot be directly applied to new types of events or other languages. In this work, we study the task of automatically classifying messages that are related to crisis events by leveraging cross-language and cross-domain labeled data. Our goal is to make use of labeled data from high-resource languages to classify messages from other (low-resource) languages and/or of new (previously unseen) types of crisis situations. For our study we consolidated from the literature a large unified dataset containing multiple crisis events and languages. Our empirical findings show that it is indeed possible to leverage data from crisis events in English to classify the same type of event in other languages, such as Spanish and Italian (80.0% F1-score). Furthermore, we achieve good performance for the cross-domain task (80.0% F1-score) in a cross-lingual setting. Overall, our work contributes to improving the data scarcity problem that is so important for multilingual crisis classification. In particular, mitigating cold-start situations in emergency events, when time is of essence. △ Less

Submitted 31 October, 2022; v1 submitted 5 September, 2022; originally announced September 2022.

Comments: Accepted at the International AAAI Conference on Web and Social Media (ICWSM 2023)

Neurosymbolic Repair for Low-Code Formula Languages

Authors: Rohan Bavishi, Harshit Joshi, José Pablo Cambronero Sánchez, Anna Fariha, Sumit Gulwani, Vu Le, Ivan Radicek, Ashish Tiwari

Abstract: Most users of low-code platforms, such as Excel and PowerApps, write programs in domain-specific formula languages to carry out nontrivial tasks. Often users can write most of the program they want, but introduce small mistakes that yield broken formulas. These mistakes, which can be both syntactic and semantic, are hard for low-code users to identify and fix, even though they can be resolved with… ▽ More Most users of low-code platforms, such as Excel and PowerApps, write programs in domain-specific formula languages to carry out nontrivial tasks. Often users can write most of the program they want, but introduce small mistakes that yield broken formulas. These mistakes, which can be both syntactic and semantic, are hard for low-code users to identify and fix, even though they can be resolved with just a few edits. We formalize the problem of producing such edits as the last-mile repair problem. To address this problem, we developed LaMirage, a LAst-MIle RepAir-engine GEnerator that combines symbolic and neural techniques to perform last-mile repair in low-code formula languages. LaMirage takes a grammar and a set of domain-specific constraints/rules, which jointly approximate the target language, and uses these to generate a repair engine that can fix formulas in that language. To tackle the challenges of localizing the errors and ranking the candidate repairs, LaMirage leverages neural techniques, whereas it relies on symbolic methods to generate candidate repairs. This combination allows LaMirage to find repairs that satisfy the provided grammar and constraints, and then pick the most natural repair. We compare LaMirage to state-of-the-art neural and symbolic approaches on 400 real Excel and PowerFx formulas, where LaMirage outperforms all baselines. We release these benchmarks to encourage subsequent work in low-code domains. △ Less

Submitted 24 July, 2022; originally announced July 2022.

Multi: a Formal Playground for Multi-Smart Contract Interaction

Authors: Martán Ceresa, César Sánchez

Abstract: Blockchains are maintained by a network of participants that run algorithms designed to maintain collectively a distributed machine tolerant to Byzantine attacks. From the point of view of users, blockchains provide the illusion of centralized computers that perform trustable verifiable computations, where all computations are deterministic and the results cannot be manipulated or undone. Smart-co… ▽ More Blockchains are maintained by a network of participants that run algorithms designed to maintain collectively a distributed machine tolerant to Byzantine attacks. From the point of view of users, blockchains provide the illusion of centralized computers that perform trustable verifiable computations, where all computations are deterministic and the results cannot be manipulated or undone. Smart-contracts are written in a special-purpose programming language with deterministic semantics. Each transaction begins with an invocation from an external user to a smart contract. Contracts have local storage and can call other contracts, and more importantly, they store, send and receive cryptocurrency. It is very important to guarantee that contracts are correct before deployment since their code cannot be modified afterward deployment. However, the resulting ecosystem makes it very difficult to reason about program correctness, since contracts can be executed by malicious users or malicious contracts can be designed to exploit other contracts that call them. Many attacks and bugs are caused by unexpected interactions between multiple contracts, the attacked contract and unknown code that performs the exploit. Moreover, there is a very aggressive competition between different blockchains to expand their user base. Ideas are implemented fast and blockchains compete to offer and adopt new features quickly. In this paper, we propose a formal extensible playground that allows reasoning about multi-contract interactions to ultimately prove properties before features are incorporated into the real blockchain. We implemented a model of computation that models the execution platform, abstracts the internal code of each individual contract and focuses on contract interactions. Moreover, we show how many features, existing or proposed, can be used to reason about multi-contract interactions. △ Less

Submitted 14 July, 2022; originally announced July 2022.

Symbolic Runtime Verification for Monitoring under Uncertainties and Assumptions

Authors: Hannes Kallwies, Martin Leucker, Cesar Sanchez

Abstract: Runtime Verification deals with the question of whether a run of a system adheres to its specification. This paper studies runtime verification in the presence of partial knowledge about the observed run, particularly where input values may not be precise or may not be observed at all. We also allow declaring assumptions on the execution which permits to obtain more precise verdicts also under… ▽ More Runtime Verification deals with the question of whether a run of a system adheres to its specification. This paper studies runtime verification in the presence of partial knowledge about the observed run, particularly where input values may not be precise or may not be observed at all. We also allow declaring assumptions on the execution which permits to obtain more precise verdicts also under imprecise inputs. To this end, we show how to understand a given correctness property as a symbolic formula and explain that monitoring boils down to solving this formula iteratively, whenever more and more observations of the run are given. We base our framework on stream runtime verification, which allows to express temporal correctness properties not only in the Boolean but also in richer logical theories. While in general our approach requires to consider larger and larger sets of formulas, we identify domains (including Booleans and Linear Algebra) for which pruning strategies exist, which allows to monitor with constant memory (i.e. independent of the length of the observation) while preserving the same inference power as the monitor that remembers all observations. We empirically exhibit the power of our technique using a prototype implementation under two important cases studies: software for testing car emissions and heart-rate monitoring. △ Less

Submitted 12 July, 2022; originally announced July 2022.

Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties

Authors: Laura Bozzelli, Adriano Peron, Cesar Sanchez

Abstract: Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applic… ▽ More Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applications e.g. for asynchronous security analysis. In this paper, we address expressiveness and decidability issues of temporal logics for asynchronous hyperproperties. We compare the expressiveness of these logics together with the extension S1S[E] of S1S with the equal-level predicate by obtaining an almost complete expressiveness picture. We also study the expressive power of these logics when interpreted on singleton sets of traces. We show that for two asynchronous extensions of HyperLTL, checking the existence of a singleton model is already undecidable, and for one of them, namely Context HyperLTL (HyperLTL_C), we establish a characterization of the singleton models in terms of the extension of standard FO[<] over traces with addition. This last result generalizes the well-known equivalence between FO[<] and LTL. Finally, we identify new boundaries on the decidability of model checking HyperLTL_C. △ Less

Submitted 6 July, 2022; originally announced July 2022.

Transaction Monitoring of Smart Contracts

Authors: Margarita Capretto, Martin Ceresa, Cesar Sanchez

Abstract: Blockchains are modern distributed systems that provide decentralized financial capabilities with trustable guarantees. Smart contracts are programs written in specialized programming languages running on a blockchain and govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other contracts during the execution of transactions initiated by external users. Once de… ▽ More Blockchains are modern distributed systems that provide decentralized financial capabilities with trustable guarantees. Smart contracts are programs written in specialized programming languages running on a blockchain and govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other contracts during the execution of transactions initiated by external users. Once deployed, smart contracts cannot be modified and their pitfalls can cause malfunctions and losses, for example by attacks from malicious users. Runtime verification is a very appealing technique to improve the reliability of smart contracts. One approach consists of specifying undesired executions (never claims) and detecting violations of the specification on the fly. This can be done by extending smart contracts with additional instructions corresponding to monitor specified properties, resulting in an onchain monitoring approach. In this paper, we study transaction monitoring that consists of detecting violations of complete transaction executions and not of individual operations within transactions. Our main contributions are to show that transaction monitoring is not possible in most blockchains and propose different execution mechanisms that would enable transaction monitoring. △ Less

Submitted 6 July, 2022; originally announced July 2022.

Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers

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 mostly caused by the use of consensus algorithms to guarantee the total order of the chain of blocks (and of the operations within each block). However, total order is often overkilling, since important advanced applications of smart-contract… ▽ More Blockchain technologies are facing a scalability challenge, which must be overcome to guarantee a wider adoption of the technology. This scalability issue is mostly caused by the use of consensus algorithms to guarantee the total order of the chain of blocks (and of the operations within each block). However, total order is often overkilling, since important advanced applications of smart-contracts do not require a total order of all the operations. Hence, if a more relaxed partial order (instead of a total order) is allowed under certain safety conditions, a much higher scalability can be achieved. In this paper, we propose a distributed concurrent data type, called Setchain, that allows implementing this partial order and increases significantly blockchain scalability. A Setchain implements a grow-only set object whose elements are not totally 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. With the Setchain, operations in the same epoch are not ordered, while operations in different epochs are. We present different Byzantine-tolerant implementations of Setchain, prove their correctness and report on an empirical evaluation of a direct implementation. Our results show that Setchain is orders of magnitude faster than consensus-based ledgers to implement grow-only sets with epoch synchronization. Since the Setchain barriers can be synchronized with block consolidation, Setchain objects can be used as a sidechain to implement many smart contract solutions with much faster operations than on basic blockchains. △ Less

Submitted 23 June, 2022; originally announced June 2022.

Metrics reloaded: Recommendations for image analysis validation

Authors: Lena Maier-Hein, Annika Reinke, Patrick Godau, Minu D. Tizabi, Florian Buettner, Evangelia Christodoulou, Ben Glocker, Fabian Isensee, Jens Kleesiek, Michal Kozubek, Mauricio Reyes, Michael A. Riegler, Manuel Wiesenfarth, A. Emre Kavur, Carole H. Sudre, Michael Baumgartner, Matthias Eisenmann, Doreen Heckmann-Nötzel, Tim Rädsch, Laura Acion, Michela Antonelli, Tal Arbel, Spyridon Bakas, Arriel Benis, Matthew Blaschko , et al. (49 additional authors not shown)

Abstract: Increasing evidence shows that flaws in machine learning (ML) algorithm validation are an underestimated global problem. Particularly in automatic biomedical image analysis, chosen performance metrics often do not reflect the domain interest, thus failing to adequately measure scientific progress and hindering translation of ML techniques into practice. To overcome this, our large international ex… ▽ More Increasing evidence shows that flaws in machine learning (ML) algorithm validation are an underestimated global problem. Particularly in automatic biomedical image analysis, chosen performance metrics often do not reflect the domain interest, thus failing to adequately measure scientific progress and hindering translation of ML techniques into practice. To overcome this, our large international expert consortium created Metrics Reloaded, a comprehensive framework guiding researchers in the problem-aware selection of metrics. Following the convergence of ML methodology across application domains, Metrics Reloaded fosters the convergence of validation methodology. The framework was developed in a multi-stage Delphi process and is based on the novel concept of a problem fingerprint - a structured representation of the given problem that captures all aspects that are relevant for metric selection, from the domain interest to the properties of the target structure(s), data set and algorithm output. Based on the problem fingerprint, users are guided through the process of choosing and applying appropriate validation metrics while being made aware of potential pitfalls. Metrics Reloaded targets image analysis problems that can be interpreted as a classification task at image, object or pixel level, namely image-level classification, object detection, semantic segmentation, and instance segmentation tasks. To improve the user experience, we implemented the framework in the Metrics Reloaded online tool, which also provides a point of access to explore weaknesses, strengths and specific recommendations for the most common validation metrics. The broad applicability of our framework across domains is demonstrated by an instantiation for various biological and medical image analysis use cases. △ Less

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

Comments: Shared first authors: Lena Maier-Hein, Annika Reinke. arXiv admin note: substantial text overlap with arXiv:2104.05642 Published in Nature Methods

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

A Tableau Method for the Realizability and Synthesis of Reactive Safety Specifications

Authors: Montserrat Hermo, Paqui Lucio, César Sánchez

Abstract: We introduce a tableau decision method for deciding realizability of specifications expressed in a safety fragment of LTL that includes bounded future temporal operators. Tableau decision procedures for temporal and modal logics have been thoroughly studied for satisfiability and for translating temporal formulae into equivalent Büchi automata, and also for model checking, where a specification an… ▽ More We introduce a tableau decision method for deciding realizability of specifications expressed in a safety fragment of LTL that includes bounded future temporal operators. Tableau decision procedures for temporal and modal logics have been thoroughly studied for satisfiability and for translating temporal formulae into equivalent Büchi automata, and also for model checking, where a specification and system are provided. However, to the best of our knowledge no tableau method has been studied for the reactive synthesis problem. Reactive synthesis starts from a specification where propositional variables are split into those controlled by the environment and those controlled by the system, and consists on automatically producing a system that guarantees the specification for all environments. Realizability is the decision problem of whether there is one such system. In this paper we present a method to decide realizability of safety specifications, from which we can also extract (i.e. synthesize) a correct system (in case the specification is realizable). Our method can easily be extended to handle richer domains (integers, etc) and bounds in the temporal operators in ways that automata approaches for synthesis cannot. △ Less

Submitted 3 June, 2022; originally announced June 2022.

Comments: 35 pages

BronchoPose: an analysis of data and model configuration for vision-based bronchoscopy pose estimation

Authors: Juan Borrego-Carazo, Carles Sánchez, David Castells-Rufas, Jordi Carrabina, Débora Gil

Abstract: Vision-based bronchoscopy (VB) models require the registration of the virtual lung model with the frames from the video bronchoscopy to provide effective guidance during the biopsy. The registration can be achieved by either tracking the position and orientation of the bronchoscopy camera or by calibrating its deviation from the pose (position and orientation) simulated in the virtual lung model.… ▽ More Vision-based bronchoscopy (VB) models require the registration of the virtual lung model with the frames from the video bronchoscopy to provide effective guidance during the biopsy. The registration can be achieved by either tracking the position and orientation of the bronchoscopy camera or by calibrating its deviation from the pose (position and orientation) simulated in the virtual lung model. Recent advances in neural networks and temporal image processing have provided new opportunities for guided bronchoscopy. However, such progress has been hindered by the lack of comparative experimental conditions. In the present paper, we share a novel synthetic dataset allowing for a fair comparison of methods. Moreover, this paper investigates several neural network architectures for the learning of temporal information at different levels of subject personalization. In order to improve orientation measurement, we also present a standardized comparison framework and a novel metric for camera orientation learning. Results on the dataset show that the proposed metric and architectures, as well as the standardized conditions, provide notable improvements to current state-of-the-art camera pose estimation in video bronchoscopy. △ Less

Submitted 25 April, 2022; originally announced April 2022.

A deep learning framework for the detection and quantification of drusen and reticular pseudodrusen on optical coherence tomography

Authors: Roy Schwartz, Hagar Khalid, Sandra Liakopoulos, Yanling Ouyang, Coen de Vente, Cristina González-Gonzalo, Aaron Y. Lee, Robyn Guymer, Emily Y. Chew, Catherine Egan, Zhichao Wu, Himeesh Kumar, Joseph Farrington, Clara I. Sánchez, Adnan Tufail

Abstract: Purpose - To develop and validate a deep learning (DL) framework for the detection and quantification of drusen and reticular pseudodrusen (RPD) on optical coherence tomography scans. Design - Development and validation of deep learning models for classification and feature segmentation. Methods - A DL framework was developed consisting of a classification model and an out-of-distribution (OOD… ▽ More Purpose - To develop and validate a deep learning (DL) framework for the detection and quantification of drusen and reticular pseudodrusen (RPD) on optical coherence tomography scans. Design - Development and validation of deep learning models for classification and feature segmentation. Methods - A DL framework was developed consisting of a classification model and an out-of-distribution (OOD) detection model for the identification of ungradable scans; a classification model to identify scans with drusen or RPD; and an image segmentation model to independently segment lesions as RPD or drusen. Data were obtained from 1284 participants in the UK Biobank (UKBB) with a self-reported diagnosis of age-related macular degeneration (AMD) and 250 UKBB controls. Drusen and RPD were manually delineated by five retina specialists. The main outcome measures were sensitivity, specificity, area under the ROC curve (AUC), kappa, accuracy and intraclass correlation coefficient (ICC). Results - The classification models performed strongly at their respective tasks (0.95, 0.93, and 0.99 AUC, respectively, for the ungradable scans classifier, the OOD model, and the drusen and RPD classification model). The mean ICC for drusen and RPD area vs. graders was 0.74 and 0.61, respectively, compared with 0.69 and 0.68 for intergrader agreement. FROC curves showed that the model's sensitivity was close to human performance. Conclusions - The models achieved high classification and segmentation performance, similar to human performance. Application of this robust framework will further our understanding of RPD as a separate entity from drusen in both research and clinical settings. △ Less

Submitted 5 April, 2022; originally announced April 2022.

Comments: 26 pages, 7 figures

Migrating CUDA to oneAPI: A Smith-Waterman Case Study

Authors: Manuel Costanzo, Enzo Rucci, Carlos Garcia Sanchez, Marcelo Naiouf, Manuel Prieto-Matias

Abstract: To face the programming challenges related to heterogeneous computing, Intel recently introduced oneAPI, a new programming environment that allows code developed in Data Parallel C++ (DPC++) language to be run on different devices such as CPUs, GPUs, FPGAs, among others. To tackle CUDA-based legacy codes, oneAPI provides a compatibility tool (dpct) that facilitates the migration to DPC++. Due to t… ▽ More To face the programming challenges related to heterogeneous computing, Intel recently introduced oneAPI, a new programming environment that allows code developed in Data Parallel C++ (DPC++) language to be run on different devices such as CPUs, GPUs, FPGAs, among others. To tackle CUDA-based legacy codes, oneAPI provides a compatibility tool (dpct) that facilitates the migration to DPC++. Due to the large amount of existing CUDA-based software in the bioinformatics context, this paper presents our experiences porting SW#db, a well-known sequence alignment tool, to DPC++ using dpct. From the experimental work, it was possible to prove the usefulness of dpct for SW#db code migration and the cross-GPU vendor, cross-architecture portability of the migrated DPC++ code. In addition, the performance results showed that the migrated DPC++ code reports similar efficiency rates to its CUDA-native counterpart or even better in some tests (approximately +5%). △ Less

Submitted 20 June, 2022; v1 submitted 21 March, 2022; originally announced March 2022.

Comments: Accepted in IWBBIO 2022

Journal ref: In: Bioinformatics and Biomedical Engineering. IWBBIO 2022. Lecture Notes in Computer Science(), vol 13347. Springer, Cham (2022)

Can autonomy make bicycle-sharing systems more sustainable? Environmental impact analysis of an emerging mobility technology

Authors: Naroa Coretti Sanchez, Luis Alonso Pastor, Kent Larson

Abstract: Autonomous bicycles have recently been proposed as a new and more efficient approach to bicycle-sharing systems (BSS), but the corresponding environmental implications remain unresearched. Conducting environmental impact assessments at an early technological stage is critical to influencing the design and, ultimately, environmental impacts of a system. Consequently, this paper aims to assess the e… ▽ More Autonomous bicycles have recently been proposed as a new and more efficient approach to bicycle-sharing systems (BSS), but the corresponding environmental implications remain unresearched. Conducting environmental impact assessments at an early technological stage is critical to influencing the design and, ultimately, environmental impacts of a system. Consequently, this paper aims to assess the environmental impact of autonomous shared bikes compared with current station-based and dockless systems under different sets of modeling hypotheses and mode-shift scenarios. The results indicate that autonomy could reduce the environmental impact per passenger kilometer traveled of current station-based and dockless BSS by 33.1 % and 58.0 %. The sensitivity analysis shows that the environmental impact of autonomous shared bicycles will mainly depend on vehicle usage rates and the need for infrastructure. Finally, this study highlights the importance of targeting the mode replacement from more polluting modes, especially as traditional mobility modes decarbonize and become more efficient. △ Less

Submitted 24 February, 2022; originally announced February 2022.

Report number: Volume 113

Journal ref: Transportation Research Part D: Transport and Environment, 2022

Recurrent Variational Network: A Deep Learning Inverse Problem Solver applied to the task of Accelerated MRI Reconstruction

Authors: George Yiasemis, Jan-Jakob Sonke, Clarisa Sánchez, Jonas Teuwen

Abstract: Magnetic Resonance Imaging can produce detailed images of the anatomy and physiology of the human body that can assist doctors in diagnosing and treating pathologies such as tumours. However, MRI suffers from very long acquisition times that make it susceptible to patient motion artifacts and limit its potential to deliver dynamic treatments. Conventional approaches such as Parallel Imaging and Co… ▽ More Magnetic Resonance Imaging can produce detailed images of the anatomy and physiology of the human body that can assist doctors in diagnosing and treating pathologies such as tumours. However, MRI suffers from very long acquisition times that make it susceptible to patient motion artifacts and limit its potential to deliver dynamic treatments. Conventional approaches such as Parallel Imaging and Compressed Sensing allow for an increase in MRI acquisition speed by reconstructing MR images from sub-sampled MRI data acquired using multiple receiver coils. Recent advancements in Deep Learning combined with Parallel Imaging and Compressed Sensing techniques have the potential to produce high-fidelity reconstructions from highly accelerated MRI data. In this work we present a novel Deep Learning-based Inverse Problem solver applied to the task of Accelerated MRI Reconstruction, called the Recurrent Variational Network (RecurrentVarNet), by exploiting the properties of Convolutional Recurrent Neural Networks and unrolled algorithms for solving Inverse Problems. The RecurrentVarNet consists of multiple recurrent blocks, each responsible for one iteration of the unrolled variational optimization scheme for solving the inverse problem of multi-coil Accelerated MRI Reconstruction. Contrary to traditional approaches, the optimization steps are performed in the observation domain ($k$-space) instead of the image domain. Each block of the RecurrentVarNet refines the observed $k$-space and comprises a data consistency term and a recurrent unit which takes as input a learned hidden state and the prediction of the previous block. Our proposed method achieves new state of the art qualitative and quantitative reconstruction results on 5-fold and 10-fold accelerated data from a public multi-coil brain dataset, outperforming previous conventional and deep learning-based approaches. △ Less

Submitted 29 March, 2022; v1 submitted 18 November, 2021; originally announced November 2021.

Comments: 18 pages, 10 figures, 3 tables, CVPR 22

HyperQB: A QBF-Based Bounded Model Checker for Hyperproperties

Authors: Tzu-Han Hsu, Borzoo Bonakdarpour, César Sánchez

Abstract: We present HyperQB, a push-button QBF-based bounded model checker for hyperproperties. HyperQB takes as input a NuSMV model and a formula expressed in the temporal logic HyperLTL. Our QBF-based technique allows HyperQB to seamlessly deal with quantifier alternations. Based on the selection of either bug hunting or synthesis, the instances of counterexamples (for negated formula) or witnesses (for… ▽ More We present HyperQB, a push-button QBF-based bounded model checker for hyperproperties. HyperQB takes as input a NuSMV model and a formula expressed in the temporal logic HyperLTL. Our QBF-based technique allows HyperQB to seamlessly deal with quantifier alternations. Based on the selection of either bug hunting or synthesis, the instances of counterexamples (for negated formula) or witnesses (for synthesis of positive formulas) are returned. We report on successful and effective verification for a rich set of experiments on a variety of case studies, including information-flow security, concurrent data structures, path planning for robots, co-termination, deniability, intransitivity of non-interference, and secrecy-preserving refinement. We also rigorously compare and contrast HyperQB with existing tools for model checking hyperporperties. △ Less

Submitted 24 January, 2024; v1 submitted 21 September, 2021; originally announced September 2021.

JUBILEE: Secure Debt Relief and Forgiveness

Authors: David Cerezo Sánchez

Abstract: JUBILEE is a securely computed mechanism for debt relief and forgiveness in a frictionless manner without involving trusted third parties, leading to more harmonious debt settlements by incentivising the parties to truthfully reveal their private information. JUBILEE improves over all previous methods: - individually rational, incentive-compatible, truthful/strategy-proof, ex-post efficient, opt… ▽ More JUBILEE is a securely computed mechanism for debt relief and forgiveness in a frictionless manner without involving trusted third parties, leading to more harmonious debt settlements by incentivising the parties to truthfully reveal their private information. JUBILEE improves over all previous methods: - individually rational, incentive-compatible, truthful/strategy-proof, ex-post efficient, optimal mechanism for debt relief and forgiveness with private information - by the novel introduction of secure computation techniques to debt relief, the "blessing of the debtor" is hereby granted for the first time: debt settlements with higher expected profits and a higher probability of success than without using secure computation A simple and practical implementation is included for "The Secure Spreadsheet". Another implementation is realised using Raziel smart contracts on a blockchain with Pravuil consensus. △ Less

Submitted 15 September, 2021; originally announced September 2021.

Lane level context and hidden space characterization for autonomous driving

Authors: Corentin Sanchez, Philippe Xu, Alexandre Armand, Philippe Bonnifait

Abstract: For an autonomous vehicle, situation understand-ing is a key capability towards safe and comfortable decision-making and navigation. Information is in general provided bymultiple sources. Prior information about the road topology andtraffic laws can be given by a High Definition (HD) map whilethe perception system provides the description of the spaceand of road entities evolving in the vehicle su… ▽ More For an autonomous vehicle, situation understand-ing is a key capability towards safe and comfortable decision-making and navigation. Information is in general provided bymultiple sources. Prior information about the road topology andtraffic laws can be given by a High Definition (HD) map whilethe perception system provides the description of the spaceand of road entities evolving in the vehicle surroundings. Incomplex situations such as those encountered in urban areas,the road user behaviors are governed by strong interactionswith the others, and with the road network. In such situations,reliable situation understanding is therefore mandatory to avoidinappropriate decisions. Nevertheless, situation understandingis a complex task that requires access to a consistent andnon-misleading representation of the vehicle surroundings. Thispaper proposes a formalism (an interaction lane grid) whichallows to represent, with different levels of abstraction, thenavigable and interacting spaces which must be considered forsafe navigation. A top-down approach is chosen to assess andcharacterize the relevant information of the situation. On a highlevel of abstraction, the identification of the areas of interestwhere the vehicle should pay attention is depicted. On a lowerlevel, it enables to characterize the spatial information in aunified representation and to infer additional information inoccluded areas by reasoning with dynamic objects. △ Less

Submitted 21 October, 2021; v1 submitted 31 August, 2021; originally announced August 2021.

Journal ref: 31st IEEE Intelligent Vehicles Symposium (IV 2020), Oct 2020, Las Vegas, United States. pp.144-149

Deep MRI Reconstruction with Radial Subsampling

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

Abstract: In spite of its extensive adaptation in almost every medical diagnostic and examinatorial application, Magnetic Resonance Imaging (MRI) is still a slow imaging modality which limits its use for dynamic imaging. In recent years, Parallel Imaging (PI) and Compressed Sensing (CS) have been utilised to accelerate the MRI acquisition. In clinical settings, subsampling the k-space measurements during sc… ▽ More In spite of its extensive adaptation in almost every medical diagnostic and examinatorial application, Magnetic Resonance Imaging (MRI) is still a slow imaging modality which limits its use for dynamic imaging. In recent years, Parallel Imaging (PI) and Compressed Sensing (CS) have been utilised to accelerate the MRI acquisition. In clinical settings, subsampling the k-space measurements during scanning time using Cartesian trajectories, such as rectilinear sampling, is currently the most conventional CS approach applied which, however, is prone to producing aliased reconstructions. With the advent of the involvement of Deep Learning (DL) in accelerating the MRI, reconstructing faithful images from subsampled data became increasingly promising. Retrospectively applying a subsampling mask onto the k-space data is a way of simulating the accelerated acquisition of k-space data in real clinical setting. In this paper we compare and provide a review for the effect of applying either rectilinear or radial retrospective subsampling on the quality of the reconstructions outputted by trained deep neural networks. With the same choice of hyper-parameters, we train and evaluate two distinct Recurrent Inference Machines (RIMs), one for each type of subsampling. The qualitative and quantitative results of our experiments indicate that the model trained on data with radial subsampling attains higher performance and learns to estimate reconstructions with higher fidelity paving the way for other DL approaches to involve radial subsampling. △ Less

Submitted 12 January, 2022; v1 submitted 17 August, 2021; originally announced August 2021.

Comments: 9 pages, 7 figures, 1 table

Report number: Proc. SPIE 12031, Medical Imaging 2022: Physics of Medical Imaging, 1203136

Simulation study on the fleet performance of shared autonomous bicycles

Authors: Naroa Coretti Sánchez, Iñigo Martinez, Luis Alonso Pastor, Kent Larson

Abstract: Rethinking cities is now more imperative than ever, as society faces global challenges such as population growth and climate change. The design of cities can not be abstracted from the design of its mobility system, and, therefore, efficient solutions must be found to transport people and goods throughout the city in an ecological way. An autonomous bicycle-sharing system would combine the most re… ▽ More Rethinking cities is now more imperative than ever, as society faces global challenges such as population growth and climate change. The design of cities can not be abstracted from the design of its mobility system, and, therefore, efficient solutions must be found to transport people and goods throughout the city in an ecological way. An autonomous bicycle-sharing system would combine the most relevant benefits of vehicle sharing, electrification, autonomy, and micro-mobility, increasing the efficiency and convenience of bicycle-sharing systems and incentivizing more people to bike and enjoy their cities in an environmentally friendly way. Due to the uniqueness and radical novelty of introducing autonomous driving technology into bicycle-sharing systems and the inherent complexity of these systems, there is a need to quantify the potential impact of autonomy on fleet performance and user experience. This paper presents an ad-hoc agent-based simulator that provides an in-depth understanding of the fleet behavior of autonomous bicycle-sharing systems in realistic scenarios, including a rebalancing system based on demand prediction. In addition, this work describes the impact of different parameters on system efficiency and service quality and quantifies the extent to which an autonomous system would outperform current bicycle-sharing schemes. The obtained results show that with a fleet size three and a half times smaller than a station-based system and eight times smaller than a dockless system, an autonomous system can provide overall improved performance and user experience even with no rebalancing. These findings indicate that the remarkable efficiency of an autonomous bicycle-sharing system could compensate for the additional cost of autonomous bicycles. △ Less

Submitted 21 June, 2021; v1 submitted 17 June, 2021; originally announced June 2021.

Report number: 100065

Journal ref: Communications in Transportation Research, Volume 2, December 2022