Showing 1–50 of 57 results for author: Ramos, M

A Computational Pipeline for Advanced Analysis of 4D Flow MRI in the Left Atrium

Authors: Xabier Morales, Ayah Elsayed, Debbie Zhao, Filip Loncaric, Ainhoa Aguado, Mireia Masias, Gina Quill, Marc Ramos, Ada Doltra, Ana Garcia, Marta Sitges, David Marlevi, Alistair Young, Martyn Nash, Bart Bijnens, Oscar Camara

Abstract: The left atrium (LA) plays a pivotal role in modulating left ventricular filling, but our comprehension of its hemodynamics is significantly limited by the constraints of conventional ultrasound analysis. 4D flow magnetic resonance imaging (4D Flow MRI) holds promise for enhancing our understanding of atrial hemodynamics. However, the low velocities within the LA and the limited spatial resolution… ▽ More The left atrium (LA) plays a pivotal role in modulating left ventricular filling, but our comprehension of its hemodynamics is significantly limited by the constraints of conventional ultrasound analysis. 4D flow magnetic resonance imaging (4D Flow MRI) holds promise for enhancing our understanding of atrial hemodynamics. However, the low velocities within the LA and the limited spatial resolution of 4D Flow MRI make analyzing this chamber challenging. Furthermore, the absence of dedicated computational frameworks, combined with diverse acquisition protocols and vendors, complicates gathering large cohorts for studying the prognostic value of hemodynamic parameters provided by 4D Flow MRI. In this study, we introduce the first open-source computational framework tailored for the analysis of 4D Flow MRI in the LA, enabling comprehensive qualitative and quantitative analysis of advanced hemodynamic parameters. Our framework proves robust to data from different centers of varying quality, producing high-accuracy automated segmentations (Dice $>$ 0.9 and Hausdorff 95 $<$ 3 mm), even with limited training data. Additionally, we conducted the first comprehensive assessment of energy, vorticity, and pressure parameters in the LA across a spectrum of disorders to investigate their potential as prognostic biomarkers. △ Less

Submitted 14 May, 2025; originally announced May 2025.

Multilingual Contextualization of Large Language Models for Document-Level Machine Translation

Authors: Miguel Moura Ramos, Patrick Fernandes, Sweta Agrawal, André F. T. Martins

Abstract: Large language models (LLMs) have demonstrated strong performance in sentence-level machine translation, but scaling to document-level translation remains challenging, particularly in modeling long-range dependencies and discourse phenomena across sentences and paragraphs. In this work, we propose a method to improve LLM-based long-document translation through targeted fine-tuning on high-quality… ▽ More Large language models (LLMs) have demonstrated strong performance in sentence-level machine translation, but scaling to document-level translation remains challenging, particularly in modeling long-range dependencies and discourse phenomena across sentences and paragraphs. In this work, we propose a method to improve LLM-based long-document translation through targeted fine-tuning on high-quality document-level data, which we curate and introduce as DocBlocks. Our approach supports multiple translation paradigms, including direct document-to-document and chunk-level translation, by integrating instructions both with and without surrounding context. This enables models to better capture cross-sentence dependencies while maintaining strong sentence-level translation performance. Experimental results show that incorporating multiple translation paradigms improves document-level translation quality and inference speed compared to prompting and agent-based methods. △ Less

Submitted 16 April, 2025; originally announced April 2025.

Comments: 9 pages, work-in-progress

Command A: An Enterprise-Ready Large Language Model

Authors: Team Cohere, :, Aakanksha, Arash Ahmadian, Marwan Ahmed, Jay Alammar, Milad Alizadeh, Yazeed Alnumay, Sophia Althammer, Arkady Arkhangorodsky, Viraat Aryabumi, Dennis Aumiller, Raphaël Avalos, Zahara Aviv, Sammie Bae, Saurabh Baji, Alexandre Barbet, Max Bartolo, Björn Bebensee, Neeral Beladia, Walter Beller-Morales, Alexandre Bérard, Andrew Berneshawi, Anna Bialas, Phil Blunsom , et al. (205 additional authors not shown)

Abstract: In this report we describe the development of Command A, a powerful large language model purpose-built to excel at real-world enterprise use cases. Command A is an agent-optimised and multilingual-capable model, with support for 23 languages of global business, and a novel hybrid architecture balancing efficiency with top of the range performance. It offers best-in-class Retrieval Augmented Genera… ▽ More In this report we describe the development of Command A, a powerful large language model purpose-built to excel at real-world enterprise use cases. Command A is an agent-optimised and multilingual-capable model, with support for 23 languages of global business, and a novel hybrid architecture balancing efficiency with top of the range performance. It offers best-in-class Retrieval Augmented Generation (RAG) capabilities with grounding and tool use to automate sophisticated business processes. These abilities are achieved through a decentralised training approach, including self-refinement algorithms and model merging techniques. We also include results for Command R7B which shares capability and architectural similarities to Command A. Weights for both models have been released for research purposes. This technical report details our original training pipeline and presents an extensive evaluation of our models across a suite of enterprise-relevant tasks and public benchmarks, demonstrating excellent performance and efficiency. △ Less

Submitted 14 April, 2025; v1 submitted 1 April, 2025; originally announced April 2025.

Comments: 55 pages

Fine-Grained Reward Optimization for Machine Translation using Error Severity Mappings

Authors: Miguel Moura Ramos, Tomás Almeida, Daniel Vareta, Filipe Azevedo, Sweta Agrawal, Patrick Fernandes, André F. T. Martins

Abstract: Reinforcement learning (RL) has been proven to be an effective and robust method for training neural machine translation systems, especially when paired with powerful reward models that accurately assess translation quality. However, most research has focused on RL methods that use sentence-level feedback, leading to inefficient learning signals due to the reward sparsity problem -- the model rece… ▽ More Reinforcement learning (RL) has been proven to be an effective and robust method for training neural machine translation systems, especially when paired with powerful reward models that accurately assess translation quality. However, most research has focused on RL methods that use sentence-level feedback, leading to inefficient learning signals due to the reward sparsity problem -- the model receives a single score for the entire sentence. To address this, we propose a novel approach that leverages fine-grained, token-level quality assessments along with error severity levels using RL methods. Specifically, we use xCOMET, a state-of-the-art quality estimation system, as our token-level reward model. We conduct experiments on small and large translation datasets with standard encoder-decoder and large language models-based machine translation systems, comparing the impact of sentence-level versus fine-grained reward signals on translation quality. Our results show that training with token-level rewards improves translation quality across language pairs over baselines according to both automatic and human evaluation. Furthermore, token-level reward optimization improves training stability, evidenced by a steady increase in mean rewards over training epochs. △ Less

Submitted 16 April, 2025; v1 submitted 8 November, 2024; originally announced November 2024.

Comments: 12 pages, work-in-progress

Learning and teaching biological data science in the Bioconductor community

Authors: Jenny Drnevich, Frederick J. Tan, Fabricio Almeida-Silva, Robert Castelo, Aedin C. Culhane, Sean Davis, Maria A. Doyle, Ludwig Geistlinger, Andrew R. Ghazi, Susan Holmes, Leo Lahti, Alexandru Mahmoud, Kozo Nishida, Marcel Ramos, Kevin Rue-Albrecht, David J. H. Shih, Laurent Gatto, Charlotte Soneson

Abstract: Modern biological research is increasingly data-intensive, leading to a growing demand for effective training in biological data science. In this article, we provide an overview of key resources and best practices available within the Bioconductor project - an open-source software community focused on omics data analysis. This guide serves as a valuable reference for both learners and educators in… ▽ More Modern biological research is increasingly data-intensive, leading to a growing demand for effective training in biological data science. In this article, we provide an overview of key resources and best practices available within the Bioconductor project - an open-source software community focused on omics data analysis. This guide serves as a valuable reference for both learners and educators in the field. △ Less

Submitted 11 March, 2025; v1 submitted 2 October, 2024; originally announced October 2024.

Comments: 16 pages, 2 figures, 1 table, 1 supplemental table; update after peer review; 16 pages, 1 figure, 1 table, 1 supplemental table

MSC Class: 97K80 ACM Class: K.3.2

Extending the Quantitative Pattern-Matching Paradigm

Authors: Sandra Alves, Delia Kesner, Miguel Ramos

Abstract: We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming languages, we use a (weak and closed) $λ$-calculus integrating a pattern matching mechanism on algebraic data types (ADTs). Remarkably, we also show that this langu… ▽ More We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming languages, we use a (weak and closed) $λ$-calculus integrating a pattern matching mechanism on algebraic data types (ADTs). Remarkably, we also show that this language not only encodes Plotkin's CBV and CBN $λ$-calculus as well as other subsuming frameworks, such as the bang-calculus, but can also be used to interpret the semantics of effectful languages with exceptions. After a thorough study of the untyped language, we introduce a type system based on intersection types, and we show through purely logical methods that the set of terminating terms of the language corresponds exactly to that of well-typed terms. Moreover, by considering non-idempotent intersection types, this characterization turns out to be quantitative, i.e. the size of the type derivation of a term t gives an upper bound for the number of evaluation steps from t to its normal form. △ Less

Submitted 20 August, 2024; originally announced August 2024.

Comments: APLAS 2024, full version (including complete proofs)

ACM Class: D.3.1; F.4.1

A Review of Large Language Models and Autonomous Agents in Chemistry

Authors: Mayk Caldas Ramos, Christopher J. Collison, Andrew D. White

Abstract: Large language models (LLMs) have emerged as powerful tools in chemistry, significantly impacting molecule design, property prediction, and synthesis optimization. This review highlights LLM capabilities in these domains and their potential to accelerate scientific discovery through automation. We also review LLM-based autonomous agents: LLMs with a broader set of tools to interact with their surr… ▽ More Large language models (LLMs) have emerged as powerful tools in chemistry, significantly impacting molecule design, property prediction, and synthesis optimization. This review highlights LLM capabilities in these domains and their potential to accelerate scientific discovery through automation. We also review LLM-based autonomous agents: LLMs with a broader set of tools to interact with their surrounding environment. These agents perform diverse tasks such as paper scraping, interfacing with automated laboratories, and synthesis planning. As agents are an emerging topic, we extend the scope of our review of agents beyond chemistry and discuss across any scientific domains. This review covers the recent history, current capabilities, and design of LLMs and autonomous agents, addressing specific challenges, opportunities, and future directions in chemistry. Key challenges include data quality and integration, model interpretability, and the need for standard benchmarks, while future directions point towards more sophisticated multi-modal agents and enhanced collaboration between agents and experimental methods. Due to the quick pace of this field, a repository has been built to keep track of the latest studies: https://github.com/ur-whitelab/LLMs-in-science. △ Less

Submitted 14 November, 2024; v1 submitted 26 June, 2024; originally announced July 2024.

Peregrine: ML-based Malicious Traffic Detection for Terabit Networks

Authors: João Romeiras Amado, Francisco Pereira, David Pissarra, Salvatore Signorello, Miguel Correia, Fernando M. V. Ramos

Abstract: Malicious traffic detectors leveraging machine learning (ML), namely those incorporating deep learning techniques, exhibit impressive detection capabilities across multiple attacks. However, their effectiveness becomes compromised when deployed in networks handling Terabit-speed traffic. In practice, these systems require substantial traffic sampling to reconcile the high data plane packet rates w… ▽ More Malicious traffic detectors leveraging machine learning (ML), namely those incorporating deep learning techniques, exhibit impressive detection capabilities across multiple attacks. However, their effectiveness becomes compromised when deployed in networks handling Terabit-speed traffic. In practice, these systems require substantial traffic sampling to reconcile the high data plane packet rates with the comparatively slower processing speeds of ML detection. As sampling significantly reduces traffic observability, it fundamentally undermines their detection capability. We present Peregrine, an ML-based malicious traffic detector for Terabit networks. The key idea is to run the detection process partially in the network data plane. Specifically, we offload the detector's ML feature computation to a commodity switch. The Peregrine switch processes a diversity of features per-packet, at Tbps line rates - three orders of magnitude higher than the fastest detector - to feed the ML-based component in the control plane. Our offloading approach presents a distinct advantage. While, in practice, current systems sample raw traffic, in Peregrine sampling occurs after feature computation. This essential trait enables computing features over all traffic, significantly enhancing detection performance. The Peregrine detector is not only effective for Terabit networks, but it is also energy- and cost-efficient. Further, by shifting a compute-heavy component to the switch, it saves precious CPU cycles and improves detection throughput. △ Less

Submitted 27 March, 2024; originally announced March 2024.

ClimateGPT: Towards AI Synthesizing Interdisciplinary Research on Climate Change

Authors: David Thulke, Yingbo Gao, Petrus Pelser, Rein Brune, Rricha Jalota, Floris Fok, Michael Ramos, Ian van Wyk, Abdallah Nasir, Hayden Goldstein, Taylor Tragemann, Katie Nguyen, Ariana Fowler, Andrew Stanco, Jon Gabriel, Jordan Taylor, Dean Moro, Evgenii Tsymbalov, Juliette de Waal, Evgeny Matusov, Mudar Yaghi, Mohammad Shihadah, Hermann Ney, Christian Dugast, Jonathan Dotan , et al. (1 additional authors not shown)

Abstract: This paper introduces ClimateGPT, a model family of domain-specific large language models that synthesize interdisciplinary research on climate change. We trained two 7B models from scratch on a science-oriented dataset of 300B tokens. For the first model, the 4.2B domain-specific tokens were included during pre-training and the second was adapted to the climate domain after pre-training. Addition… ▽ More This paper introduces ClimateGPT, a model family of domain-specific large language models that synthesize interdisciplinary research on climate change. We trained two 7B models from scratch on a science-oriented dataset of 300B tokens. For the first model, the 4.2B domain-specific tokens were included during pre-training and the second was adapted to the climate domain after pre-training. Additionally, ClimateGPT-7B, 13B and 70B are continuously pre-trained from Llama~2 on a domain-specific dataset of 4.2B tokens. Each model is instruction fine-tuned on a high-quality and human-generated domain-specific dataset that has been created in close cooperation with climate scientists. To reduce the number of hallucinations, we optimize the model for retrieval augmentation and propose a hierarchical retrieval strategy. To increase the accessibility of our model to non-English speakers, we propose to make use of cascaded machine translation and show that this approach can perform comparably to natively multilingual models while being easier to scale to a large number of languages. Further, to address the intrinsic interdisciplinary aspect of climate change we consider different research perspectives. Therefore, the model can produce in-depth answers focusing on different perspectives in addition to an overall answer. We propose a suite of automatic climate-specific benchmarks to evaluate LLMs. On these benchmarks, ClimateGPT-7B performs on par with the ten times larger Llama-2-70B Chat model while not degrading results on general domain benchmarks. Our human evaluation confirms the trends we saw in our benchmarks. All models were trained and evaluated using renewable energy and are released publicly. △ Less

Submitted 17 January, 2024; originally announced January 2024.

Biometric Technologies and the Law: Developing a Taxonomy for Guiding Policymakers

Authors: Luis Felipe M. Ramos

Abstract: Despite the increasing adoption of biometric technologies, their regulation has not kept up with the same pace, particularly with regard to safeguarding individuals' privacy and personal data. Policymakers may struggle to comprehend the technology behind biometric systems and their potential impact on fundamental rights, resulting in insufficient or inadequate legal regulation. This study seeks to… ▽ More Despite the increasing adoption of biometric technologies, their regulation has not kept up with the same pace, particularly with regard to safeguarding individuals' privacy and personal data. Policymakers may struggle to comprehend the technology behind biometric systems and their potential impact on fundamental rights, resulting in insufficient or inadequate legal regulation. This study seeks to bridge this gap by proposing a taxonomy of biometric technologies that can aid in their effective deployment and supervision. Through a literature review, the technical characteristics of biometric systems were identified and categorised. The resulting taxonomy can enhance the understanding of biometric technologies and facilitate the development of regulation that prioritises privacy and personal data protection. △ Less

Submitted 27 October, 2023; originally announced December 2023.

Comments: 11 pages, 1 figure, submitted to 57th Hawaii International Conference on System Sciences (HICSS-57)

ACM Class: J.1; J.4; K.4.1; K.5.2

Aligning Neural Machine Translation Models: Human Feedback in Training and Inference

Authors: Miguel Moura Ramos, Patrick Fernandes, António Farinhas, André F. T. Martins

Abstract: Reinforcement learning from human feedback (RLHF) is a recent technique to improve the quality of the text generated by a language model, making it closer to what humans would generate. A core ingredient in RLHF's success in aligning and improving large language models (LLMs) is its reward model, trained using human feedback on model outputs. In machine translation (MT), where metrics trained from… ▽ More Reinforcement learning from human feedback (RLHF) is a recent technique to improve the quality of the text generated by a language model, making it closer to what humans would generate. A core ingredient in RLHF's success in aligning and improving large language models (LLMs) is its reward model, trained using human feedback on model outputs. In machine translation (MT), where metrics trained from human annotations can readily be used as reward models, recent methods using minimum Bayes risk decoding and reranking have succeeded in improving the final quality of translation. In this study, we comprehensively explore and compare techniques for integrating quality metrics as reward models into the MT pipeline. This includes using the reward model for data filtering, during the training phase through RL, and at inference time by employing reranking techniques, and we assess the effects of combining these in a unified approach. Our experimental results, conducted across multiple translation tasks, underscore the crucial role of effective data filtering, based on estimated quality, in harnessing the full potential of RL in enhancing MT quality. Furthermore, our findings demonstrate the effectiveness of combining RL training with reranking techniques, showcasing substantial improvements in translation quality. △ Less

Submitted 4 July, 2024; v1 submitted 15 November, 2023; originally announced November 2023.

Comments: EAMT 2024

Automatic Parallelization of Software Network Functions

Authors: Francisco Pereira, Fernando M. V. Ramos, Luis Pedrosa

Abstract: Software network functions (NFs) trade-off flexibility and ease of deployment for an increased challenge of performance. The traditional way to increase NF performance is by distributing traffic to multiple CPU cores, but this poses a significant challenge: how to parallelize an NF without breaking its semantics? We propose Maestro, a tool that analyzes a sequential implementation of an NF and aut… ▽ More Software network functions (NFs) trade-off flexibility and ease of deployment for an increased challenge of performance. The traditional way to increase NF performance is by distributing traffic to multiple CPU cores, but this poses a significant challenge: how to parallelize an NF without breaking its semantics? We propose Maestro, a tool that analyzes a sequential implementation of an NF and automatically generates an enhanced parallel version that carefully configures the NIC's Receive Side Scaling mechanism to distribute traffic across cores, while preserving semantics. When possible, Maestro orchestrates a shared-nothing architecture, with each core operating independently without shared memory coordination, maximizing performance. Otherwise, Maestro choreographs a fine-grained read-write locking mechanism that optimizes operation for typical Internet traffic. We parallelized 8 software NFs and show that they generally scale-up linearly until bottlenecked by PCIe when using small packets or by 100Gbps line-rate with typical Internet traffic. Maestro further outperforms modern hardware-based transactional memory mechanisms, even for challenging parallel-unfriendly workloads. △ Less

Submitted 13 October, 2023; v1 submitted 27 July, 2023; originally announced July 2023.

Comments: 21 pages, 14 figures, to be published in NSDI24

Predicting small molecules solubilities on endpoint devices using deep ensemble neural networks

Authors: Mayk Caldas Ramos, Andrew D. White

Abstract: Aqueous solubility is a valuable yet challenging property to predict. Computing solubility using first-principles methods requires accounting for the competing effects of entropy and enthalpy, resulting in long computations for relatively poor accuracy. Data-driven approaches, such as deep learning, offer improved accuracy and computational efficiency but typically lack uncertainty quantification.… ▽ More Aqueous solubility is a valuable yet challenging property to predict. Computing solubility using first-principles methods requires accounting for the competing effects of entropy and enthalpy, resulting in long computations for relatively poor accuracy. Data-driven approaches, such as deep learning, offer improved accuracy and computational efficiency but typically lack uncertainty quantification. Additionally, ease of use remains a concern for any computational technique, resulting in the sustained popularity of group-based contribution methods. In this work, we addressed these problems with a deep learning model with predictive uncertainty that runs on a static website (without a server). This approach moves computing needs onto the website visitor without requiring installation, removing the need to pay for and maintain servers. Our model achieves satisfactory results in solubility prediction. Furthermore, we demonstrate how to create molecular property prediction models that balance uncertainty and ease of use. The code is available at https://github.com/ur-whitelab/mol.dev, and the model is usable at https://mol.dev. △ Less

Submitted 7 March, 2024; v1 submitted 11 July, 2023; originally announced July 2023.

The Segment Anything Model (SAM) for Remote Sensing Applications: From Zero to One Shot

Authors: Lucas Prado Osco, Qiusheng Wu, Eduardo Lopes de Lemos, Wesley Nunes Gonçalves, Ana Paula Marques Ramos, Jonathan Li, José Marcato Junior

Abstract: Segmentation is an essential step for remote sensing image processing. This study aims to advance the application of the Segment Anything Model (SAM), an innovative image segmentation model by Meta AI, in the field of remote sensing image analysis. SAM is known for its exceptional generalization capabilities and zero-shot learning, making it a promising approach to processing aerial and orbital im… ▽ More Segmentation is an essential step for remote sensing image processing. This study aims to advance the application of the Segment Anything Model (SAM), an innovative image segmentation model by Meta AI, in the field of remote sensing image analysis. SAM is known for its exceptional generalization capabilities and zero-shot learning, making it a promising approach to processing aerial and orbital images from diverse geographical contexts. Our exploration involved testing SAM across multi-scale datasets using various input prompts, such as bounding boxes, individual points, and text descriptors. To enhance the model's performance, we implemented a novel automated technique that combines a text-prompt-derived general example with one-shot training. This adjustment resulted in an improvement in accuracy, underscoring SAM's potential for deployment in remote sensing imagery and reducing the need for manual annotation. Despite the limitations encountered with lower spatial resolution images, SAM exhibits promising adaptability to remote sensing data analysis. We recommend future research to enhance the model's proficiency through integration with supplementary fine-tuning techniques and other networks. Furthermore, we provide the open-source code of our modifications on online repositories, encouraging further and broader adaptations of SAM to the remote sensing domain. △ Less

Submitted 31 October, 2023; v1 submitted 28 June, 2023; originally announced June 2023.

Comments: 20 pages, 9 figures

14 Examples of How LLMs Can Transform Materials Science and Chemistry: A Reflection on a Large Language Model Hackathon

Authors: Kevin Maik Jablonka, Qianxiang Ai, Alexander Al-Feghali, Shruti Badhwar, Joshua D. Bocarsly, Andres M Bran, Stefan Bringuier, L. Catherine Brinson, Kamal Choudhary, Defne Circi, Sam Cox, Wibe A. de Jong, Matthew L. Evans, Nicolas Gastellu, Jerome Genzling, María Victoria Gil, Ankur K. Gupta, Zhi Hong, Alishba Imran, Sabine Kruschwitz, Anne Labarre, Jakub Lála, Tao Liu, Steven Ma, Sauradeep Majumdar , et al. (28 additional authors not shown)

Abstract: Large-language models (LLMs) such as GPT-4 caught the interest of many scientists. Recent studies suggested that these models could be useful in chemistry and materials science. To explore these possibilities, we organized a hackathon. This article chronicles the projects built as part of this hackathon. Participants employed LLMs for various applications, including predicting properties of mole… ▽ More Large-language models (LLMs) such as GPT-4 caught the interest of many scientists. Recent studies suggested that these models could be useful in chemistry and materials science. To explore these possibilities, we organized a hackathon. This article chronicles the projects built as part of this hackathon. Participants employed LLMs for various applications, including predicting properties of molecules and materials, designing novel interfaces for tools, extracting knowledge from unstructured data, and developing new educational applications. The diverse topics and the fact that working prototypes could be generated in less than two days highlight that LLMs will profoundly impact the future of our fields. The rich collection of ideas and projects also indicates that the applications of LLMs are not limited to materials science and chemistry but offer potential benefits to a wide range of scientific disciplines. △ Less

Submitted 14 July, 2023; v1 submitted 9 June, 2023; originally announced June 2023.

The Potential of Visual ChatGPT For Remote Sensing

Authors: Lucas Prado Osco, Eduardo Lopes de Lemos, Wesley Nunes Gonçalves, Ana Paula Marques Ramos, José Marcato Junior

Abstract: Recent advancements in Natural Language Processing (NLP), particularly in Large Language Models (LLMs), associated with deep learning-based computer vision techniques, have shown substantial potential for automating a variety of tasks. One notable model is Visual ChatGPT, which combines ChatGPT's LLM capabilities with visual computation to enable effective image analysis. The model's ability to pr… ▽ More Recent advancements in Natural Language Processing (NLP), particularly in Large Language Models (LLMs), associated with deep learning-based computer vision techniques, have shown substantial potential for automating a variety of tasks. One notable model is Visual ChatGPT, which combines ChatGPT's LLM capabilities with visual computation to enable effective image analysis. The model's ability to process images based on textual inputs can revolutionize diverse fields. However, its application in the remote sensing domain remains unexplored. This is the first paper to examine the potential of Visual ChatGPT, a cutting-edge LLM founded on the GPT architecture, to tackle the aspects of image processing related to the remote sensing domain. Among its current capabilities, Visual ChatGPT can generate textual descriptions of images, perform canny edge and straight line detection, and conduct image segmentation. These offer valuable insights into image content and facilitate the interpretation and extraction of information. By exploring the applicability of these techniques within publicly available datasets of satellite images, we demonstrate the current model's limitations in dealing with remote sensing images, highlighting its challenges and future prospects. Although still in early development, we believe that the combination of LLMs and visual models holds a significant potential to transform remote sensing image processing, creating accessible and practical application opportunities in the field. △ Less

Submitted 5 July, 2023; v1 submitted 25 April, 2023; originally announced April 2023.

Bayesian Optimization of Catalysis With In-Context Learning

Authors: Mayk Caldas Ramos, Shane S. Michtavy, Marc D. Porosoff, Andrew D. White

Abstract: Large language models (LLMs) can perform accurate classification with zero or few examples through in-context learning. We extend this capability to regression with uncertainty estimation using frozen LLMs (e.g., GPT-3.5, Gemini), enabling Bayesian optimization (BO) in natural language without explicit model training or feature engineering. We apply this to materials discovery by representing expe… ▽ More Large language models (LLMs) can perform accurate classification with zero or few examples through in-context learning. We extend this capability to regression with uncertainty estimation using frozen LLMs (e.g., GPT-3.5, Gemini), enabling Bayesian optimization (BO) in natural language without explicit model training or feature engineering. We apply this to materials discovery by representing experimental catalyst synthesis and testing procedures as natural language prompts. A key challenge in materials discovery is the need to characterize suboptimal candidates, which slows progress. While BO is effective for navigating large design spaces, standard surrogate models like Gaussian processes assume smoothness and continuity, an assumption that fails in highly non-linear domains such as heterogeneous catalysis. Our task-agnostic BO workflow overcomes this by operating directly in language space, producing interpretable and actionable predictions without requiring structural or electronic descriptors. On benchmarks like aqueous solubility and oxidative coupling of methane (OCM), BO-ICL matches or outperforms Gaussian processes. In live experiments on the reverse water-gas shift (RWGS) reaction, BO-ICL identifies near-optimal multi-metallic catalysts within six iterations from a pool of 3,700 candidates. Our method redefines materials representation and accelerates discovery, with broad applications across catalysis, materials science, and AI. Code: https://github.com/ur-whitelab/BO-ICL. △ Less

Submitted 14 May, 2025; v1 submitted 11 April, 2023; originally announced April 2023.

Quantitative Global Memory

Authors: Sandra Alves, Delia Kesner, Miguel Ramos

Abstract: We show that recent approaches of static analysis based on quantitative typing systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs.… ▽ More We show that recent approaches of static analysis based on quantitative typing systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs. We show that the type system is quantitatively sound and complete with respect to the original operational semantics of the language. △ Less

Submitted 16 June, 2023; v1 submitted 15 March, 2023; originally announced March 2023.

Comments: WoLLIC 2023, full version (including proofs)

ACM Class: D.3.1; F.4.1

The smooth output assumption, and why deep networks are better than wide ones

Authors: Luis Sa-Couto, Jose Miguel Ramos, Andreas Wichert

Abstract: When several models have similar training scores, classical model selection heuristics follow Occam's razor and advise choosing the ones with least capacity. Yet, modern practice with large neural networks has often led to situations where two networks with exactly the same number of parameters score similar on the training set, but the deeper one generalizes better to unseen examples. With this i… ▽ More When several models have similar training scores, classical model selection heuristics follow Occam's razor and advise choosing the ones with least capacity. Yet, modern practice with large neural networks has often led to situations where two networks with exactly the same number of parameters score similar on the training set, but the deeper one generalizes better to unseen examples. With this in mind, it is well accepted that deep networks are superior to shallow wide ones. However, theoretically there is no difference between the two. In fact, they are both universal approximators. In this work we propose a new unsupervised measure that predicts how well a model will generalize. We call it the output sharpness, and it is based on the fact that, in reality, boundaries between concepts are generally unsharp. We test this new measure on several neural network settings, and architectures, and show how generally strong the correlation is between our metric, and test set performance. Having established this measure, we give a mathematical probabilistic argument that predicts network depth to be correlated with our proposed measure. After verifying this in real data, we are able to formulate the key argument of the work: output sharpness hampers generalization; deep networks have an in built bias against it; therefore, deep networks beat wide ones. All in all the work not only provides a helpful predictor of overfitting that can be used in practice for model selection (or even regularization), but also provides a much needed theoretical grounding for the success of modern deep neural networks. △ Less

Submitted 25 November, 2022; originally announced November 2022.

Understanding the double descent curve in Machine Learning

Authors: Luis Sa-Couto, Jose Miguel Ramos, Miguel Almeida, Andreas Wichert

Abstract: The theory of bias-variance used to serve as a guide for model selection when applying Machine Learning algorithms. However, modern practice has shown success with over-parameterized models that were expected to overfit but did not. This led to the proposal of the double descent curve of performance by Belkin et al. Although it seems to describe a real, representative phenomenon, the field is lack… ▽ More The theory of bias-variance used to serve as a guide for model selection when applying Machine Learning algorithms. However, modern practice has shown success with over-parameterized models that were expected to overfit but did not. This led to the proposal of the double descent curve of performance by Belkin et al. Although it seems to describe a real, representative phenomenon, the field is lacking a fundamental theoretical understanding of what is happening, what are the consequences for model selection and when is double descent expected to occur. In this paper we develop a principled understanding of the phenomenon, and sketch answers to these important questions. Furthermore, we report real experimental results that are correctly predicted by our proposed hypothesis. △ Less

Submitted 18 November, 2022; originally announced November 2022.

Multi-level Data Representation For Training Deep Helmholtz Machines

Authors: Jose Miguel Ramos, Luis Sa-Couto, Andreas Wichert

Abstract: A vast majority of the current research in the field of Machine Learning is done using algorithms with strong arguments pointing to their biological implausibility such as Backpropagation, deviating the field's focus from understanding its original organic inspiration to a compulsive search for optimal performance. Yet, there have been a few proposed models that respect most of the biological cons… ▽ More A vast majority of the current research in the field of Machine Learning is done using algorithms with strong arguments pointing to their biological implausibility such as Backpropagation, deviating the field's focus from understanding its original organic inspiration to a compulsive search for optimal performance. Yet, there have been a few proposed models that respect most of the biological constraints present in the human brain and are valid candidates for mimicking some of its properties and mechanisms. In this paper, we will focus on guiding the learning of a biologically plausible generative model called the Helmholtz Machine in complex search spaces using a heuristic based on the Human Image Perception mechanism. We hypothesize that this model's learning algorithm is not fit for Deep Networks due to its Hebbian-like local update rule, rendering it incapable of taking full advantage of the compositional properties that multi-layer networks provide. We propose to overcome this problem, by providing the network's hidden layers with visual queues at different resolutions using a Multi-level Data representation. The results on several image datasets showed the model was able to not only obtain better overall quality but also a wider diversity in the generated images, corroborating our intuition that using our proposed heuristic allows the model to take more advantage of the network's depth growth. More importantly, they show the unexplored possibilities underlying brain-inspired models and techniques. △ Less

Submitted 26 October, 2022; originally announced October 2022.

Deep Semi-Supervised and Self-Supervised Learning for Diabetic Retinopathy Detection

Authors: Jose Miguel Arrieta Ramos, Oscar Perdómo, Fabio A. González

Abstract: Diabetic retinopathy (DR) is one of the leading causes of blindness in the working-age population of developed countries, caused by a side effect of diabetes that reduces the blood supply to the retina. Deep neural networks have been widely used in automated systems for DR classification on eye fundus images. However, these models need a large number of annotated images. In the medical domain, ann… ▽ More Diabetic retinopathy (DR) is one of the leading causes of blindness in the working-age population of developed countries, caused by a side effect of diabetes that reduces the blood supply to the retina. Deep neural networks have been widely used in automated systems for DR classification on eye fundus images. However, these models need a large number of annotated images. In the medical domain, annotations from experts are costly, tedious, and time-consuming; as a result, a limited number of annotated images are available. This paper presents a semi-supervised method that leverages unlabeled images and labeled ones to train a model that detects diabetic retinopathy. The proposed method uses unsupervised pretraining via self-supervised learning followed by supervised fine-tuning with a small set of labeled images and knowledge distillation to increase the performance in classification task. This method was evaluated on the EyePACS test and Messidor-2 dataset achieving 0.94 and 0.89 AUC respectively using only 2% of EyePACS train labeled images. △ Less

Submitted 3 August, 2022; originally announced August 2022.

A Novel Capsule Neural Network Based Model for Drowsiness Detection Using Electroencephalography Signals

Authors: Luis Guarda, Juan Tapia, Enrique Lopez Droguett, Marcelo Ramos

Abstract: The early detection of drowsiness has become vital to ensure the correct and safe development of several industries' tasks. Due to the transient mental state of a human subject between alertness and drowsiness, automated drowsiness detection is a complex problem to tackle. The electroencephalography signals allow us to record variations in an individual's brain's electrical potential, where each o… ▽ More The early detection of drowsiness has become vital to ensure the correct and safe development of several industries' tasks. Due to the transient mental state of a human subject between alertness and drowsiness, automated drowsiness detection is a complex problem to tackle. The electroencephalography signals allow us to record variations in an individual's brain's electrical potential, where each of them gives specific information about a subject's mental state. However, due to this type of signal's nature, its acquisition, in general, is complex, so it is hard to have a large volume of data to apply techniques of Deep Learning for processing and classification optimally. Nevertheless, Capsule Neural Networks are a brand-new Deep Learning algorithm proposed for work with reduced amounts of data. It is a robust algorithm to handle the data's hierarchical relationships, which is an essential characteristic for work with biomedical signals. Therefore, this paper presents a Deep Learning-based method for drowsiness detection with CapsNet by using a concatenation of spectrogram images of the electroencephalography signals channels. The proposed CapsNet model is compared with a Convolutional Neural Network, which is outperformed by the proposed model, which obtains an average accuracy of 86,44% and 87,57% of sensitivity against an average accuracy of 75,86% and 79,47% sensitivity for the CNN, showing that CapsNet is more suitable for this kind of datasets and tasks. △ Less

Submitted 4 April, 2022; originally announced April 2022.

EVL: a typed functional language for event processing

Authors: Sandra Alves, Maribel Fernández, Miguel Ramos

Abstract: We define EVL, a minimal higher-order functional language to deal with generic events. The notion of generic event extends the well-known notion of event traditionally used in a variety of areas, such as database management, concurrency, reactive systems and cybersecurity. Generic events were introduced in the context of a metamodel to specify obligations in access control systems. Event specifica… ▽ More We define EVL, a minimal higher-order functional language to deal with generic events. The notion of generic event extends the well-known notion of event traditionally used in a variety of areas, such as database management, concurrency, reactive systems and cybersecurity. Generic events were introduced in the context of a metamodel to specify obligations in access control systems. Event specifications are represented as records and we use polymorphic record types to type events in EVL. We show how the higher-order capabilities of EVL can be used in the context of Complex Event Processing (CEP), to define higher-order parameterised functions that deal with the usual CEP techniques. △ Less

Submitted 28 October, 2021; v1 submitted 18 September, 2021; originally announced September 2021.

Comments: Submitted to MSCS

ACM Class: F.3.1; D.3.1

An ML-style Record Calculus with Extensible Records

Authors: Sandra Alves, Miguel Ramos

Abstract: In this work, we develop a polymorphic record calculus with extensible records. Extensible records are records that can have new fields added to them, or preexisting fields removed from them. We also develop a static type system for this calculus and a sound and complete type inference algorithm. Most ML-style polymorphic record calculi that support extensible records are based on row variables. W… ▽ More In this work, we develop a polymorphic record calculus with extensible records. Extensible records are records that can have new fields added to them, or preexisting fields removed from them. We also develop a static type system for this calculus and a sound and complete type inference algorithm. Most ML-style polymorphic record calculi that support extensible records are based on row variables. We present an alternative construction based on the polymorphic record calculus developed by Ohori. Ohori based his polymorphic record calculus on the idea of kind restrictions. This allowed him to express polymorphic operations on records such as field selection and modification. With the addition of extensible types, we were able to extend Ohori's original calculus with other powerful operations on records such as field addition and removal. △ Less

Submitted 28 December, 2021; v1 submitted 13 August, 2021; originally announced August 2021.

Comments: In Proceedings MFPS 2021, arXiv:2112.13746

Report number: EPTCS 351-1

Journal ref: EPTCS 351, 2021, pp. 1-17

Counting and Locating High-Density Objects Using Convolutional Neural Network

Authors: Mauro dos Santos de Arruda, Lucas Prado Osco, Plabiany Rodrigo Acosta, Diogo Nunes Gonçalves, José Marcato Junior, Ana Paula Marques Ramos, Edson Takashi Matsubara, Zhipeng Luo, Jonathan Li, Jonathan de Andrade Silva, Wesley Nunes Gonçalves

Abstract: This paper presents a Convolutional Neural Network (CNN) approach for counting and locating objects in high-density imagery. To the best of our knowledge, this is the first object counting and locating method based on a feature map enhancement and a Multi-Stage Refinement of the confidence map. The proposed method was evaluated in two counting datasets: tree and car. For the tree dataset, our meth… ▽ More This paper presents a Convolutional Neural Network (CNN) approach for counting and locating objects in high-density imagery. To the best of our knowledge, this is the first object counting and locating method based on a feature map enhancement and a Multi-Stage Refinement of the confidence map. The proposed method was evaluated in two counting datasets: tree and car. For the tree dataset, our method returned a mean absolute error (MAE) of 2.05, a root-mean-squared error (RMSE) of 2.87 and a coefficient of determination (R$^2$) of 0.986. For the car dataset (CARPK and PUCPR+), our method was superior to state-of-the-art methods. In the these datasets, our approach achieved an MAE of 4.45 and 3.16, an RMSE of 6.18 and 4.39, and an R$^2$ of 0.975 and 0.999, respectively. The proposed method is suitable for dealing with high object-density, returning a state-of-the-art performance for counting and locating objects. △ Less

Submitted 8 February, 2021; originally announced February 2021.

Comments: 15 pages, 10 figures, 8 tables

MSC Class: 68T07 ACM Class: I.2.1

Journal ref: Expert Systems with Applications, 2022

A Deep Learning Approach Based on Graphs to Detect Plantation Lines

Authors: Diogo Nunes Gonçalves, Mauro dos Santos de Arruda, Hemerson Pistori, Vanessa Jordão Marcato Fernandes, Ana Paula Marques Ramos, Danielle Elis Garcia Furuya, Lucas Prado Osco, Hongjie He, Jonathan Li, José Marcato Junior, Wesley Nunes Gonçalves

Abstract: Deep learning-based networks are among the most prominent methods to learn linear patterns and extract this type of information from diverse imagery conditions. Here, we propose a deep learning approach based on graphs to detect plantation lines in UAV-based RGB imagery presenting a challenging scenario containing spaced plants. The first module of our method extracts a feature map throughout the… ▽ More Deep learning-based networks are among the most prominent methods to learn linear patterns and extract this type of information from diverse imagery conditions. Here, we propose a deep learning approach based on graphs to detect plantation lines in UAV-based RGB imagery presenting a challenging scenario containing spaced plants. The first module of our method extracts a feature map throughout the backbone, which consists of the initial layers of the VGG16. This feature map is used as an input to the Knowledge Estimation Module (KEM), organized in three concatenated branches for detecting 1) the plant positions, 2) the plantation lines, and 3) for the displacement vectors between the plants. A graph modeling is applied considering each plant position on the image as vertices, and edges are formed between two vertices (i.e. plants). Finally, the edge is classified as pertaining to a certain plantation line based on three probabilities (higher than 0.5): i) in visual features obtained from the backbone; ii) a chance that the edge pixels belong to a line, from the KEM step; and iii) an alignment of the displacement vectors with the edge, also from KEM. Experiments were conducted in corn plantations with different growth stages and patterns with aerial RGB imagery. A total of 564 patches with 256 x 256 pixels were used and randomly divided into training, validation, and testing sets in a proportion of 60\%, 20\%, and 20\%, respectively. The proposed method was compared against state-of-the-art deep learning methods, and achieved superior performance with a significant margin, returning precision, recall, and F1-score of 98.7\%, 91.9\%, and 95.1\%, respectively. This approach is useful in extracting lines with spaced plantation patterns and could be implemented in scenarios where plantation gaps occur, generating lines with few-to-none interruptions. △ Less

Submitted 5 February, 2021; originally announced February 2021.

Comments: 19 pages, 11 figures, 4 tables

MSC Class: 68Txx

Bayesian Paired-Comparison with the bpcs Package

Authors: David Issa Mattos, Érika Martins Silva Ramos

Abstract: This article introduces the bpcs R package (Bayesian Paired Comparison in Stan) and the statistical models implemented in the package. This package aims to facilitate the use of Bayesian models for paired comparison data in behavioral research. Bayesian analysis of paired comparison data allows parameter estimation even in conditions where the maximum likelihood does not exist, allows easy extensi… ▽ More This article introduces the bpcs R package (Bayesian Paired Comparison in Stan) and the statistical models implemented in the package. This package aims to facilitate the use of Bayesian models for paired comparison data in behavioral research. Bayesian analysis of paired comparison data allows parameter estimation even in conditions where the maximum likelihood does not exist, allows easy extension of paired comparison models, provide straightforward interpretation of the results with credible intervals, have better control of type I error, have more robust evidence towards the null hypothesis, allows propagation of uncertainties, includes prior information, and perform well when handling models with many parameters and latent variables. The bpcs package provides a consistent interface for R users and several functions to evaluate the posterior distribution of all parameters, to estimate the posterior distribution of any contest between items, and to obtain the posterior distribution of the ranks. Three reanalyses of recent studies that used the frequentist Bradley-Terry model are presented. These reanalyses are conducted with the Bayesian models of the bpcs package, and all the code used to fit the models, generate the figures, and the tables are available in the online appendix. △ Less

Submitted 20 September, 2021; v1 submitted 27 January, 2021; originally announced January 2021.

Comments: Accepted for publication in the Journal of Behavior Research Methods (https://www.springer.com/journal/13428)

A Review on Deep Learning in UAV Remote Sensing

Authors: Lucas Prado Osco, José Marcato Junior, Ana Paula Marques Ramos, Lúcio André de Castro Jorge, Sarah Narges Fatholahi, Jonathan de Andrade Silva, Edson Takashi Matsubara, Hemerson Pistori, Wesley Nunes Gonçalves, Jonathan Li

Abstract: Deep Neural Networks (DNNs) learn representation from data with an impressive capability, and brought important breakthroughs for processing images, time-series, natural language, audio, video, and many others. In the remote sensing field, surveys and literature revisions specifically involving DNNs algorithms' applications have been conducted in an attempt to summarize the amount of information p… ▽ More Deep Neural Networks (DNNs) learn representation from data with an impressive capability, and brought important breakthroughs for processing images, time-series, natural language, audio, video, and many others. In the remote sensing field, surveys and literature revisions specifically involving DNNs algorithms' applications have been conducted in an attempt to summarize the amount of information produced in its subfields. Recently, Unmanned Aerial Vehicles (UAV) based applications have dominated aerial sensing research. However, a literature revision that combines both "deep learning" and "UAV remote sensing" thematics has not yet been conducted. The motivation for our work was to present a comprehensive review of the fundamentals of Deep Learning (DL) applied in UAV-based imagery. We focused mainly on describing classification and regression techniques used in recent applications with UAV-acquired data. For that, a total of 232 papers published in international scientific journal databases was examined. We gathered the published material and evaluated their characteristics regarding application, sensor, and technique used. We relate how DL presents promising results and has the potential for processing tasks associated with UAV-based image data. Lastly, we project future perspectives, commentating on prominent DL paths to be explored in the UAV remote sensing field. Our revision consists of a friendly-approach to introduce, commentate, and summarize the state-of-the-art in UAV-based image applications with DNNs algorithms in diverse subfields of remote sensing, grouping it in the environmental, urban, and agricultural contexts. △ Less

Submitted 20 August, 2023; v1 submitted 22 January, 2021; originally announced January 2021.

Comments: 27 pages, 10 figures

Journal ref: International Journal of Applied Earth Observation and Geoinformation, 2022

A CNN Approach to Simultaneously Count Plants and Detect Plantation-Rows from UAV Imagery

Authors: Lucas Prado Osco, Mauro dos Santos de Arruda, Diogo Nunes Gonçalves, Alexandre Dias, Juliana Batistoti, Mauricio de Souza, Felipe David Georges Gomes, Ana Paula Marques Ramos, Lúcio André de Castro Jorge, Veraldo Liesenberg, Jonathan Li, Lingfei Ma, José Marcato Junior, Wesley Nunes Gonçalves

Abstract: In this paper, we propose a novel deep learning method based on a Convolutional Neural Network (CNN) that simultaneously detects and geolocates plantation-rows while counting its plants considering highly-dense plantation configurations. The experimental setup was evaluated in a cornfield with different growth stages and in a Citrus orchard. Both datasets characterize different plant density scena… ▽ More In this paper, we propose a novel deep learning method based on a Convolutional Neural Network (CNN) that simultaneously detects and geolocates plantation-rows while counting its plants considering highly-dense plantation configurations. The experimental setup was evaluated in a cornfield with different growth stages and in a Citrus orchard. Both datasets characterize different plant density scenarios, locations, types of crops, sensors, and dates. A two-branch architecture was implemented in our CNN method, where the information obtained within the plantation-row is updated into the plant detection branch and retro-feed to the row branch; which are then refined by a Multi-Stage Refinement method. In the corn plantation datasets (with both growth phases, young and mature), our approach returned a mean absolute error (MAE) of 6.224 plants per image patch, a mean relative error (MRE) of 0.1038, precision and recall values of 0.856, and 0.905, respectively, and an F-measure equal to 0.876. These results were superior to the results from other deep networks (HRNet, Faster R-CNN, and RetinaNet) evaluated with the same task and dataset. For the plantation-row detection, our approach returned precision, recall, and F-measure scores of 0.913, 0.941, and 0.925, respectively. To test the robustness of our model with a different type of agriculture, we performed the same task in the citrus orchard dataset. It returned an MAE equal to 1.409 citrus-trees per patch, MRE of 0.0615, precision of 0.922, recall of 0.911, and F-measure of 0.965. For citrus plantation-row detection, our approach resulted in precision, recall, and F-measure scores equal to 0.965, 0.970, and 0.964, respectively. The proposed method achieved state-of-the-art performance for counting and geolocating plants and plant-rows in UAV images from different types of crops. △ Less

Submitted 14 February, 2021; v1 submitted 31 December, 2020; originally announced December 2020.

Comments: 27 pages, 12 figures, 9 tables

ACM Class: J.2

Journal ref: ISPRS JOURNAL OF PHOTOGRAMMETRY AND REMOTE SENSING 174 (2021) 1-17

Modeling and Implementation of Quadcopter Autonomous Flight Based on Alternative Methods to Determine Propeller Parameters

Authors: Gene Patrick S. Rible, Nicolette Ann A. Arriola, Manuel C. Ramos Jr

Abstract: To properly simulate and implement a quadcopter flight control for intended load and flight conditions, the quadcopter model must have parameters on various relationships including propeller thrust-torque, thrust-PWM, and thrust--angular speed to a certain level of accuracy. Thrust-torque modeling requires an expensive reaction torque measurement sensor. In the absence of sophisticated equipment,… ▽ More To properly simulate and implement a quadcopter flight control for intended load and flight conditions, the quadcopter model must have parameters on various relationships including propeller thrust-torque, thrust-PWM, and thrust--angular speed to a certain level of accuracy. Thrust-torque modeling requires an expensive reaction torque measurement sensor. In the absence of sophisticated equipment, the study comes up with alternative methods to complete the quadcopter model. The study also presents a method of modeling the rotational aerodynamic drag on the quadcopter. Although the resulting model of the reaction torque generated by the quadcopter's propellers and the model of the drag torque acting on the quadcopter body that are derived using the methods in this study may not yield the true values of these quantities, the experimental modeling techniques presented in this work ensure that the derived dynamic model for the quadcopter will nevertheless behave identically with the true model for the quadcopter. The derived dynamic model is validated by basic flight controller simulation and actual flight implementation. The model is used as basis for a quadcopter design, which eventually is used for test purposes of basic flight control. This study serves as a baseline for fail-safe control of a quadcopter experiencing an unexpected motor failure. △ Less

Submitted 17 October, 2020; originally announced October 2020.

Comments: 15 pages, 20 figures

ACM Class: I.2.9

Journal ref: Advances in Science, Technology and Engineering Systems Journal, vol. 5, no. 5, pp. 727-741 (2020)

Fail-Safe Controller Architectures for Quadcopter with Motor Failures

Authors: Gene Patrick S. Rible, Nicolette Ann A. Arriola, Manuel C. Ramos, Jr

Abstract: A fail-safe algorithm in case of motor failure was developed, simulated, and tested. For practical fail-safe flight, the quadcopter may fly with only three or two opposing propellers. Altitude for two-propeller architecture was maintained by a PID controller that is independent from the inner and outer controllers. A PID controller on propeller force deviations from equilibrium was augmented to th… ▽ More A fail-safe algorithm in case of motor failure was developed, simulated, and tested. For practical fail-safe flight, the quadcopter may fly with only three or two opposing propellers. Altitude for two-propeller architecture was maintained by a PID controller that is independent from the inner and outer controllers. A PID controller on propeller force deviations from equilibrium was augmented to the inner controller of the three-propeller architecture. Both architectures used LQR for the inner attitude controller and a damped second order outer controller that zeroes the error along the horizontal coordinates. The restrictiveness, stability, robustness, and symmetry of these architectures were investigated with respect to their output limits, initial conditions, and controller frequencies. Although the three-propeller architecture allows for distribution of propeller forces, the two-propeller architecture is more efficient, robust, and stable. The two-propeller architecture is also robust to model uncertainties. It was shown that higher yaw rate leads to greater stability when operating in fail-safe mode. △ Less

Submitted 21 September, 2020; originally announced September 2020.

Comments: 7 pages, 9 figures, published in the 2020 6th International Conference on Control, Automation and Robotics (ICCAR) Proceedings

ACM Class: I.2.9

Journal ref: "Fail-Safe Controller Architectures for Quadcopter with Motor Failures," 2020 6th International Conference on Control, Automation and Robotics (ICCAR), Singapore, Singapore, 2020, pp. 384-391

Generation and Distribution of Quantum Oblivious Keys for Secure Multiparty Computation

Authors: Mariano Lemus, Mariana F. Ramos, Preeti Yadav, Nuno A. Silva, Nelson J. Muga, Andre Souto, Nikola Paunkovic, Paulo Mateus, Armando N. Pinto

Abstract: The oblivious transfer primitive is sufficient to implement secure multiparty computation. However, secure multiparty computation based only on classical cryptography is severely limited by the security and efficiency of the oblivious transfer implementation. We present a method to efficiently and securely generate and distribute oblivious keys by exchanging qubits and by performing commitments us… ▽ More The oblivious transfer primitive is sufficient to implement secure multiparty computation. However, secure multiparty computation based only on classical cryptography is severely limited by the security and efficiency of the oblivious transfer implementation. We present a method to efficiently and securely generate and distribute oblivious keys by exchanging qubits and by performing commitments using classical hash functions. With the presented hybrid approach, quantum and classical, we obtain a practical and high-speed oblivious transfer protocol, secure even against quantum computer attacks. The oblivious distributed keys allow implementing a fast and secure oblivious transfer protocol, which can pave the way for the widespread of applications based on secure multiparty computation. △ Less

Submitted 17 June, 2020; v1 submitted 25 September, 2019; originally announced September 2019.

Comments: 11 pages, 5 figures

Journal ref: Appl. Sci. 2020, 10(12), 4080

Random Linear Network Coding on Programmable Switches

Authors: Diogo Gonçalves, Salvatore Signorello, Fernando M. V. Ramos, Muriel Médard

Abstract: By extending the traditional store-and-forward mechanism, network coding has the capability to improve a network's throughput, robustness, and security. Given the fundamentally different packet processing required by this new paradigm and the inflexibility of hardware, existing solutions are based on software. As a result, they have limited performance and scalability, creating a barrier to its wi… ▽ More By extending the traditional store-and-forward mechanism, network coding has the capability to improve a network's throughput, robustness, and security. Given the fundamentally different packet processing required by this new paradigm and the inflexibility of hardware, existing solutions are based on software. As a result, they have limited performance and scalability, creating a barrier to its wide-spread adoption. By leveraging the recent advances in programmable networking hardware, in this paper we propose a random linear network coding data plane written in P4, as a first step towards a production-level platform. Our solution includes the ability to combine the payload of multiple packets and of executing the required Galois field operations, and shows promise to be practical even under the strict memory and processing constraints of switching hardware. △ Less

Submitted 5 September, 2019; originally announced September 2019.

Comments: 6 pages, 4 figures

ACM Class: C.2.1; C.2.2; C.2.3

Rama: Controller Fault Tolerance in Software-Defined Networking Made Practical

Authors: André Mantas, Fernando M. V. Ramos

Abstract: In Software-Defined Networking (SDN), network applications use the logically centralized network view provided by the controller to remotely orchestrate the network switches. To avoid the controller being a single point of failure, traditional fault-tolerance techniques are employed to guarantee availability, a fundamental requirement in production environments. Unfortunately, these techniques fal… ▽ More In Software-Defined Networking (SDN), network applications use the logically centralized network view provided by the controller to remotely orchestrate the network switches. To avoid the controller being a single point of failure, traditional fault-tolerance techniques are employed to guarantee availability, a fundamental requirement in production environments. Unfortunately, these techniques fall short of ensuring correct network behaviour under controller failures. The problem of these techniques is that they deal with only part of the problem: guaranteeing that application and controller state remains consistent between replicas. However, in an SDN the switches maintain hard state that must also be handled consistently. Fault-tolerant SDN must therefore include switch state into the problem. A recently proposed fault-tolerant controller platform, Ravana, solves this problem by extending fault-tolerant SDN control with mechanisms that guarantee control messages to be processed transactionally and exactly once, at both the controllers and the switches. These guarantees are given even in the face of controller and switch crashes. The elegance of this solution comes at a cost. Ravana requires switches to be modified and OpenFlow to be extended with hitherto unforeseen additions to the protocol. In face of this challenge we propose Rama, a fault-tolerant SDN controller platform that offers the same strong guarantees as Ravana without requiring modifications to switches or to the OpenFlow protocol. Experiments with our prototype implementation show the additional overhead to be modest, making Rama the first fault-tolerant SDN solution that can be immediately deployable. △ Less

Submitted 5 February, 2019; originally announced February 2019.

Impact of network randomness on multiple opinion dynamics

Authors: Vivian Dornelas, Marlon Ramos, Celia Anteneodo

Abstract: People often face the challenge of choosing among different options with similar attractiveness. To study the distribution of preferences that emerge in such situations, a useful approach is to simulate opinion dynamics on top of complex networks, composed by nodes (individuals) and their connections (edges), where the state of each node can be one amongst several opinions including the undecided… ▽ More People often face the challenge of choosing among different options with similar attractiveness. To study the distribution of preferences that emerge in such situations, a useful approach is to simulate opinion dynamics on top of complex networks, composed by nodes (individuals) and their connections (edges), where the state of each node can be one amongst several opinions including the undecided state. We use two different dynamics rules: the one proposed by Travieso-Fontoura (TF) and the plurality rule (PR), which are paradigmatic of outflow and inflow dynamics, respectively. We are specially interested in the impact of the network randomness on the final distribution of opinions. For that purpose, we consider Watts-Strogatz networks, which possess the small-world property, and where randomness is controlled by a probability $p$ of adding random shortcuts to an initially regular network. Depending on the value of $p$, the average connectivity $\langle k \rangle$, and the initial conditions, the final distribution can be basically (i) consensus, (ii) coexistence of different options, or (iii) predominance of indecision. We find that, in both dynamics, the predominance of a winning opinion is favored by increasing the number of reconnections (shortcuts), promoting consensus. In contrast to the TF case, in the PR dynamics, a fraction of undecided nodes can persist in the final state. In such cases, a maximum number of undecided nodes occurs within the small-world region, due to ties in the decision group. △ Less

Submitted 7 January, 2018; originally announced January 2018.

ANCHOR: logically-centralized security for Software-Defined Networks

Authors: Diego Kreutz, Jiangshan Yu, Fernando M. V. Ramos, Paulo Esteves-Verissimo

Abstract: While the centralization of SDN brought advantages such as a faster pace of innovation, it also disrupted some of the natural defenses of traditional architectures against different threats. The literature on SDN has mostly been concerned with the functional side, despite some specific works concerning non-functional properties like 'security' or 'dependability'. Though addressing the latter in an… ▽ More While the centralization of SDN brought advantages such as a faster pace of innovation, it also disrupted some of the natural defenses of traditional architectures against different threats. The literature on SDN has mostly been concerned with the functional side, despite some specific works concerning non-functional properties like 'security' or 'dependability'. Though addressing the latter in an ad-hoc, piecemeal way, may work, it will most likely lead to efficiency and effectiveness problems. We claim that the enforcement of non-functional properties as a pillar of SDN robustness calls for a systemic approach. As a general concept, we propose ANCHOR, a subsystem architecture that promotes the logical centralization of non-functional properties. To show the effectiveness of the concept, we focus on 'security' in this paper: we identify the current security gaps in SDNs and we populate the architecture middleware with the appropriate security mechanisms, in a global and consistent manner. Essential security mechanisms provided by anchor include reliable entropy and resilient pseudo-random generators, and protocols for secure registration and association of SDN devices. We claim and justify in the paper that centralizing such mechanisms is key for their effectiveness, by allowing us to: define and enforce global policies for those properties; reduce the complexity of controllers and forwarding devices; ensure higher levels of robustness for critical services; foster interoperability of the non-functional property enforcement mechanisms; and promote the security and resilience of the architecture itself. We discuss design and implementation aspects, and we prove and evaluate our algorithms and mechanisms, including the formalisation of the main protocols and the verification of their core security properties using the Tamarin prover. △ Less

Submitted 31 December, 2018; v1 submitted 9 November, 2017; originally announced November 2017.

Comments: 42 pages, 4 figures, 3 tables, 5 algorithms, 139 references

AngularJS Performance: A Survey Study

Authors: Miguel Ramos, Marco Tulio Valente, Ricardo Terra

Abstract: AngularJS is a popular JavaScript MVC-based framework to construct single-page web applications. In this paper, we report the results of a survey with 95 professional developers about performance issues of AngularJS applications. We report common practices followed by developers to avoid performance problems (e.g., use of third-party or custom components), the general causes of performance problem… ▽ More AngularJS is a popular JavaScript MVC-based framework to construct single-page web applications. In this paper, we report the results of a survey with 95 professional developers about performance issues of AngularJS applications. We report common practices followed by developers to avoid performance problems (e.g., use of third-party or custom components), the general causes of performance problems in AngularJS applications (e.g., inadequate architecture decisions taken by AngularJS users), and the technical and specific causes of performance problems (e.g., unnecessary processing included in the digest cycle, which is the internal computation that automatically updates the view with changes detected in the model). △ Less

Submitted 6 May, 2017; originally announced May 2017.

Comments: Accepted at IEEE Software

Secure Multi-Cloud Virtual Network Embedding

Authors: Max Alaluna, Luís Ferrolho, José Rui Figueira, Nuno Neves, Fernando M. V. Ramos

Abstract: Modern network virtualization platforms enable users to specify custom topologies and arbitrary addressing schemes for their virtual networks. These platforms have, however, been targeting the data center of a single provider, which is insufficient to support (critical) applications that need to be deployed across multiple trust domains, while enforcing diverse security requirements. This paper ad… ▽ More Modern network virtualization platforms enable users to specify custom topologies and arbitrary addressing schemes for their virtual networks. These platforms have, however, been targeting the data center of a single provider, which is insufficient to support (critical) applications that need to be deployed across multiple trust domains, while enforcing diverse security requirements. This paper addresses this limitation by presenting a novel solution for the central resource allocation problem of network virtualization -- the virtual network embedding, which aims to find efficient mappings of virtual network requests onto the substrate network. We improve over the state-of-the-art by considering security as a first-class citizen of virtual networks, while enhancing the substrate infrastructure with resources from multiple cloud providers. Our solution enables the definition of flexible policies in three core elements: on the virtual links, where alternative security compromises can be explored (e.g., encryption); on the virtual switches, supporting various degrees of protection and redundancy if necessary; and on the substrate infrastructure, extending it across multiple clouds, including public and private facilities, with their inherently diverse trust levels associated. We propose an optimal solution to this problem formulated as a Mixed Integer Linear Program (MILP). The results of our evaluation give insight into the trade-offs associated with the inclusion of security demands into network virtualization. In particular, they provide evidence that enhancing the user's virtual networks with security does not preclude high acceptance rates and an efficient use of resources, and allows providers to increase their revenues. △ Less

Submitted 6 October, 2018; v1 submitted 3 March, 2017; originally announced March 2017.

Comments: 1. Paper title changed to be more suitable; 2. Rewrite Introduction (section 1), Secure Virtual Network Embedding Problem (section 3) and MILP Formulation (Section 5) to make it clearer; 3. Figure 3 inserted to help in explanation on the main and backup VNE mappings; 4. Added references on Related Work (Section 7)

The KISS principle in Software-Defined Networking: An architecture for Keeping It Simple and Secure

Authors: Diego Kreutz, Jiangshan Yu, Paulo Esteves-Verissimo, Catia Magalhaes, Fernando M. V. Ramos

Abstract: Security is an increasingly fundamental requirement in Software-Defined Networking (SDN). However, the pace of adoption of secure mechanisms has been slow, which we estimate to be a consequence of the performance overhead of traditional solutions and of the complexity of the support infrastructure required. As a first step to addressing these problems, we propose a modular secure SDN control plane… ▽ More Security is an increasingly fundamental requirement in Software-Defined Networking (SDN). However, the pace of adoption of secure mechanisms has been slow, which we estimate to be a consequence of the performance overhead of traditional solutions and of the complexity of the support infrastructure required. As a first step to addressing these problems, we propose a modular secure SDN control plane communications architecture, KISS, with innovative solutions in the context of key distribution and secure channel support. A comparative analysis of the performance impact of essential security primitives guided our selection of basic primitives for KISS. We further propose iDVV, the integrated device verification value, a deterministic but indistinguishable-from-random secret code generation protocol, allowing the local but synchronized generation/verification of keys at both ends of the channel, even on a per-message basis. iDVV is expected to give an important contribution both to the robustness and simplification of the authentication and secure communication problems in SDN. We show that our solution, while offering the same security properties, outperforms reference alternatives, with performance improvements up to 30% over OpenSSL, and improvement in robustness based on a code footprint one order of magnitude smaller. Finally, we also prove and test randomness of the proposed algorithms. △ Less

Submitted 2 November, 2017; v1 submitted 14 February, 2017; originally announced February 2017.

Comments: 12 pages, 7 figures, 2 algorithms, 41 references

AngularJS in the Wild: A Survey with 460 Developers

Authors: Miguel Ramos, Marco Tulio Valente, Ricardo Terra, Gustavo Santos

Abstract: To implement modern web applications, a new family of JavaScript frameworks has emerged, using the MVC pattern. Among these frameworks, the most popular one is AngularJS, which is supported by Google. In spite of its popularity, there is not a clear knowledge on how AngularJS design and features affect the development experience of Web applications. Therefore, this paper reports the results of a s… ▽ More To implement modern web applications, a new family of JavaScript frameworks has emerged, using the MVC pattern. Among these frameworks, the most popular one is AngularJS, which is supported by Google. In spite of its popularity, there is not a clear knowledge on how AngularJS design and features affect the development experience of Web applications. Therefore, this paper reports the results of a survey about AngularJS, including answers from 460 developers. Our contributions include the identification of the most appreciated features of AngularJS (e.g., custom interface components, dependency injection, and two-way data binding) and the most problematic aspects of the framework (e.g., performance and implementation of directives). △ Less

Submitted 27 September, 2016; v1 submitted 5 August, 2016; originally announced August 2016.

Comments: Accepted at 7th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU)

An SDN-based approach to enhance BGP security

Authors: Regivaldo Costa, Fernando M. V. Ramos

Abstract: BGP is vulnerable to a series of attacks. Many solutions have been proposed in the past two decades, but the most effective remain largely undeployed. This is due to three fundamental reasons: the solutions are too computationally expensive for current routers, they require changes to BGP, and/or they do not give the right incentives to promote deployment. In this abstract we propose a Software-… ▽ More BGP is vulnerable to a series of attacks. Many solutions have been proposed in the past two decades, but the most effective remain largely undeployed. This is due to three fundamental reasons: the solutions are too computationally expensive for current routers, they require changes to BGP, and/or they do not give the right incentives to promote deployment. In this abstract we propose a Software-Defined Networking (SDN) architecture to secure BGP routing. Our solution, BGPSecX, targets an IXP and it includes techniques to allow different IXPs to collaborate. With SDN we remove the computational burden from routers and do not make changes to BGP. Targeting IXPs and promoting inter-IXP collaboration enables the creation of incentives to foster adoption of BGP security services. △ Less

Submitted 12 March, 2016; v1 submitted 7 February, 2016; originally announced February 2016.

Consistent and fault-tolerant SDN with unmodified switches

Authors: André Mantas, Fernando M. V. Ramos

Abstract: In a reliable SDN environment, different controllers coordinate different switches and backup controllers can be set in place to tolerate faults. This approach increases the challenge to maintain a consistent network view. If this global view is not consistent with the actual network state, applications will operate on a stale state and potentially lead to incorrect behavior. Faced with this pro… ▽ More In a reliable SDN environment, different controllers coordinate different switches and backup controllers can be set in place to tolerate faults. This approach increases the challenge to maintain a consistent network view. If this global view is not consistent with the actual network state, applications will operate on a stale state and potentially lead to incorrect behavior. Faced with this problem, we propose a fault-tolerant SDN controller that is able to maintain a consistent network view by using transactional semantics on both control and data plane state. Different from previous proposals, our solution does not require changes to OpenFlow or to switches, increasing the chances of quicker adoption. △ Less

Submitted 13 March, 2016; v1 submitted 12 February, 2016; originally announced February 2016.

Comments: 2 pages

Secure and Dependable Virtual Network Embedding

Authors: Luís Ferrolho, Max Alaluna, Nuno Neves, Fernando M. V. Ramos

Abstract: One of the fundamental problems in network virtualization is Virtual Network Embedding (VNE). The VNE problem deals with finding an effective mapping of the virtual nodes & links onto the substrate network. The recent advances in network virtualization gave cloud operators the ability to extend their cloud computing offerings with virtual networks. This trend, jointly with the increasing evidence… ▽ More One of the fundamental problems in network virtualization is Virtual Network Embedding (VNE). The VNE problem deals with finding an effective mapping of the virtual nodes & links onto the substrate network. The recent advances in network virtualization gave cloud operators the ability to extend their cloud computing offerings with virtual networks. This trend, jointly with the increasing evidence of incidents in cloud facilities demonstrate that security and dependability is becoming a critical factor that should be considered by VNE algorithms. In this abstract we propose a VNE solution that considers security and dependability as first class citizens. The resiliency properties of our solution are enhanced by assuming a multiple cloud provider model. △ Less

Submitted 6 February, 2016; originally announced February 2016.

(Literally) above the clouds: virtualizing the network over multiple clouds

Authors: Max Alaluna, Fernando M. V. Ramos, Nuno Neves

Abstract: Recent SDN-based solutions give cloud providers the opportunity to extend their "as-a-service" model with the offer of complete network virtualization. They provide tenants with the freedom to specify the network topologies and addressing schemes of their choosing, while guaranteeing the required level of isolation among them. These platforms, however, have been targeting the datacenter of a singl… ▽ More Recent SDN-based solutions give cloud providers the opportunity to extend their "as-a-service" model with the offer of complete network virtualization. They provide tenants with the freedom to specify the network topologies and addressing schemes of their choosing, while guaranteeing the required level of isolation among them. These platforms, however, have been targeting the datacenter of a single cloud provider with full control over the infrastructure. This paper extends this concept further by supporting the creation of virtual networks that span across several datacenters, which may belong to distinct cloud providers, while including private facilities owned by the tenant. In order to achieve this, we introduce a new network layer above the existing cloud hypervisors, affording the necessary level of control over the communications while hiding the heterogeneity of the clouds. The benefits of this approach are various, such as enabling finer decisions on where to place the virtual machines (e.g., to fulfill legal requirements), avoiding single points of failure, and potentially decreasing costs. Although our focus in the paper is on architecture design, we also present experimental results of a first prototype of the proposed solution. △ Less

Submitted 10 March, 2016; v1 submitted 3 December, 2015; originally announced December 2015.

Medusa: An Efficient Cloud Fault-Tolerant MapReduce

Authors: Pedro A. R. S. Costa, Xiao Bai, Fernando M. V. Ramos, Miguel Correia

Abstract: Applications such as web search and social networking have been moving from centralized to decentralized cloud architectures to improve their scalability. MapReduce, a programming framework for processing large amounts of data using thousands of machines in a single cloud, also needs to be scaled out to multiple clouds to adapt to this evolution. The challenge of building a multi-cloud distributed… ▽ More Applications such as web search and social networking have been moving from centralized to decentralized cloud architectures to improve their scalability. MapReduce, a programming framework for processing large amounts of data using thousands of machines in a single cloud, also needs to be scaled out to multiple clouds to adapt to this evolution. The challenge of building a multi-cloud distributed architecture is substantial. Notwithstanding, the ability to deal with the new types of faults introduced by such setting, such as the outage of a whole datacenter or an arbitrary fault caused by a malicious cloud insider, increases the endeavor considerably. In this paper we propose Medusa, a platform that allows MapReduce computations to scale out to multiple clouds and tolerate several types of faults. Our solution fulfills four objectives. First, it is transparent to the user, who writes her typical MapReduce application without modification. Second, it does not require any modification to the widely used Hadoop framework. Third, the proposed system goes well beyond the fault-tolerance offered by MapReduce to tolerate arbitrary faults, cloud outages, and even malicious faults caused by corrupt cloud insiders. Fourth, it achieves this increased level of fault tolerance at reasonable cost. We performed an extensive experimental evaluation in the ExoGENI testbed, demonstrating that our solution significantly reduces execution time when compared to traditional methods that achieve the same level of resilience. △ Less

Submitted 23 November, 2015; originally announced November 2015.

Formalization of context-free language theory

Authors: Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, José Carlos Bacelar Almeida

Abstract: Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of fundamental results related to context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless… ▽ More Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of fundamental results related to context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols inaccessible symbols, empty rules and unit rules) and the existence of a Chomsky Normal Form for context-free grammars. △ Less

Submitted 30 October, 2015; originally announced October 2015.

Formalization of the pumping lemma for context-free languages

Authors: Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, José Carlos Bacelar Almeida

Abstract: Context-free languages (CFLs) are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages. Context-free languages (CFLs) are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages. △ Less

Submitted 15 October, 2015; originally announced October 2015.

Formalization of simplification for context-free grammars

Authors: Marcus V. M. Ramos, Ruy J. G. B. de Queiroz

Abstract: Context-free grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of the fact that general context-free grammars generate languages that can be also generated by simpler and equivalent context-free grammars. Namely, useless symbol elimination, inacc… ▽ More Context-free grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of the fact that general context-free grammars generate languages that can be also generated by simpler and equivalent context-free grammars. Namely, useless symbol elimination, inaccessible symbol elimination, unit rules elimination and empty rules elimination operations were described and proven correct with respect to the preservation of the language generated by the original grammar. △ Less

Submitted 15 October, 2015; v1 submitted 7 September, 2015; originally announced September 2015.

Comments: LSFA 2015

Formalization of closure properties for context-free grammars

Authors: Marcus V. M. Ramos, Ruy J. G. B. de Queiroz

Abstract: Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and the Coq proof assistant. The results obtained so far include the representation of context-free grammars, the description of algorithms for some operations on… ▽ More Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and the Coq proof assistant. The results obtained so far include the representation of context-free grammars, the description of algorithms for some operations on them (union, concatenation and closure) and the proof of related theorems (e.g. the correctness of these algorithms). A brief survey of related works is presented, as well as plans for further development. △ Less

Submitted 10 June, 2015; originally announced June 2015.

Journal ref: Preliminary Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications, LSFA'14 (2014), pp. 187-198