-
Translating a VDM Model of a Medical Device into Kapture
Authors:
Joe Hare,
Leo Freitas,
Ken Pierce
Abstract:
As the complexity of safety-critical medical devices increases, so does the need for clear, verifiable, software requirements. This paper explores the use of Kapture, a formal modelling tool developed by D-RisQ, to translate an existing formal VDM model of a medical implant for treating focal epilepsy called CANDO. The work was undertaken without prior experience in formal methods. The paper asses…
▽ More
As the complexity of safety-critical medical devices increases, so does the need for clear, verifiable, software requirements. This paper explores the use of Kapture, a formal modelling tool developed by D-RisQ, to translate an existing formal VDM model of a medical implant for treating focal epilepsy called CANDO. The work was undertaken without prior experience in formal methods. The paper assess Kapture's usability, the challenges of formal modelling, and the effectiveness of the translated model. The result is a model in Kapture which covers over 90% of the original VDM model, and produces matching traces of results. While several issues were encountered during design and implementation, mainly due to the initial learning curve, this paper demonstrates that complex systems can be effectively modelled in Kapture by inexperienced users and highlights some difficulties in translating VDM specifications to Kapture.
△ Less
Submitted 11 June, 2025;
originally announced June 2025.
-
Generalizing the Invertible Matrix Theorem with Linear Relations using Graphical Linear Algebra
Authors:
Iago Leal de Freitas,
Júlia Mota,
João Paixão,
Lucas Rufino
Abstract:
Linear algebra's main concerns are sets of vectors, linear functions, subspaces, linear systems, matrices and concepts about those, such as whether the solution of linear system exists or is unique; a set of vectors is linearly independent or spans the whole space; a linear function has a right or a left inverse; a linear function is surjective or injective; and the kernel of a matrix is trivial o…
▽ More
Linear algebra's main concerns are sets of vectors, linear functions, subspaces, linear systems, matrices and concepts about those, such as whether the solution of linear system exists or is unique; a set of vectors is linearly independent or spans the whole space; a linear function has a right or a left inverse; a linear function is surjective or injective; and the kernel of a matrix is trivial or the its image is full.
The Invertible Matrix Theorem ties all these ideas and many others together. Many modern linear algebra books use this theorem as a guiding principle to explain many connections in linear algebra. The main idea is to separately characterize whether the linear function is surjective or injective. The proof usually uses a matrix decomposition as the key step. However, the invertible matrix theorem deals with a single linear function, a single set of vectors, a single subspace, and a single matrix.
In this work, we generalize part of the invertible matrix theorem to results about a pair of linear functions, a pair of sets of vectors, a pair of subspaces, and a single linear relation. The main idea is to separately characterize the linear relation's fundamental properties -- whether it is surjective, injective, deterministic and total. Our proof uses a decomposition of a linear relation as the key step.
Unfortunately, reasoning with linear relations in classical notation requires applying many rules besides shuffling quantifiers and variables around, which can obscure the symmetries in the results. Therefore, this work employs graphical linear algebra, a two-dimensional diagrammatic syntax with the fundamental rules of linear relations built-in.
△ Less
Submitted 13 April, 2025; v1 submitted 23 February, 2025;
originally announced February 2025.
-
Leveraging graph neural networks and mobility data for COVID-19 forecasting
Authors:
Fernando H. O. Duarte,
Gladston J. P. Moreira,
Eduardo J. S. Luz,
Leonardo B. L. Santos,
Vander L. S. Freitas
Abstract:
The COVID-19 pandemic has victimized over 7 million people to date, prompting diverse research efforts. Spatio-temporal models combining mobility data with machine learning have gained attention for disease forecasting. Here, we explore Graph Convolutional Recurrent Network (GCRN) and Graph Convolutional Long Short-Term Memory (GCLSTM), which combine the power of Graph Neural Networks (GNN) with t…
▽ More
The COVID-19 pandemic has victimized over 7 million people to date, prompting diverse research efforts. Spatio-temporal models combining mobility data with machine learning have gained attention for disease forecasting. Here, we explore Graph Convolutional Recurrent Network (GCRN) and Graph Convolutional Long Short-Term Memory (GCLSTM), which combine the power of Graph Neural Networks (GNN) with traditional architectures that deal with sequential data. The aim is to forecast future values of COVID-19 cases in Brazil and China by leveraging human mobility networks, whose nodes represent geographical locations and links are flows of vehicles or people. We show that employing backbone extraction to filter out negligible connections in the mobility network enhances predictive stability. Comparing regression and classification tasks demonstrates that binary classification yields smoother, more interpretable results. Interestingly, we observe qualitatively equivalent results for both Brazil and China datasets by introducing sliding windows of variable size and prediction horizons. Compared to prior studies, introducing the sliding window and the network backbone extraction strategies yields improvements of about 80% in root mean squared errors.
△ Less
Submitted 20 January, 2025;
originally announced January 2025.
-
Uma proposta para o uso de RPG no Ensino de Física: A Vingança de Newton
Authors:
Maria Rita Vasconcelos Brandão Souza,
Luís Henrique de Freitas,
Glaucia de Souza Silva,
Felipe Xavier de Carvalho,
Leonardo Antônio M. Souza
Abstract:
This work explores the use of Role Playing Games (RPG) as an active methodology in teaching Modern Physics, focusing on a game called Newton's Revenge. The game was developed with the aim of engaging students in collaborative and investigative learning processes, using gamification elements to increase motivation and involvement. Based on the constructivist theories of Piaget and Vygotsky, the RPG…
▽ More
This work explores the use of Role Playing Games (RPG) as an active methodology in teaching Modern Physics, focusing on a game called Newton's Revenge. The game was developed with the aim of engaging students in collaborative and investigative learning processes, using gamification elements to increase motivation and involvement. Based on the constructivist theories of Piaget and Vygotsky, the RPG stimu-\newline lates cognitive and social development by placing students in the roles of historical science figures. Through contextualized physical challenges, such as understanding the Photoelectric Effect, participants actively construct knowledge. This study presents preliminary learning data obtained through pre- and post-tests, as well as evaluates students' perceptions of using educational games in science education. The results indicate that the use of RPG can be an effective tool for teaching Modern Physics, promoting greater engagement and understanding of scientific concepts.
△ Less
Submitted 26 November, 2024;
originally announced November 2024.
-
Federated Learning in Chemical Engineering: A Tutorial on a Framework for Privacy-Preserving Collaboration Across Distributed Data Sources
Authors:
Siddhant Dutta,
Iago Leal de Freitas,
Pedro Maciel Xavier,
Claudio Miceli de Farias,
David Esteban Bernal Neira
Abstract:
Federated Learning (FL) is a decentralized machine learning approach that has gained attention for its potential to enable collaborative model training across clients while protecting data privacy, making it an attractive solution for the chemical industry. This work aims to provide the chemical engineering community with an accessible introduction to the discipline. Supported by a hands-on tutori…
▽ More
Federated Learning (FL) is a decentralized machine learning approach that has gained attention for its potential to enable collaborative model training across clients while protecting data privacy, making it an attractive solution for the chemical industry. This work aims to provide the chemical engineering community with an accessible introduction to the discipline. Supported by a hands-on tutorial and a comprehensive collection of examples, it explores the application of FL in tasks such as manufacturing optimization, multimodal data integration, and drug discovery while addressing the unique challenges of protecting proprietary information and managing distributed datasets. The tutorial was built using key frameworks such as $\texttt{Flower}$ and $\texttt{TensorFlow Federated}$ and was designed to provide chemical engineers with the right tools to adopt FL in their specific needs. We compare the performance of FL against centralized learning across three different datasets relevant to chemical engineering applications, demonstrating that FL will often maintain or improve classification performance, particularly for complex and heterogeneous data. We conclude with an outlook on the open challenges in federated learning to be tackled and current approaches designed to remediate and improve this framework.
△ Less
Submitted 12 February, 2025; v1 submitted 23 November, 2024;
originally announced November 2024.
-
Markov switching zero-inflated space-time multinomial models for comparing multiple infectious diseases
Authors:
Dirk Douwes-Schultz,
Alexandra M. Schmidt,
Laís Picinini Freitas,
Marilia Sá Carvalho
Abstract:
Despite multivariate spatio-temporal counts often containing many zeroes, zero-inflated multinomial models for space-time data have not been considered. We are interested in comparing the transmission dynamics of several co-circulating infectious diseases across space and time where some can be absent for long periods. We first assume there is a baseline disease that is well-established and always…
▽ More
Despite multivariate spatio-temporal counts often containing many zeroes, zero-inflated multinomial models for space-time data have not been considered. We are interested in comparing the transmission dynamics of several co-circulating infectious diseases across space and time where some can be absent for long periods. We first assume there is a baseline disease that is well-established and always present in the region. The other diseases switch between periods of presence and absence in each area through a series of coupled Markov chains, which account for long periods of disease absence, disease interactions and disease spread from neighboring areas. Since we are mainly interested in comparing the diseases, we assume the cases of the present diseases in an area jointly follow an autoregressive multinomial model. We use the multinomial model to investigate whether there are associations between certain factors, such as temperature, and differences in the transmission intensity of the diseases. Inference is performed using efficient Bayesian Markov chain Monte Carlo methods based on jointly sampling all presence indicators. We apply the model to spatio-temporal counts of dengue, Zika and chikungunya cases in Rio de Janeiro, during the first triple epidemic.
△ Less
Submitted 21 October, 2024;
originally announced October 2024.
-
Proceedings of the 22nd International Overture Workshop
Authors:
Hugo Daniel Macedo,
Ken Pierce,
Leo Freitas
Abstract:
This volume contains the papers presented at the 22nd International Overture Workshop, held on the 10th of September 2024. This event was the latest in a series of workshops around the Vienna Development Method (VDM), the open-source project Overture, and related tools and formalisms. VDM is one of the longest established formal methods for systems development. A lively community of researchers an…
▽ More
This volume contains the papers presented at the 22nd International Overture Workshop, held on the 10th of September 2024. This event was the latest in a series of workshops around the Vienna Development Method (VDM), the open-source project Overture, and related tools and formalisms. VDM is one of the longest established formal methods for systems development. A lively community of researchers and practitioners has grown up in academia and industry has grown around the modelling languages (VDM-SL, VDM++, VDM-RT, CML) and tools (VDMTools, Overture, Crescendo, Symphony, the INTO-CPS chain, and ViennaTalk). Together, these provide a platform for work on modelling and analysis technology that includes static and dynamic analysis, test generation, execution support, and model checking. This workshop provided updates on the emerging technology of VDM/Overture, including collaboration infrastructure, collaborative modelling and co-simulation for Cyber-Physical Systems.
△ Less
Submitted 30 September, 2024;
originally announced October 2024.
-
Federated Learning with Quantum Computing and Fully Homomorphic Encryption: A Novel Computing Paradigm Shift in Privacy-Preserving ML
Authors:
Siddhant Dutta,
Pavana P Karanth,
Pedro Maciel Xavier,
Iago Leal de Freitas,
Nouhaila Innan,
Sadok Ben Yahia,
Muhammad Shafique,
David E. Bernal Neira
Abstract:
The widespread deployment of products powered by machine learning models is raising concerns around data privacy and information security worldwide. To address this issue, Federated Learning was first proposed as a privacy-preserving alternative to conventional methods that allow multiple learning clients to share model knowledge without disclosing private data. A complementary approach known as F…
▽ More
The widespread deployment of products powered by machine learning models is raising concerns around data privacy and information security worldwide. To address this issue, Federated Learning was first proposed as a privacy-preserving alternative to conventional methods that allow multiple learning clients to share model knowledge without disclosing private data. A complementary approach known as Fully Homomorphic Encryption (FHE) is a quantum-safe cryptographic system that enables operations to be performed on encrypted weights. However, implementing mechanisms such as these in practice often comes with significant computational overhead and can expose potential security threats. Novel computing paradigms, such as analog, quantum, and specialized digital hardware, present opportunities for implementing privacy-preserving machine learning systems while enhancing security and mitigating performance loss. This work instantiates these ideas by applying the FHE scheme to a Federated Learning Neural Network architecture that integrates both classical and quantum layers.
△ Less
Submitted 12 October, 2024; v1 submitted 13 September, 2024;
originally announced September 2024.
-
Rorqual: Speeding up Narwhal with TEEs
Authors:
Luciano Freitas,
Shashank Motepalli,
Matej Pavlovic,
Benjamin Livshits
Abstract:
In this paper, we introduce Rorqual, a protocol designed to enhance the performance of the Narwhal Mempool by integrating Trusted Execution Environments (TEEs). Both Narwhal and Roqual are protocols based on a Directed Acyclic Graph (DAG). Compared to Narwhal, Rorqual achieves significant reductions in latency and increases throughput by streamlining the steps required to include a vertex in the D…
▽ More
In this paper, we introduce Rorqual, a protocol designed to enhance the performance of the Narwhal Mempool by integrating Trusted Execution Environments (TEEs). Both Narwhal and Roqual are protocols based on a Directed Acyclic Graph (DAG). Compared to Narwhal, Rorqual achieves significant reductions in latency and increases throughput by streamlining the steps required to include a vertex in the DAG. The use of TEEs also reduces the communication complexity of the protocol while maintaining low computational costs. Through rigorous analysis, we demonstrate the protocol's robustness under both normal and adversarial conditions, highlighting its improvements in throughput, latency, and security.
△ Less
Submitted 26 August, 2024;
originally announced August 2024.
-
Asynchronous Latency and Fast Atomic Snapshot
Authors:
João Paulo Bezerra,
Luciano Freitas,
Petr Kuznetsov
Abstract:
This paper introduces a novel, fast atomic-snapshot protocol for asynchronous message-passing systems. In the process of defining what ``fast'' means exactly, we spot a few interesting issues that arise when conventional time metrics are applied to long-lived asynchronous algorithms. We reveal some gaps in latency claims made in earlier work on snapshot algorithms, which hamper their comparative t…
▽ More
This paper introduces a novel, fast atomic-snapshot protocol for asynchronous message-passing systems. In the process of defining what ``fast'' means exactly, we spot a few interesting issues that arise when conventional time metrics are applied to long-lived asynchronous algorithms. We reveal some gaps in latency claims made in earlier work on snapshot algorithms, which hamper their comparative time-complexity analysis. We then come up with a new unifying time-complexity metric that captures the latency of an operation in an asynchronous, long-lived implementation. This allows us to formally grasp latency improvements of our atomic-snapshot algorithm with respect to the state-of-the-art protocols: optimal latency in fault-free runs without contention, short constant latency in fault-free runs with contention, the worst-case latency proportional to the number of active concurrent failures, and constant, close to optimal, amortized latency.
△ Less
Submitted 22 May, 2025; v1 submitted 5 August, 2024;
originally announced August 2024.
-
Large-scale Epidemiological modeling: Scanning for Mosquito-Borne Diseases Spatio-temporal Patterns in Brazil
Authors:
Eduardo C. Araujo,
Claudia T. Codeço,
Sandro Loch,
Luã B. Vacaro,
Laís P. Freitas,
Raquel M. Lana,
Leonardo S. Bastos,
Iasmim F. de Almeida,
Fernanda Valente,
Luiz M. Carvalho,
Flávio C. Coelho
Abstract:
The influence of climate on mosquito-borne diseases like dengue and chikungunya is well-established, but comprehensively tracking long-term spatial and temporal trends across large areas has been hindered by fragmented data and limited analysis tools. This study presents an unprecedented analysis, in terms of breadth, estimating the SIR transmission parameters from incidence data in all 5,570 muni…
▽ More
The influence of climate on mosquito-borne diseases like dengue and chikungunya is well-established, but comprehensively tracking long-term spatial and temporal trends across large areas has been hindered by fragmented data and limited analysis tools. This study presents an unprecedented analysis, in terms of breadth, estimating the SIR transmission parameters from incidence data in all 5,570 municipalities in Brazil over 14 years (2010-2023) for both dengue and chikungunya. We describe the Episcanner computational pipeline, developed to estimate these parameters, producing a reusable dataset describing all dengue and chikungunya epidemics that have taken place in this period, in Brazil. The analysis reveals new insights into the climate-epidemic nexus: We identify distinct geographical and temporal patterns of arbovirus disease incidence across Brazil, highlighting how climatic factors like temperature and precipitation influence the timing and intensity of dengue and chikungunya epidemics. The innovative Episcanner tool empowers researchers and public health officials to explore these patterns in detail, facilitating targeted interventions and risk assessments. This research offers a new perspective on the long-term dynamics of climate-driven mosquito-borne diseases and their geographical specificities linked to the effects of global temperature fluctuations such as those captured by the ENSO index.
△ Less
Submitted 30 July, 2024;
originally announced July 2024.
-
Local spin-flip transitions induced by magnetic quantum impurities in two-dimensional magnets
Authors:
Tim Bauer,
Lucas R. D. Freitas,
Eric C. Andrade,
Reinhold Egger,
Rodrigo G. Pereira
Abstract:
We predict a general local spin-flip transition mechanism caused by magnetic quantum impurities in (partially) polarized phases of quantum magnets in the absence of conservation laws. This transition arises when a magnon bound state crosses zero energy as function of the magnetic field. As application, we study 2D van der Waals magnets described by the Kitaev-Heisenberg honeycomb model which appli…
▽ More
We predict a general local spin-flip transition mechanism caused by magnetic quantum impurities in (partially) polarized phases of quantum magnets in the absence of conservation laws. This transition arises when a magnon bound state crosses zero energy as function of the magnetic field. As application, we study 2D van der Waals magnets described by the Kitaev-Heisenberg honeycomb model which applies to the transition metal trihalides CrI$_3$ and $α$-RuCl$_3$. We consider adatom and substitutional impurity positions, and show how spin-flip transitions can be detected in scanning tunneling spectroscopy.
△ Less
Submitted 2 August, 2024; v1 submitted 30 May, 2024;
originally announced May 2024.
-
Leveraging Visibility Graphs for Enhanced Arrhythmia Classification with Graph Convolutional Networks
Authors:
Rafael F. Oliveira,
Gladston J. P. Moreira,
Vander L. S. Freitas,
Eduardo J. S. Luz
Abstract:
Arrhythmias, detectable through electrocardiograms (ECGs), pose significant health risks, underscoring the need for accurate and efficient automated detection techniques. While recent advancements in graph-based methods have demonstrated potential to enhance arrhythmia classification, the challenge lies in effectively representing ECG signals as graphs. This study investigates the use of Visibilit…
▽ More
Arrhythmias, detectable through electrocardiograms (ECGs), pose significant health risks, underscoring the need for accurate and efficient automated detection techniques. While recent advancements in graph-based methods have demonstrated potential to enhance arrhythmia classification, the challenge lies in effectively representing ECG signals as graphs. This study investigates the use of Visibility Graph (VG) and Vector Visibility Graph (VVG) representations combined with Graph Convolutional Networks (GCNs) for arrhythmia classification under the ANSI/AAMI standard, ensuring reproducibility and fair comparison with other techniques. Through extensive experiments on the MIT-BIH dataset, we evaluate various GCN architectures and preprocessing parameters. Our findings demonstrate that VG and VVG mappings enable GCNs to classify arrhythmias directly from raw ECG signals, without the need for preprocessing or noise removal. Notably, VG offers superior computational efficiency, while VVG delivers enhanced classification performance by leveraging additional lead features. The proposed approach outperforms baseline methods in several metrics, although challenges persist in classifying the supraventricular ectopic beat (S) class, particularly under the inter-patient paradigm.
△ Less
Submitted 3 December, 2024; v1 submitted 19 April, 2024;
originally announced April 2024.
-
Text clustering applied to data augmentation in legal contexts
Authors:
Lucas José Gonçalves Freitas,
Thaís Rodrigues,
Guilherme Rodrigues,
Pamella Edokawa,
Ariane Farias
Abstract:
Data analysis and machine learning are of preeminent importance in the legal domain, especially in tasks like clustering and text classification. In this study, we harnessed the power of natural language processing tools to enhance datasets meticulously curated by experts. This process significantly improved the classification workflow for legal texts using machine learning techniques. We consider…
▽ More
Data analysis and machine learning are of preeminent importance in the legal domain, especially in tasks like clustering and text classification. In this study, we harnessed the power of natural language processing tools to enhance datasets meticulously curated by experts. This process significantly improved the classification workflow for legal texts using machine learning techniques. We considered the Sustainable Development Goals (SDGs) data from the United Nations 2030 Agenda as a practical case study. Data augmentation clustering-based strategy led to remarkable enhancements in the accuracy and sensitivity metrics of classification models. For certain SDGs within the 2030 Agenda, we observed performance gains of over 15%. In some cases, the example base expanded by a noteworthy factor of 5. When dealing with unclassified legal texts, data augmentation strategies centered around clustering prove to be highly effective. They provide a valuable means to expand the existing knowledge base without the need for labor-intensive manual classification efforts.
△ Less
Submitted 8 April, 2024;
originally announced April 2024.
-
Performance Assessment of Universal Machine Learning Interatomic Potentials: Challenges and Directions for Materials' Surfaces
Authors:
Bruno Focassio,
Luis Paulo Mezzina Freitas,
Gabriel R. Schleder
Abstract:
Machine learning interatomic potentials (MLIPs) are one of the main techniques in the materials science toolbox, able to bridge ab initio accuracy with the computational efficiency of classical force fields. This allows simulations ranging from atoms, molecules, and biosystems, to solid and bulk materials, surfaces, nanomaterials, and their interfaces and complex interactions. A recent class of ad…
▽ More
Machine learning interatomic potentials (MLIPs) are one of the main techniques in the materials science toolbox, able to bridge ab initio accuracy with the computational efficiency of classical force fields. This allows simulations ranging from atoms, molecules, and biosystems, to solid and bulk materials, surfaces, nanomaterials, and their interfaces and complex interactions. A recent class of advanced MLIPs, which use equivariant representations and deep graph neural networks, is known as universal models. These models are proposed as foundational models suitable for any system, covering most elements from the periodic table. Current universal MLIPs (UIPs) have been trained with the largest consistent dataset available nowadays. However, these are composed mostly of bulk materials' DFT calculations. In this article, we assess the universality of all openly available UIPs, namely MACE, CHGNet, and M3GNet, in a representative task of generalization: calculation of surface energies. We find that the out-of-the-box foundational models have significant shortcomings in this task, with errors correlated to the total energy of surface simulations, having an out-of-domain distance from the training dataset. Our results show that while UIPs are an efficient starting point for fine-tuning specialized models, we envision the potential of increasing the coverage of the materials space towards universal training datasets for MLIPs.
△ Less
Submitted 30 May, 2024; v1 submitted 6 March, 2024;
originally announced March 2024.
-
Generalization of Legendre functions applied to Rosen-Morse scattering states
Authors:
F. L. Freitas
Abstract:
A generalization of associated Legendre functions is proposed and used to describe the scattering states of the Rosen-Morse potential. The functions are then given explicit formulas in terms of the hypergeometric function, their asymptotic behavior is examined and shown to match the requirements for states in the regions of total and partial reflection. Elementary expressions are given for reflect…
▽ More
A generalization of associated Legendre functions is proposed and used to describe the scattering states of the Rosen-Morse potential. The functions are then given explicit formulas in terms of the hypergeometric function, their asymptotic behavior is examined and shown to match the requirements for states in the regions of total and partial reflection. Elementary expressions are given for reflection and transmission coefficients, and an integral identity for the generalized Legendre functions is proven, allowing the calculation of the spectral measure of the induced integral transform for the scattering states. These methods provide a complete classical solution to the potential, without need of path integral techniques.
△ Less
Submitted 29 December, 2023; v1 submitted 25 December, 2023;
originally announced December 2023.
-
Solution of the Basel problem using the Feynman integral trick
Authors:
F. L. Freitas
Abstract:
Euler's solution in 1734 of the Basel problem, which asks for a closed form expression for the sum of the reciprocals of all perfect squares, is one of the most celebrated results of mathematical analysis. In the modern era, numerous proofs of it have been produced, each emphasizing a different style of calculation, as a way of testing the power of some demonstration method. It's often thought tha…
▽ More
Euler's solution in 1734 of the Basel problem, which asks for a closed form expression for the sum of the reciprocals of all perfect squares, is one of the most celebrated results of mathematical analysis. In the modern era, numerous proofs of it have been produced, each emphasizing a different style of calculation, as a way of testing the power of some demonstration method. It's often thought that solutions using calculus need to involve advanced contour integration techniques or geometric coordinate transformations. We show that this is not the case, as the result can be derived by analyzing basic properties of a particular one-dimensional integral, and as such, can be obtained with techniques typical of regular calculus tests and math competitions.
△ Less
Submitted 10 December, 2023; v1 submitted 7 December, 2023;
originally announced December 2023.
-
Electric polarization near vortices in the extended Kitaev model
Authors:
Lucas R. D. Freitas,
Tim Bauer,
Reinhold Egger,
Rodrigo G. Pereira
Abstract:
We formulate a Majorana mean-field theory for the extended $JKΓ$ Kitaev model in a magnetic Zeeman field of arbitrary direction, and apply it for studying spatially inhomogeneous states harboring vortices. This mean-field theory is exact in the pure Kitaev limit and captures the essential physics throughout the Kitaev spin liquid phase. We determine the charge profile around vortices and the corre…
▽ More
We formulate a Majorana mean-field theory for the extended $JKΓ$ Kitaev model in a magnetic Zeeman field of arbitrary direction, and apply it for studying spatially inhomogeneous states harboring vortices. This mean-field theory is exact in the pure Kitaev limit and captures the essential physics throughout the Kitaev spin liquid phase. We determine the charge profile around vortices and the corresponding quadrupole tensor. The quadrupole-quadrupole interaction between distant vortices is shown to be either repulsive or attractive, depending on parameters. We predict that electrically biased scanning probe tips enable the creation of vortices at preselected positions. Our results open new perspectives for the electric manipulation of Ising anyons in Kitaev spin liquids.
△ Less
Submitted 5 February, 2024; v1 submitted 27 November, 2023;
originally announced November 2023.
-
International System of Quantities library in VDM
Authors:
Leo Freitas
Abstract:
The International Systems of Quantities (ISQ) standard was published in 1960 to tame the wide diversity of measurement systems being developed across the world, such as the centimetre-gram-second versus the meter-kilogram-second for example. Such a standard is highly motivated by the potential of ``trivial'' (rather error-prone) mistakes in converting between incompatible units. There have been su…
▽ More
The International Systems of Quantities (ISQ) standard was published in 1960 to tame the wide diversity of measurement systems being developed across the world, such as the centimetre-gram-second versus the meter-kilogram-second for example. Such a standard is highly motivated by the potential of ``trivial'' (rather error-prone) mistakes in converting between incompatible units. There have been such accidents in space missions, medical devices, etc. Thus, rendering modelling or simulation experiments unusable or unsafe. We address this problem by providing a \textbf{SAFE}-ISQ VDM-library that is: Simple, Accurate, Fast, and Effective. It extends an ecosystem of other VDM mathematical toolkit extensions, which include a translation and proof environment for VDM in Isabelle at https://github.com/leouk/VDM_Toolkit.
△ Less
Submitted 16 November, 2023;
originally announced November 2023.
-
A Bayesian framework for measuring association and its application to emotional dynamics in Web discourse
Authors:
Henrique S. Xavier,
Diogo Cortiz,
Mateus Silvestrin,
Ana Luísa Freitas,
Letícia Yumi Nakao Morello,
Fernanda Naomi Pantaleão,
Gabriel Gaudencio do Rêgo
Abstract:
This paper introduces a Bayesian framework designed to measure the degree of association between categorical random variables. The method is grounded in the formal definition of variable independence and is implemented using Markov Chain Monte Carlo (MCMC) techniques. Unlike commonly employed techniques in Association Rule Learning, this approach enables a clear and precise estimation of confidenc…
▽ More
This paper introduces a Bayesian framework designed to measure the degree of association between categorical random variables. The method is grounded in the formal definition of variable independence and is implemented using Markov Chain Monte Carlo (MCMC) techniques. Unlike commonly employed techniques in Association Rule Learning, this approach enables a clear and precise estimation of confidence intervals and the statistical significance of the measured degree of association. We applied the method to non-exclusive emotions identified by annotators in 4,613 tweets written in Portuguese. This analysis revealed pairs of emotions that exhibit associations and mutually opposed pairs. Moreover, the method identifies hierarchical relations between categories, a feature observed in our data, and is utilized to cluster emotions into basic-level groups.
△ Less
Submitted 11 March, 2024; v1 submitted 9 November, 2023;
originally announced November 2023.
-
SoK: Decentralized Sequencers for Rollups
Authors:
Shashank Motepalli,
Luciano Freitas,
Benjamin Livshits
Abstract:
Rollups have emerged as a promising solution to enhance blockchain scalability, offering increased throughput, reduced latency, and lower transaction fees. However, they currently rely on a centralized sequencer to determine transaction ordering, compromising the decentralization principle of blockchain systems. Recognizing this, there is a clear need for decentralized sequencers in rollups. Howev…
▽ More
Rollups have emerged as a promising solution to enhance blockchain scalability, offering increased throughput, reduced latency, and lower transaction fees. However, they currently rely on a centralized sequencer to determine transaction ordering, compromising the decentralization principle of blockchain systems. Recognizing this, there is a clear need for decentralized sequencers in rollups. However, designing such a system is intricate. This paper presents a comprehensive exploration of decentralized sequencers in rollups, formulating their ideal properties, dissecting their core components, and synthesizing community insights. Our findings emphasize the imperative for an adept sequencer design, harmonizing with the overarching goals of the blockchain ecosystem, and setting a trajectory for subsequent research endeavors.
△ Less
Submitted 5 October, 2023;
originally announced October 2023.
-
Swiper: a new paradigm for efficient weighted distributed protocols
Authors:
Andrei Tonkikh,
Luciano Freitas
Abstract:
The majority of fault-tolerant distributed algorithms are designed assuming a nominal corruption model, in which at most a fraction $f_n$ of parties can be corrupted by the adversary. However, due to the infamous Sybil attack, nominal models are not sufficient to express the trust assumptions in open (i.e., permissionless) settings. Instead, permissionless systems typically operate in a weighted m…
▽ More
The majority of fault-tolerant distributed algorithms are designed assuming a nominal corruption model, in which at most a fraction $f_n$ of parties can be corrupted by the adversary. However, due to the infamous Sybil attack, nominal models are not sufficient to express the trust assumptions in open (i.e., permissionless) settings. Instead, permissionless systems typically operate in a weighted model, where each participant is associated with a weight and the adversary can corrupt a set of parties holding at most a fraction $f_w$ of the total weight.
In this paper, we suggest a simple way to transform a large class of protocols designed for the nominal model into the weighted model. To this end, we formalize and solve three novel optimization problems, which we collectively call the weight reduction problems, that allow us to map large real weights into small integer weights while preserving the properties necessary for the correctness of the protocols. In all cases, we manage to keep the sum of the integer weights to be at most linear in the number of parties, resulting in extremely efficient protocols for the weighted model. Moreover, we demonstrate that, on weight distributions that emerge in practice, the sum of the integer weights tends to be far from the theoretical worst case and, sometimes, even smaller than the number of participants.
While, for some protocols, our transformation requires an arbitrarily small reduction in resilience (i.e., $f_w = f_n - ε$), surprisingly, for many important problems, we manage to obtain weighted solutions with the same resilience ($f_w = f_n$) as nominal ones. Notable examples include erasure-coded distributed storage and broadcast protocols, verifiable secret sharing, and asynchronous consensus.
△ Less
Submitted 4 November, 2024; v1 submitted 28 July, 2023;
originally announced July 2023.
-
Massive graviton from diffeomorphism invariance
Authors:
João M. L. de Freitas,
Iberê Kuntz
Abstract:
We describe a mechanism in which the graviton acquires a mass from the functional measure without violating the diffeomorphism symmetry nor including Stückelberg fields. Since gauge invariance is not violated, the number of degrees of freedom goes as in general relativity. For the same reason, Boulware-Deser ghosts and the vDVZ disconinuity do not show up. The graviton thus becomes massive at the…
▽ More
We describe a mechanism in which the graviton acquires a mass from the functional measure without violating the diffeomorphism symmetry nor including Stückelberg fields. Since gauge invariance is not violated, the number of degrees of freedom goes as in general relativity. For the same reason, Boulware-Deser ghosts and the vDVZ disconinuity do not show up. The graviton thus becomes massive at the quantum level while avoiding the usual issues of massive gravity.
△ Less
Submitted 22 January, 2024; v1 submitted 25 July, 2023;
originally announced July 2023.
-
Topologically sorting VDM-SL definitions for Isabelle/HOL translation
Authors:
Leo Freitas
Abstract:
There is an ecosystem of VDM libraries and extensions that includes a translation and proof environment for VDM in Isabelle. Translation works for a large subset of VDM-SL and further constructs are being added on demand. A key impediment for novice users is that Isabelle/HOL requires all definitions to be declared before they are used, where (mutually) recursive definitions must be defined in tan…
▽ More
There is an ecosystem of VDM libraries and extensions that includes a translation and proof environment for VDM in Isabelle. Translation works for a large subset of VDM-SL and further constructs are being added on demand. A key impediment for novice users is that Isabelle/HOL requires all definitions to be declared before they are used, where (mutually) recursive definitions must be defined in tandem. In this paper, we describe a solution to this problem, which will enable wider access to the translator plugin for novice users as well as real models.
△ Less
Submitted 1 April, 2023;
originally announced April 2023.
-
VDM recursive functions in Isabelle/HOL
Authors:
Leo Freitas,
Peter Gorm Larsen
Abstract:
For recursive functions general principles of induction needs to be applied. Instead of verifying them directly using the Vienna Development Method Specification Language (VDM-SL), we suggest a translation to Isabelle/HOL. In this paper, the challenges of such a translation for recursive functions are presented. This is an extension of an existing translation and a VDM mathematical toolbox in Isab…
▽ More
For recursive functions general principles of induction needs to be applied. Instead of verifying them directly using the Vienna Development Method Specification Language (VDM-SL), we suggest a translation to Isabelle/HOL. In this paper, the challenges of such a translation for recursive functions are presented. This is an extension of an existing translation and a VDM mathematical toolbox in Isabelle/HOL enabling support for recursive functions.
△ Less
Submitted 30 March, 2023;
originally announced March 2023.
-
Specification-based CSV Support in VDM
Authors:
Leo Freitas,
Aaron John Buhagiar
Abstract:
CSV is a widely used format for data representing systems control, information exchange and processing, logging, etc. Nevertheless, the format is riddled with tricky corner cases and inconsistencies, which can make input data unreliable, thus, rendering modelling or simulation experiments unusable or unsafe. We address this problem by providing a SAFE-CSV VDM-library that is: Simple, Accurate, Fas…
▽ More
CSV is a widely used format for data representing systems control, information exchange and processing, logging, etc. Nevertheless, the format is riddled with tricky corner cases and inconsistencies, which can make input data unreliable, thus, rendering modelling or simulation experiments unusable or unsafe. We address this problem by providing a SAFE-CSV VDM-library that is: Simple, Accurate, Fast, and Effective. It extends an ecosystem of other VDM mathematical toolkit extensions, which also includes a translation and proof environment for VDM in Isabelle
△ Less
Submitted 28 March, 2023;
originally announced March 2023.
-
Augmenting a Physics-Informed Neural Network for the 2D Burgers Equation by Addition of Solution Data Points
Authors:
Marlon Sproesser Mathias,
Wesley Pereira de Almeida,
Marcel Rodrigues de Barros,
Jefferson Fialho Coelho,
Lucas Palmiro de Freitas,
Felipe Marino Moreno,
Caio Fabricio Deberaldini Netto,
Fabio Gagliardi Cozman,
Anna Helena Reali Costa,
Eduardo Aoun Tannuri,
Edson Satoshi Gomi,
Marcelo Dottori
Abstract:
We implement a Physics-Informed Neural Network (PINN) for solving the two-dimensional Burgers equations. This type of model can be trained with no previous knowledge of the solution; instead, it relies on evaluating the governing equations of the system in points of the physical domain. It is also possible to use points with a known solution during training. In this paper, we compare PINNs trained…
▽ More
We implement a Physics-Informed Neural Network (PINN) for solving the two-dimensional Burgers equations. This type of model can be trained with no previous knowledge of the solution; instead, it relies on evaluating the governing equations of the system in points of the physical domain. It is also possible to use points with a known solution during training. In this paper, we compare PINNs trained with different amounts of governing equation evaluation points and known solution points. Comparing models that were trained purely with known solution points to those that have also used the governing equations, we observe an improvement in the overall observance of the underlying physics in the latter. We also investigate how changing the number of each type of point affects the resulting models differently. Finally, we argue that the addition of the governing equations during training may provide a way to improve the overall performance of the model without relying on additional data, which is especially important for situations where the number of known solution points is limited.
△ Less
Submitted 18 January, 2023;
originally announced January 2023.
-
Functional observability and subspace reconstruction in nonlinear systems
Authors:
Arthur N. Montanari,
Leandro Freitas,
Daniele Proverbio,
Jorge Gonçalves
Abstract:
Time-series analysis is fundamental for modeling and predicting dynamical behaviors from time-ordered data, with applications in many disciplines such as physics, biology, finance, and engineering. Measured time-series data, however, are often low dimensional or even univariate, thus requiring embedding methods to reconstruct the original system's state space. The observability of a system establi…
▽ More
Time-series analysis is fundamental for modeling and predicting dynamical behaviors from time-ordered data, with applications in many disciplines such as physics, biology, finance, and engineering. Measured time-series data, however, are often low dimensional or even univariate, thus requiring embedding methods to reconstruct the original system's state space. The observability of a system establishes fundamental conditions under which such reconstruction is possible. However, complete observability is too restrictive in applications where reconstructing the entire state space is not necessary and only a specific subspace is relevant. Here, we establish the theoretic condition to reconstruct a nonlinear functional of state variables from measurement processes, generalizing the concept of functional observability to nonlinear systems. When the functional observability condition holds, we show how to construct a map from the embedding space to the desired functional of state variables, characterizing the quality of such reconstruction. The theoretical results are then illustrated numerically using chaotic systems with contrasting observability properties. By exploring the presence of functionally unobservable regions in embedded attractors, we also apply our theory for the early warning of seizure-like events in simulated and empirical data. The studies demonstrate that the proposed functional observability condition can be assessed a priori to guide time-series analysis and experimental design for the dynamical characterization of complex systems.
△ Less
Submitted 10 January, 2023;
originally announced January 2023.
-
A Physics-Informed Neural Network to Model Port Channels
Authors:
Marlon S. Mathias,
Marcel R. de Barros,
Jefferson F. Coelho,
Lucas P. de Freitas,
Felipe M. Moreno,
Caio F. D. Netto,
Fabio G. Cozman,
Anna H. R. Costa,
Eduardo A. Tannuri,
Edson S. Gomi,
Marcelo Dottori
Abstract:
We describe a Physics-Informed Neural Network (PINN) that simulates the flow induced by the astronomical tide in a synthetic port channel, with dimensions based on the Santos - São Vicente - Bertioga Estuarine System. PINN models aim to combine the knowledge of physical systems and data-driven machine learning models. This is done by training a neural network to minimize the residuals of the gover…
▽ More
We describe a Physics-Informed Neural Network (PINN) that simulates the flow induced by the astronomical tide in a synthetic port channel, with dimensions based on the Santos - São Vicente - Bertioga Estuarine System. PINN models aim to combine the knowledge of physical systems and data-driven machine learning models. This is done by training a neural network to minimize the residuals of the governing equations in sample points. In this work, our flow is governed by the Navier-Stokes equations with some approximations. There are two main novelties in this paper. First, we design our model to assume that the flow is periodic in time, which is not feasible in conventional simulation methods. Second, we evaluate the benefit of resampling the function evaluation points during training, which has a near zero computational cost and has been verified to improve the final model, especially for small batch sizes. Finally, we discuss some limitations of the approximations used in the Navier-Stokes equations regarding the modeling of turbulence and how it interacts with PINNs.
△ Less
Submitted 20 December, 2022;
originally announced December 2022.
-
A Gravity-Consistent Confinement of Fermions in Braneworld
Authors:
L. F. F. Freitas,
I. C. Jardim,
G. Alencar,
R. R. Landim
Abstract:
In this manuscript, we discuss the confinement of the spin $\frac{1}{2}$ field on a plethora of branewords models. Recently, in (Eur.Phys.J.C 80 (2020) 5, 432), we studied the consistency of the Standard Model (SM) fields localization on braneworlds with the Einstein equation. In that paper, we discussed the consistency of the spinor field confinement and, by using a Yukawa-like interaction given…
▽ More
In this manuscript, we discuss the confinement of the spin $\frac{1}{2}$ field on a plethora of branewords models. Recently, in (Eur.Phys.J.C 80 (2020) 5, 432), we studied the consistency of the Standard Model (SM) fields localization on braneworlds with the Einstein equation. In that paper, we discussed the consistency of the spinor field confinement and, by using a Yukawa-like interaction given by $\mathcal{L}_{int}\propto f(y)\barΨΨ$, we obtained that the function must be defined as $f(y)\propto e^{-A}A'$. This shape of the scalar function emerge from the requirement that the spin $\frac{1}{2}$ (zero-mode) localization cannot modify the metric on bulk. This ensures that the confinement of gravity on the brane is preserved. In the present manuscript, we find a covariant scalar-coupling function that can generate this interaction. This provide a new mechanism for localizing fermion fields over the brane. We also discuss massive modes and we found some gravitational configuration where there are confined and discretized massive modes.
△ Less
Submitted 31 January, 2023; v1 submitted 5 December, 2022;
originally announced December 2022.
-
Scanning tunneling spectroscopy of Majorana zero modes in a Kitaev spin liquid
Authors:
Tim Bauer,
Lucas R. D. Freitas,
Rodrigo G. Pereira,
Reinhold Egger
Abstract:
We describe scanning tunneling spectroscopic signatures of Majorana zero modes (MZMs) in Kitaev spin liquids. The tunnel conductance is determined by the dynamical spin correlations of the spin liquid, which we compute exactly, and by spin-anisotropic cotunneling form factors. Near a $\mathbb{Z}_2$ vortex, the tunnel conductance has a staircase voltage dependence, where conductance steps arise fro…
▽ More
We describe scanning tunneling spectroscopic signatures of Majorana zero modes (MZMs) in Kitaev spin liquids. The tunnel conductance is determined by the dynamical spin correlations of the spin liquid, which we compute exactly, and by spin-anisotropic cotunneling form factors. Near a $\mathbb{Z}_2$ vortex, the tunnel conductance has a staircase voltage dependence, where conductance steps arise from MZMs and (at higher voltages) from additional vortex configurations. By scanning the probe tip position, one can detect the vortex locations. Our analysis suggests that topological magnon bound states near defects or magnetic impurities generate spectroscopic signatures that are qualitatively different from those of MZMs.
△ Less
Submitted 8 February, 2023; v1 submitted 26 September, 2022;
originally announced September 2022.
-
Enhancing Oceanic Variables Forecast in the Santos Channel by Estimating Model Error with Random Forests
Authors:
Felipe M. Moreno,
Caio F. D. Netto,
Marcel R. de Barros,
Jefferson F. Coelho,
Lucas P. de Freitas,
Marlon S. Mathias,
Luiz A. Schiaveto Neto,
Marcelo Dottori,
Fabio G. Cozman,
Anna H. R. Costa,
Edson S. Gomi,
Eduardo A. Tannuri
Abstract:
In this work we improve forecasting of Sea Surface Height (SSH) and current velocity (speed and direction) in oceanic scenarios. We do so by resorting to Random Forests so as to predict the error of a numerical forecasting system developed for the Santos Channel in Brazil. We have used the Santos Operational Forecasting System (SOFS) and data collected in situ between the years of 2019 and 2021. I…
▽ More
In this work we improve forecasting of Sea Surface Height (SSH) and current velocity (speed and direction) in oceanic scenarios. We do so by resorting to Random Forests so as to predict the error of a numerical forecasting system developed for the Santos Channel in Brazil. We have used the Santos Operational Forecasting System (SOFS) and data collected in situ between the years of 2019 and 2021. In previous studies we have applied similar methods for current velocity in the channel entrance, in this work we expand the application to improve the SHH forecast and include four other stations in the channel. We have obtained an average reduction of 11.9% in forecasting Root-Mean Square Error (RMSE) and 38.7% in bias with our approach. We also obtained an increase of Agreement (IOA) in 10 of the 14 combinations of forecasted variables and stations.
△ Less
Submitted 22 July, 2022;
originally announced August 2022.
-
Hypothesis tests for multiple responses regression models in R: The htmcglm Package
Authors:
Lineu Alberto Cavazani de Freitas,
Wagner Hugo Bonat
Abstract:
This article describes the R package htmcglm implemented for performing hypothesis tests on regression and dispersion parameters of multivariate covariance generalized linear models (McGLMs). McGLMs provide a general statistical modeling framework for normal and non-normal multivariate data analysis along with a wide range of correlation structures. The proposed package considers the Wald statisti…
▽ More
This article describes the R package htmcglm implemented for performing hypothesis tests on regression and dispersion parameters of multivariate covariance generalized linear models (McGLMs). McGLMs provide a general statistical modeling framework for normal and non-normal multivariate data analysis along with a wide range of correlation structures. The proposed package considers the Wald statistics to perform general hypothesis tests and build tailored ANOVAs, MANOVAs and multiple comparison tests. The goal of the package is to provide tools to improve the interpretation of regression and dispersion parameters. We assess the effects of the covariates on the response variables by testing the regression coefficients. Similarly, we perform tests on the dispersion coefficients in order to assess the correlation between study units. It could be of interest in situations where the data observations are correlated with each other, such as in longitudinal, times series, spatial and repeated measures studies. The htmcglm package provides a user friendly interface to perform MANOVA like tests as well as multivariate hypothesis tests for models of the mcglm class. We describe the package implementation and illustrate it through the analysis of two data sets. The first deals with an experiment on soybean yield; the problem has three response variables of different types (continuous, counting and binomial) and three explanatory variables (amount of water, fertilization and block). The second dataset addresses a problem where responses are longitudinal bivariate counts of hunting animals; the explanatory variables used are the hunting method and sex of the animal. With these examples we were able to illustrate several tests in which the proposal proves to be useful for the evaluation of regression and dispersion parameters both in problems with dependent or independent observations.
△ Less
Submitted 2 August, 2022;
originally announced August 2022.
-
Hypothesis tests for multiple responses regression: effect of probiotics on addiction and binge eating disorder
Authors:
Lineu Alberto Cavazani de Freitas,
Ligia de Oliveira Carlos,
Antônio Carlos Ligocki Campos,
Wagner Hugo Bonat
Abstract:
Clinical trials are common in medical research where multiple non-Gaussian responses and time-dependent observations are frequent. The analysis of data from these studies requires statistical modeling techniques that take these characteristics into account. We propose a general strategy based on the Wald statistics to perform hypothesis tests like ANOVAs, MANOVAs and multiple comparison tests on r…
▽ More
Clinical trials are common in medical research where multiple non-Gaussian responses and time-dependent observations are frequent. The analysis of data from these studies requires statistical modeling techniques that take these characteristics into account. We propose a general strategy based on the Wald statistics to perform hypothesis tests like ANOVAs, MANOVAs and multiple comparison tests on regression and dispersion parameters of multivariate covariance generalized linear models (McGLMs). McGLMs provide a general statistical modeling framework for normal and non-normal multivariate data analysis along with a wide range of correlation structures. We design different simulation scenarios to verify the properties of the proposed tests. The results are promising showing that the proposed tests present the levels of confidence close to the specified one for all simulation study scenarios. Complementary to the proposal, we developed implementations in the R language to carry out the tests presented, the codes are available in the supplementary material. The proposal is motivated by the analysis of a clinical trial that aims to evaluate the effect of the use of probiotics in the control of addiction and binge eating disorder in patients undergoing bariatric surgery. The subjects were separated into two groups (placebo and treatment) and evaluated at three different times. The results indicate that addiction and binge eating disorder reduce over time, but there is no difference between groups at each time point.
△ Less
Submitted 29 July, 2022;
originally announced August 2022.
-
Modeling Oceanic Variables with Dynamic Graph Neural Networks
Authors:
Caio F. D. Netto,
Marcel R. de Barros,
Jefferson F. Coelho,
Lucas P. de Freitas,
Felipe M. Moreno,
Marlon S. Mathias,
Marcelo Dottori,
Fábio G. Cozman,
Anna H. R. Costa,
Edson S. Gomi,
Eduardo A. Tannuri
Abstract:
Researchers typically resort to numerical methods to understand and predict ocean dynamics, a key task in mastering environmental phenomena. Such methods may not be suitable in scenarios where the topographic map is complex, knowledge about the underlying processes is incomplete, or the application is time critical. On the other hand, if ocean dynamics are observed, they can be exploited by recent…
▽ More
Researchers typically resort to numerical methods to understand and predict ocean dynamics, a key task in mastering environmental phenomena. Such methods may not be suitable in scenarios where the topographic map is complex, knowledge about the underlying processes is incomplete, or the application is time critical. On the other hand, if ocean dynamics are observed, they can be exploited by recent machine learning methods. In this paper we describe a data-driven method to predict environmental variables such as current velocity and sea surface height in the region of Santos-Sao Vicente-Bertioga Estuarine System in the southeastern coast of Brazil. Our model exploits both temporal and spatial inductive biases by joining state-of-the-art sequence models (LSTM and Transformers) and relational models (Graph Neural Networks) in an end-to-end framework that learns both the temporal features and the spatial relationship shared among observation sites. We compare our results with the Santos Operational Forecasting System (SOFS). Experiments show that better results are attained by our model, while maintaining flexibility and little domain knowledge dependency.
△ Less
Submitted 25 June, 2022;
originally announced June 2022.
-
Homomorphic Sortition -- Secret Leader Election for PoS Blockchains
Authors:
Luciano Freitas,
Andrei Tonkikh,
Adda-Akram Bendoukha,
Sara Tucci-Piergiovanni,
Renaud Sirdey,
Oana Stan,
Petr Kuznetsov
Abstract:
In a single secret leader election protocol (SSLE), one of the system participants is chosen and, unless it decides to reveal itself, no other participant can identify it. SSLE has a great potential in protecting blockchain consensus protocols against denial of service (DoS) attacks. However, all existing solutions either make strong synchrony assumptions or have expiring registration, meaning tha…
▽ More
In a single secret leader election protocol (SSLE), one of the system participants is chosen and, unless it decides to reveal itself, no other participant can identify it. SSLE has a great potential in protecting blockchain consensus protocols against denial of service (DoS) attacks. However, all existing solutions either make strong synchrony assumptions or have expiring registration, meaning that they require elected processes to re-register themselves before they can be re-elected again. This, in turn, prohibits the use of these SSLE protocols to elect leaders in partially-synchronous consensus protocols as there may be long periods of network instability when no new blocks are decided and, thus, no new registrations (or re-registrations) are possible. In this paper, we propose Homomorphic Sortition -- the first asynchronous SSLE protocol with non-expiring registration, making it the first solution compatible with partially-synchronous leader-based consensus protocols.
Homomorphic Sortition relies on Threshold Fully Homomorphic Encryption (ThFHE) and is tailored to proof-of-stake (PoS) blockchains, with several important optimizations with respect to prior proposals. In particular, unlike most existing SSLE protocols, it works with arbitrary stake distributions and does not require a user with multiple coins to be registered multiple times. Our protocol is highly parallelizable and can be run completely off-chain after setup.
Some blockchains require a sequence of rounds to have non-repeating leaders. We define a generalization of SSLE, called Secret Leader Permutation (SLP) in which the application can choose how many non-repeating leaders should be output in a sequence of rounds and we show how Homomorphic Sortition also solves this problem.
△ Less
Submitted 30 January, 2023; v1 submitted 23 June, 2022;
originally announced June 2022.
-
Distributed Randomness from Approximate Agreement
Authors:
Luciano Freitas,
Petr Kuznetsov,
Andrei Tonkikh
Abstract:
Randomisation is a critical tool in designing distributed systems. The common coin primitive, enabling the system members to agree on an unpredictable random number, has proven to be particularly useful. We observe, however, that it is impossible to implement a truly random common coin protocol in a fault-prone asynchronous system.
To circumvent this impossibility, we introduce two relaxations o…
▽ More
Randomisation is a critical tool in designing distributed systems. The common coin primitive, enabling the system members to agree on an unpredictable random number, has proven to be particularly useful. We observe, however, that it is impossible to implement a truly random common coin protocol in a fault-prone asynchronous system.
To circumvent this impossibility, we introduce two relaxations of the perfect common coin: (1) approximate common coin generating random numbers that are close to each other; and (2) Monte Carlo common coin generating a common random number with an arbitrarily small, but non-zero, probability of failure. Building atop the approximate agreement primitive, we obtain efficient asynchronous implementations of the two abstractions, tolerating up to one third of Byzantine processes. Our protocols do not assume trusted setup or public key infrastructure and converge to the perfect coin exponentially fast in the protocol running time.
By plugging one of our protocols for Monte Carlo common coin in a well-known consensus algorithm, we manage to get a binary Byzantine agreement protocol with $O(n^3 \log n)$ communication complexity, resilient against an adaptive adversary, and tolerating the optimal number $f<n/3$ of failures without trusted setup or PKI. To the best of our knowledge, the best communication complexity for binary Byzantine agreement achieved so far in this setting is $O(n^4)$. We also show how the approximate common coin, combined with a variant of Gray code, can be used to solve an interesting problem of Intersecting Random Subsets, which we introduce in this paper.
△ Less
Submitted 24 May, 2022;
originally announced May 2022.
-
Flood risk map from hydrological and mobility data: a case study in São Paulo (Brazil)
Authors:
Lívia Rodrigues Tomás,
Giovanni Guarnieri Soares,
Aurelienne A. S. Jorge,
Jeferson Feitosa Mendes,
Vander L. S. Freitas,
Leonardo B. L. Santos
Abstract:
Cities increasingly face flood risk primarily due to extensive changes of the natural land cover to built-up areas with impervious surfaces. In urban areas, flood impacts come mainly from road interruption. This paper proposes an urban flood risk map from hydrological and mobility data, considering the megacity of São Paulo, Brazil, as a case study. We estimate the flood susceptibility through the…
▽ More
Cities increasingly face flood risk primarily due to extensive changes of the natural land cover to built-up areas with impervious surfaces. In urban areas, flood impacts come mainly from road interruption. This paper proposes an urban flood risk map from hydrological and mobility data, considering the megacity of São Paulo, Brazil, as a case study. We estimate the flood susceptibility through the Height Above the Nearest Drainage algorithm; and the potential impact through the exposure and vulnerability components. We aggregate all variables into a regular grid and then classify the cells of each component into three classes: Moderate, High, and Very High. All components, except the flood susceptibility, have few cells in the Very High class. The flood susceptibility component reflects the presence of watercourses, and it has a strong influence on the location of those cells classified as Very High.
△ Less
Submitted 10 April, 2022;
originally announced April 2022.
-
$3$-anti-circulant digraphs are $α$-diperfect and BE-diperfect
Authors:
Lucas Ismaily Bezerra Freitas,
Orlando Lee
Abstract:
Let $D$ be a digraph. A subset $S$ of $V(D)$ is a stable set if every pair of vertices in $S$ is non-adjacent in $D$. A collection of disjoint paths $\mathcal{P}$ of $D$ is a path partition of $V(D)$, if every vertex in $V(D)$ is exactly on a path of $\mathcal{P}$. We say that a stable set $S$ and a path partition $\mathcal{P}$ are orthogonal if each path of $P$ contains exactly one vertex of $S$.…
▽ More
Let $D$ be a digraph. A subset $S$ of $V(D)$ is a stable set if every pair of vertices in $S$ is non-adjacent in $D$. A collection of disjoint paths $\mathcal{P}$ of $D$ is a path partition of $V(D)$, if every vertex in $V(D)$ is exactly on a path of $\mathcal{P}$. We say that a stable set $S$ and a path partition $\mathcal{P}$ are orthogonal if each path of $P$ contains exactly one vertex of $S$. A digraph $D$ satisfies the $α$-property if for every maximum stable set $S$ of $D$, there exists a path partition $\mathcal{P}$ such that $S$ and $\mathcal{P}$ are orthogonal. A digraph $D$ is $α$-diperfect if every induced subdigraph of $D$ satisfies the $α$-property. In 1982, Claude Berge proposed a characterization for $α$-diperfect digraphs in terms of forbidden anti-directed odd cycles. In 2018, Sambinelli, Silva and Lee proposed a similar conjecture. A digraph $D$ satisfies the Begin-End-property or BE-property if for every maximum stable set $S$ of $D$, there exists a path partition $\mathcal{P}$ such that (i) $S$ and $\mathcal{P}$ are orthogonal and (ii) for each path $P \in \mathcal{P}$, either the start or the end of $P$ belongs to $S$. A digraph $D$ is BE-diperfect if every induced subdigraph of $D$ satisfies the BE-property. Sambinelli, Silva and Lee proposed a characterization for BE-diperfect digraphs in terms of forbidden blocking odd cycles. In this paper, we verified both conjectures for $3$-anti-circulant digraphs. We also present some structural results for $α$-diperfect and BE-diperfect digraphs.
△ Less
Submitted 31 March, 2022; v1 submitted 9 March, 2022;
originally announced March 2022.
-
Global-threshold and backbone high-resolution weather radar networks are significantly complementary in a watershed
Authors:
Aurelienne A. S. Jorge,
Iuri da Silva Diniz,
Vander L. S. Freitas,
Izabelly C. Costa,
Leonardo B. L. Santos
Abstract:
There are several criteria for building up networks from time series related to different points in geographical space. The most used criterion is the Global-Threshold (GT). Using a weather radar dataset, this paper shows that the Backbone (BB) - a local-threshold criterion - generates networks whose geographical configuration is complementary to the GT networks. We compare the results for two wel…
▽ More
There are several criteria for building up networks from time series related to different points in geographical space. The most used criterion is the Global-Threshold (GT). Using a weather radar dataset, this paper shows that the Backbone (BB) - a local-threshold criterion - generates networks whose geographical configuration is complementary to the GT networks. We compare the results for two well-known similarities measures: the Pearson Correlation (PC) coefficient and the Mutual Information (MI). The extracted backbone network (miBB), whose number of links is the same as the global MI (miGT), has the lowest average shortest path and presents a small-world effect. Regarding the global PC (pcGT) and its corresponding BB network (pcBB), there is a significant linear relationship: $R2=0.77$ with a slope of $1.15$ (p-value $<E-7$) for the pcGT network, and $R2=0.68$ with a slope of $0.76$ (p-value $<E-7$) for the pcBB network. In relation to the MI ones, only the miGT present a high $R2$ ($0.79$, with slope = $1.95$), whereas the miBB has an $R2$ of only $0.20$ ($\text{slope} =0.24$). On the one hand, the GT networks present a sizeable connected component in the central area, close to the main rivers. On the other hand, the BB networks present a few meaningful connected components surrounding the watershed and dominating cells close to the outlet, with significant statistical differences in the altimetry distribution.
△ Less
Submitted 13 January, 2022;
originally announced January 2022.
-
Some results on Berge's conjecture and Begin-End conjecture
Authors:
Lucas Ismaily Bezerra Freitas,
Orlando Lee
Abstract:
Let $D$ be a digraph. A subset $S$ of $V(D)$ is a stable set if every pair of vertices in $S$ is non-adjacent in $D$. A collection of disjoint paths $\mathcal{P}$ of $D$ is a path partition of $V(D)$, if every vertex in $V(D)$ is on a path of $\mathcal{P}$. We say that a stable set $S$ and a path partition $\mathcal{P}$ are orthogonal if each path of $P$ contains exactly one vertex of $S$. A digra…
▽ More
Let $D$ be a digraph. A subset $S$ of $V(D)$ is a stable set if every pair of vertices in $S$ is non-adjacent in $D$. A collection of disjoint paths $\mathcal{P}$ of $D$ is a path partition of $V(D)$, if every vertex in $V(D)$ is on a path of $\mathcal{P}$. We say that a stable set $S$ and a path partition $\mathcal{P}$ are orthogonal if each path of $P$ contains exactly one vertex of $S$. A digraph $D$ satisfies the $α$-property if for every maximum stable set $S$ of $D$, there exists a path partition $\mathcal{P}$ such that $S$ and $\mathcal{P}$ are orthogonal. A digraph $D$ is $α$-diperfect if every induced subdigraph of $D$ satisfies the $α$-property. In 1982, Claude Berge proposed a characterization of $α$-diperfect digraphs in terms of forbidden anti-directed odd cycles. In 2018, Sambinelli, Silva and Lee proposed a similar conjecture. A digraph $D$ satisfies the Begin-End-property or BE-property if for every maximum stable set $S$ of $D$, there exists a path partition $\mathcal{P}$ such that (i) $S$ and $\mathcal{P}$ are orthogonal and (ii) for each path $P \in \mathcal{P}$, either the start or the end of $P$ lies in $S$. A digraph $D$ is BE-diperfect if every induced subdigraph of $D$ satisfies the BE-property. Sambinelli, Silva and Lee proposed a characterization of BE-diperfect digraphs in terms of forbidden blocking odd cycles. In this paper, we show some structural results for $α$-diperfect and BE-diperfect digraphs. In particular, we show that in every minimal counterexample $D$ to both conjectures, the size of a maximum stable set is smaller than $\vert V(D)\vert /2$. As an application we use these results to prove both conjectures for arc-locally in-semicomplete and arc-locally out-semicomplete digraphs.
△ Less
Submitted 23 November, 2021;
originally announced November 2021.
-
Discrete Bilal distribution with right-censored data
Authors:
Bruno Caparroz Lopes de Freitas,
Jorge Alberto Achcar,
Marcos Vinicius de Oliveira Peres,
Edson Zangiacomi Martinez
Abstract:
This paper presents inferences for the discrete Bilal (DB) distribution introduced by Altun et al. (2020). We consider parameter estimation for DB distribution in the presence of randomly right-censored data.We use maximum likelihood and Bayesian methods for the estimation of the model parameters. We also consider the inclusion of a cure fraction in the model. The usefulness of the proposed model…
▽ More
This paper presents inferences for the discrete Bilal (DB) distribution introduced by Altun et al. (2020). We consider parameter estimation for DB distribution in the presence of randomly right-censored data.We use maximum likelihood and Bayesian methods for the estimation of the model parameters. We also consider the inclusion of a cure fraction in the model. The usefulness of the proposed model was illustrated with three examples considering real datasets. These applications suggested that the model based on DB distribution performs at least as good as some other traditional discrete models as the DsFx-I, discrete Lindley, discrete Rayleigh, and discrete Burr- Hatke distributions. R codes are provided in an appendix at the end of the paper so that reader can carry out their own analysis.
△ Less
Submitted 2 November, 2021;
originally announced November 2021.
-
A Bayesian hierarchical model for disease mapping that accounts for scaling and heavy-tailed latent effects
Authors:
Victoire Michal,
Laís Picinini Freitas,
Alexandra M. Schmidt,
Oswaldo Gonçalves Cruz
Abstract:
In disease mapping, the relative risk of a disease is commonly estimated across different areas within a region of interest. The number of cases in an area is often assumed to follow a Poisson distribution whose mean is decomposed as the product between an offset and the logarithm of the disease's relative risk. The log risk may be written as the sum of fixed effects and latent random effects. The…
▽ More
In disease mapping, the relative risk of a disease is commonly estimated across different areas within a region of interest. The number of cases in an area is often assumed to follow a Poisson distribution whose mean is decomposed as the product between an offset and the logarithm of the disease's relative risk. The log risk may be written as the sum of fixed effects and latent random effects. The BYM2 model decomposes each latent effect into a weighted sum of independent and spatial effects. We build on the BYM2 model to allow for heavy-tailed latent effects and accommodate potentially outlying risks, after accounting for the fixed effects. We assume a scale mixture structure wherein the variance of the latent process changes across areas and allows for outlier identification. We propose two prior specifications for this scale mixture parameter. These are compared through simulation studies and in the analysis of Zika cases from the first (2015-2016) epidemic in Rio de Janeiro city, Brazil. The simulation studies show that, in terms of the model assessment criterion WAIC and outlier detection, the two proposed parametrisations perform better than the model proposed by Congdon (2017) to capture outliers. In particular, the proposed parametrisations are more efficient, in terms of outlier detection, than Congdon's when outliers are neighbours. Our analysis of Zika cases finds 19 out of 160 districts of Rio as potential outliers, after accounting for the socio-development index. Our proposed model may help prioritise interventions and identify potential issues in the recording of cases.
△ Less
Submitted 20 March, 2024; v1 submitted 21 September, 2021;
originally announced September 2021.
-
A Weakly Supervised Dataset of Fine-Grained Emotions in Portuguese
Authors:
Diogo Cortiz,
Jefferson O. Silva,
Newton Calegari,
Ana Luísa Freitas,
Ana Angélica Soares,
Carolina Botelho,
Gabriel Gaudencio Rêgo,
Waldir Sampaio,
Paulo Sergio Boggio
Abstract:
Affective Computing is the study of how computers can recognize, interpret and simulate human affects. Sentiment Analysis is a common task inNLP related to this topic, but it focuses only on emotion valence (positive, negative, neutral). An emerging approach in NLP is Emotion Recognition, which relies on fined-grained classification. This research describes an approach to create a lexical-based we…
▽ More
Affective Computing is the study of how computers can recognize, interpret and simulate human affects. Sentiment Analysis is a common task inNLP related to this topic, but it focuses only on emotion valence (positive, negative, neutral). An emerging approach in NLP is Emotion Recognition, which relies on fined-grained classification. This research describes an approach to create a lexical-based weakly supervised corpus for fine-grained emotion in Portuguese. We evaluated our dataset by fine-tuning a transformer-based language model (BERT) and validating it on a Gold Standard annotated validation set. Our results (F1-score=.64) suggest lexical-based weak supervision as an appropriate strategy for initial work in low resourced environment.
△ Less
Submitted 8 October, 2021; v1 submitted 17 August, 2021;
originally announced August 2021.
-
Gapless excitations in non-Abelian Kitaev spin liquids with line defects
Authors:
Lucas R. D. Freitas,
Rodrigo G. Pereira
Abstract:
We show that line defects in a non-Abelian Kitaev spin liquid harbor gapless one-dimensional Majorana modes if the interaction across the defect falls below a critical value. Treating the weak interaction at the line defect within a mean-field approximation, we determine the critical interaction strength as a function of the external magnetic field. In the gapless regime, we use the low-energy eff…
▽ More
We show that line defects in a non-Abelian Kitaev spin liquid harbor gapless one-dimensional Majorana modes if the interaction across the defect falls below a critical value. Treating the weak interaction at the line defect within a mean-field approximation, we determine the critical interaction strength as a function of the external magnetic field. In the gapless regime, we use the low-energy effective field theory to calculate the spin-lattice relaxation rate for a nuclear spin near the defect and find a cubic temperature dependence that agrees with experiments in the Kitaev material $α\text{-RuCl}_3$.
△ Less
Submitted 7 January, 2022; v1 submitted 9 August, 2021;
originally announced August 2021.
-
Some results on structure of all arc-locally (out) in-semicomplete digraphs
Authors:
Lucas I. B. Freitas,
Orlando Lee
Abstract:
Arc-locally semicomplete and arc-locally in-semicomplete digraphs were introduced by Bang-Jensen as a common generalization of both semicomplete and semicomplete bipartite digraphs in 1993. Later, Bang-Jensen (2004), Galeana-Sanchez and Goldfeder (2009) and Wang and Wang (2009) provided a characterization of strong arc-locally semicomplete digraphs. In 2009, Wang and Wang characterized strong arc-…
▽ More
Arc-locally semicomplete and arc-locally in-semicomplete digraphs were introduced by Bang-Jensen as a common generalization of both semicomplete and semicomplete bipartite digraphs in 1993. Later, Bang-Jensen (2004), Galeana-Sanchez and Goldfeder (2009) and Wang and Wang (2009) provided a characterization of strong arc-locally semicomplete digraphs. In 2009, Wang and Wang characterized strong arc-locally in-semicomplete digraphs. In 2012, Galeana-Sanchez and Goldfeder provided a characterization of all arc-locally semicomplete digraphs which generalizes some results by Bang-Jensen. In this paper, we characterize the structure of arbitrary connected arc-locally (out) in-semicomplete digraphs and arbitrary connected arc-locally semicomplete digraphs.
△ Less
Submitted 22 April, 2021;
originally announced April 2021.
-
Hit by the Data: a visual data analysis regarding the effects of traffic public policies
Authors:
Luana Müller,
Camila Moser,
Guilherme Paris,
Lucas Freitas,
Mayara Oliveira,
Wagner Signoretti,
Isabel Harb Manssour,
Milene Selbach Silveira
Abstract:
The availability of Open Government Data (OGD) provides means for citizens to understand and follow governmental policies and decisions, showing evidence of how the latter have contributed to both the place they live in and their lives. In such a scenario, one of the proposals is the use of visualizations to support the process of data analysis and interpretation. Herein, we present the use of thr…
▽ More
The availability of Open Government Data (OGD) provides means for citizens to understand and follow governmental policies and decisions, showing evidence of how the latter have contributed to both the place they live in and their lives. In such a scenario, one of the proposals is the use of visualizations to support the process of data analysis and interpretation. Herein, we present the use of three different visualization tools, a commercial one and two academic ones, applied to two specific Brazilian cases: the implementation of the Drink Driving Law and the construction of a new overpass in an important city avenue. Our focus was on the analysis of how visualization could help in the identification of the effects of such traffic public policies. As our main contributions, we present details on the effects of the observed policies, as well as new cases showing how visualization tools can assist users to interpret OGD.
△ Less
Submitted 12 February, 2021;
originally announced February 2021.
-
Vulnerability analysis in Complex Networks under a Flood Risk Reduction point of view
Authors:
Leonardo B. L. Santos,
Giovanni G. Soares,
Tanishq Garg,
Aurelienne A. S. Jorge,
Luciana R. Londe,
Regina T. Reani,
Roberta B. Bacelar,
Carlos E. S. Oliveira,
Vander L. S. Freitas,
Igor M. Sokolov
Abstract:
The measurement and mapping of transportation network vulnerability to natural hazards constitute subjects of global interest, especially due to climate change, and for a sustainable development agenda. During a flood, some elements of a transportation network can be affected, causing loss of life of people and damage to vehicles, streets/roads, and other logistics services, sometimes with severe…
▽ More
The measurement and mapping of transportation network vulnerability to natural hazards constitute subjects of global interest, especially due to climate change, and for a sustainable development agenda. During a flood, some elements of a transportation network can be affected, causing loss of life of people and damage to vehicles, streets/roads, and other logistics services, sometimes with severe economic impacts. The Network Science approach may offer a valuable perspective considering one type of vulnerability related to network type critical infrastructures: the topological vulnerability. The topological vulnerability index associated with an element is defined as the reduction in the network's average efficiency due to the removal of the set of edges related to that element. We present a topological vulnerability index analysis for the highways in the state of Santa Catarina, Brazil, and produce a map considering that index and the areas susceptible to urban floods and landslides. The risk knowledge, combining hazard and vulnerability, is the first pillar of an Early Warning System, and represent an important tool for stakeholders from the transportation sector in a disaster risk reduction agenda.
△ Less
Submitted 24 February, 2023; v1 submitted 21 December, 2020;
originally announced December 2020.
-
Including steady-state information in nonlinear models: an application to the development of soft-sensors
Authors:
Leandro Freitas,
Bruno H. G. Barbosa,
Luis A. Aguirre
Abstract:
When the dynamical data of a system only convey dynamic information over a limited operating range, the identification of models with good performance over a wider operating range is very unlikely. Nevertheless, models with such characteristic are desirable to implement modern control systems. To overcome such a shortcoming, this paper describes a methodology to train models from dynamical data an…
▽ More
When the dynamical data of a system only convey dynamic information over a limited operating range, the identification of models with good performance over a wider operating range is very unlikely. Nevertheless, models with such characteristic are desirable to implement modern control systems. To overcome such a shortcoming, this paper describes a methodology to train models from dynamical data and steady-state information, which is assumed available. The novelty is that the procedure can be applied to models with rather complex structures such as multilayer perceptron neural networks in a bi-objective fashion without the need to compute fixed points neither analytically nor numerically. As a consequence, the required computing time is greatly reduced. The capabilities of the proposed method are explored in numerical examples and the development of soft-sensors for downhole pressure estimation for a real deep-water offshore oil well. The results indicate that the procedure yields suitable soft-sensors with good dynamical and static performance and, in the case of models that are nonlinear in the parameters, the gain in computation time is about three orders of magnitude considering existing approaches.
△ Less
Submitted 3 September, 2020;
originally announced September 2020.
-
Consistency Conditions for $p$-Form Fields Localization on Codimension two Braneworlds
Authors:
L. F. F. Freitas,
G. Alencar,
R. R. Landim
Abstract:
Recently, in (Eur.Phys.J.C 80 (2020) 5, 432), the present authors obtained general stringent conditions on the localization of fields in braneworlds by imposing that its zero-mode must satisfy Einstein's equations (EE). Here, we continue this study by considering free $p$-form. These fields present an on-shell equivalency relation between a $p$-form and a $(D-p-2)$-form, provided by Hodge duality…
▽ More
Recently, in (Eur.Phys.J.C 80 (2020) 5, 432), the present authors obtained general stringent conditions on the localization of fields in braneworlds by imposing that its zero-mode must satisfy Einstein's equations (EE). Here, we continue this study by considering free $p$-form. These fields present an on-shell equivalency relation between a $p$-form and a $(D-p-2)$-form, provided by Hodge duality (HD). This symmetry will impose a new consistency condition, namely, confinement of a $p$-form must imply the localization of its dual. We apply the above conditions to $6$D braneworlds. With this, we find that in global string-like defects, for example, the $1$-form has a normalizable zero-mode. By using the HD, we show that its bulk dual $3$-form also has a normalizable zero-mode, making the confinement consistent with HD. However, these solutions cannot be made consistent with EE, therefore, these fields must be ruled out. In fact, by imposing both conditions, only the scalar and its dual field can be consistently localized. In this way, all the literature so far in which the free $1$-form is localized in codimension two models should be reviewed. These results also point to the fact that the symmetries of the fields can be used to verify the consistency of their localization and even prohibit it.
△ Less
Submitted 12 December, 2020; v1 submitted 18 June, 2020;
originally announced June 2020.