Showing 1–20 of 20 results for author: Muñoz, C

Embedding Differential Dynamic Logic in PVS

Authors: J. Tanner Slagel, Mariano Moscato, Lauren White, César A. Muñoz, Swee Balachandran, Aaron Dutle

Abstract: Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and d… ▽ More Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL's proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS. △ Less

Submitted 23 April, 2024; originally announced April 2024.

Comments: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672

ACM Class: F.3.1

Journal ref: EPTCS 402, 2024, pp. 43-62

Eliciting Personality Traits in Large Language Models

Authors: Airlie Hilliard, Cristian Munoz, Zekun Wu, Adriano Soares Koshiyama

Abstract: Large Language Models (LLMs) are increasingly being utilized by both candidates and employers in the recruitment context. However, with this comes numerous ethical concerns, particularly related to the lack of transparency in these "black-box" models. Although previous studies have sought to increase the transparency of these models by investigating the personality traits of LLMs, many of the prev… ▽ More Large Language Models (LLMs) are increasingly being utilized by both candidates and employers in the recruitment context. However, with this comes numerous ethical concerns, particularly related to the lack of transparency in these "black-box" models. Although previous studies have sought to increase the transparency of these models by investigating the personality traits of LLMs, many of the previous studies have provided them with personality assessments to complete. On the other hand, this study seeks to obtain a better understanding of such models by examining their output variations based on different input prompts. Specifically, we use a novel elicitation approach using prompts derived from common interview questions, as well as prompts designed to elicit particular Big Five personality traits to examine whether the models were susceptible to trait-activation like humans are, to measure their personality based on the language used in their outputs. To do so, we repeatedly prompted multiple LMs with different parameter sizes, including Llama-2, Falcon, Mistral, Bloom, GPT, OPT, and XLNet (base and fine tuned versions) and examined their personality using classifiers trained on the myPersonality dataset. Our results reveal that, generally, all LLMs demonstrate high openness and low extraversion. However, whereas LMs with fewer parameters exhibit similar behaviour in personality traits, newer and LMs with more parameters exhibit a broader range of personality traits, with increased agreeableness, emotional stability, and openness. Furthermore, a greater number of parameters is positively associated with openness and conscientiousness. Moreover, fine-tuned models exhibit minor modulations in their personality traits, contingent on the dataset. Implications and directions for future research are discussed. △ Less

Submitted 15 February, 2024; v1 submitted 13 February, 2024; originally announced February 2024.

Comments: Manuscript submitted to ACM Facct. Authors One and Two contributed equally to this work

CompactifAI: Extreme Compression of Large Language Models using Quantum-Inspired Tensor Networks

Authors: Andrei Tomut, Saeed S. Jahromi, Abhijoy Sarkar, Uygar Kurt, Sukhbinder Singh, Faysal Ishtiaq, Cesar Muñoz, Prabdeep Singh Bajaj, Ali Elborady, Gianni del Bimbo, Mehrazin Alizadeh, David Montero, Pablo Martin-Ramiro, Muhammad Ibrahim, Oussama Tahiri Alaoui, John Malcolm, Samuel Mugel, Roman Orus

Abstract: Large Language Models (LLMs) such as ChatGPT and LlaMA are advancing rapidly in generative Artificial Intelligence (AI), but their immense size poses significant challenges, such as huge training and inference costs, substantial energy demands, and limitations for on-site deployment. Traditional compression methods such as pruning, distillation, and low-rank approximation focus on reducing the eff… ▽ More Large Language Models (LLMs) such as ChatGPT and LlaMA are advancing rapidly in generative Artificial Intelligence (AI), but their immense size poses significant challenges, such as huge training and inference costs, substantial energy demands, and limitations for on-site deployment. Traditional compression methods such as pruning, distillation, and low-rank approximation focus on reducing the effective number of neurons in the network, while quantization focuses on reducing the numerical precision of individual weights to reduce the model size while kee** the number of neurons fixed. While these compression methods have been relatively successful in practice, there is no compelling reason to believe that truncating the number of neurons is an optimal strategy. In this context, this paper introduces CompactifAI, an innovative LLM compression approach using quantum-inspired Tensor Networks that focuses on the model's correlation space instead, allowing for a more controlled, refined and interpretable model compression. Our method is versatile and can be implemented with - or on top of - other compression techniques. As a benchmark, we demonstrate that a combination of CompactifAI with quantization allows to reduce a 93% the memory size of LlaMA 7B, reducing also 70% the number of parameters, accelerating 50% the training and 25% the inference times of the model, and just with a small accuracy drop of 2% - 3%, going much beyond of what is achievable today by other compression techniques. Our methods also allow to perform a refined layer sensitivity profiling, showing that deeper layers tend to be more suitable for tensor network compression, which is compatible with recent observations on the ineffectiveness of those layers for LLM performance. Our results imply that standard LLMs are, in fact, heavily overparametrized, and do not need to be large at all. △ Less

Submitted 13 May, 2024; v1 submitted 25 January, 2024; originally announced January 2024.

Comments: 5 pages, 4 figures, 2 tables, and supplementary information of 2 pages and 1 figure. Revised version with new benchmarks for LlaMA2-7B

RaViTT: Random Vision Transformer Tokens

Authors: Felipe A. Quezada, Carlos F. Navarro, Cristian Muñoz, Manuel Zamorano, Jorge Jara-Wilde, Violeta Chang, Cristóbal A. Navarro, Mauricio Cerda

Abstract: Vision Transformers (ViTs) have successfully been applied to image classification problems where large annotated datasets are available. On the other hand, when fewer annotations are available, such as in biomedical applications, image augmentation techniques like introducing image variations or combinations have been proposed. However, regarding ViT patch sampling, less has been explored outside… ▽ More Vision Transformers (ViTs) have successfully been applied to image classification problems where large annotated datasets are available. On the other hand, when fewer annotations are available, such as in biomedical applications, image augmentation techniques like introducing image variations or combinations have been proposed. However, regarding ViT patch sampling, less has been explored outside grid-based strategies. In this work, we propose Random Vision Transformer Tokens (RaViTT), a random patch sampling strategy that can be incorporated into existing ViTs. We experimentally evaluated RaViTT for image classification, comparing it with a baseline ViT and state-of-the-art (SOTA) augmentation techniques in 4 datasets, including ImageNet-1k and CIFAR-100. Results show that RaViTT increases the accuracy of the baseline in all datasets and outperforms the SOTA augmentation techniques in 3 out of 4 datasets by a significant margin +1.23% to +4.32%. Interestingly, RaViTT accuracy improvements can be achieved even with fewer tokens, thus reducing the computational load of any ViT model for a given accuracy value. △ Less

Submitted 19 June, 2023; originally announced June 2023.

Comments: 9 pages, 6 figures

MSC Class: 68T07

Evaluating explainability for machine learning predictions using model-agnostic metrics

Authors: Cristian Munoz, Kleyton da Costa, Bernardo Modenesi, Adriano Koshiyama

Abstract: Rapid advancements in artificial intelligence (AI) technology have brought about a plethora of new challenges in terms of governance and regulation. AI systems are being integrated into various industries and sectors, creating a demand from decision-makers to possess a comprehensive and nuanced understanding of the capabilities and limitations of these systems. One critical aspect of this demand i… ▽ More Rapid advancements in artificial intelligence (AI) technology have brought about a plethora of new challenges in terms of governance and regulation. AI systems are being integrated into various industries and sectors, creating a demand from decision-makers to possess a comprehensive and nuanced understanding of the capabilities and limitations of these systems. One critical aspect of this demand is the ability to explain the results of machine learning models, which is crucial to promoting transparency and trust in AI systems, as well as fundamental in hel** machine learning models to be trained ethically. In this paper, we present novel metrics to quantify the degree of which AI model predictions can be easily explainable by its features. Our metrics summarize different aspects of explainability into scalars, providing a more comprehensive understanding of model predictions and facilitating communication between decision-makers and stakeholders, thereby increasing the overall transparency and accountability of AI systems. △ Less

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

Uncovering Bias in Face Generation Models

Authors: Cristian Muñoz, Sara Zannone, Umar Mohammed, Adriano Koshiyama

Abstract: Recent advancements in GANs and diffusion models have enabled the creation of high-resolution, hyper-realistic images. However, these models may misrepresent certain social groups and present bias. Understanding bias in these models remains an important research question, especially for tasks that support critical decision-making and could affect minorities. The contribution of this work is a nove… ▽ More Recent advancements in GANs and diffusion models have enabled the creation of high-resolution, hyper-realistic images. However, these models may misrepresent certain social groups and present bias. Understanding bias in these models remains an important research question, especially for tasks that support critical decision-making and could affect minorities. The contribution of this work is a novel analysis covering architectures and embedding spaces for fine-grained understanding of bias over three approaches: generators, attribute modifier, and post-processing bias mitigators. This work shows that generators suffer from bias across all social groups with attribute preferences such as between 75%-85% for whiteness and 60%-80% for the female gender (for all trained CelebA models) and low probabilities of generating children and older men. Modifier and mitigators work as post-processor and change the generator performance. For instance, attribute channel perturbation strategies modify the embedding spaces. We quantify the influence of this change on group fairness by measuring the impact on image quality and group features. Specifically, we use the Fréchet Inception Distance (FID), the Face Matching Error and the Self-Similarity score. For Interfacegan, we analyze one and two attribute channel perturbations and examine the effect on the fairness distribution and the quality of the image. Finally, we analyzed the post-processing bias mitigators, which are the fastest and most computationally efficient way to mitigate bias. We find that these mitigation techniques show similar results on KL divergence and FID score, however, self-similarity scores show a different feature concentration on the new groups of the data distribution. The weaknesses and ongoing challenges described in this work must be considered in the pursuit of creating fair and unbiased face generation models. △ Less

Submitted 22 February, 2023; originally announced February 2023.

Exoplanet atmosphere evolution: emulation with neural networks

Authors: James G. Rogers, Clàudia Janó Muñoz, James E. Owen, T. Lucas Makinen

Abstract: Atmospheric mass-loss is known to play a leading role in sculpting the demographics of small, close-in exoplanets. Knowledge of how such planets evolve allows one to ``rewind the clock'' to infer the conditions in which they formed. Here, we explore the relationship between a planet's core mass and their atmospheric mass after protoplanetary disc dispersal by exploiting XUV photoevaporation as an… ▽ More Atmospheric mass-loss is known to play a leading role in sculpting the demographics of small, close-in exoplanets. Knowledge of how such planets evolve allows one to ``rewind the clock'' to infer the conditions in which they formed. Here, we explore the relationship between a planet's core mass and their atmospheric mass after protoplanetary disc dispersal by exploiting XUV photoevaporation as an evolutionary process. Historically, this style of inference problem would be computationally infeasible due to the large number of planet models required; however, we make use of a novel atmospheric evolution emulator which utilises neural networks to provide three orders of magnitude in speedup. First, we provide proof-of-concept for this emulator on a real problem, by inferring the initial atmospheric conditions to the TOI-270 multi-planet system. Using the emulator we find near-indistinguishable results when compared to original model. We then apply the emulator to the more complex inference problem, which aims to find the initial conditions for a sample of \textit{Kepler}, \textit{K2} and \textit{TESS} planets with well-constrained masses and radii. We demonstrate there is a relationship between core masses and the atmospheric mass that they retain after disc dispersal, and this trend is consistent with the `boil-off' scenario, in which close-in planets undergo dramatic atmospheric escape during disc dispersal. Thus, it appears the exoplanet population is consistent with the idea that close-in exoplanets initially acquired large massive atmospheres, the majority of which is lost during disc dispersal; before the final population is sculpted by atmospheric loss over 100~Myr to Gyr timescales. △ Less

Submitted 8 January, 2023; v1 submitted 28 October, 2021; originally announced October 2021.

Comments: 16 pages, 10 figures. Accepted for publication in MNRAS

From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project

Authors: Aaron Dutle, César Muñoz, Esther Conrad, Alwyn Goodloe, Laura Titolo, Ivan Perez, Swee Balachandran, Dimitra Giannakopoulou, Anastasia Mavridou, Thomas Pressburger

Abstract: The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requ… ▽ More The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight. △ Less

Submitted 2 December, 2020; originally announced December 2020.

Comments: In Proceedings FMAS 2020, arXiv:2012.01176

Journal ref: EPTCS 329, 2020, pp. 23-30

Classification and reconstruction of optical quantum states with deep neural networks

Authors: Shahnawaz Ahmed, Carlos Sánchez Muñoz, Franco Nori, Anton Frisk Kockum

Abstract: We apply deep-neural-network-based techniques to quantum state classification and reconstruction. We demonstrate high classification accuracies and reconstruction fidelities, even in the presence of noise and with little data. Using optical quantum states as examples, we first demonstrate how convolutional neural networks (CNNs) can successfully classify several types of states distorted by, e.g.,… ▽ More We apply deep-neural-network-based techniques to quantum state classification and reconstruction. We demonstrate high classification accuracies and reconstruction fidelities, even in the presence of noise and with little data. Using optical quantum states as examples, we first demonstrate how convolutional neural networks (CNNs) can successfully classify several types of states distorted by, e.g., additive Gaussian noise or photon loss. We further show that a CNN trained on noisy inputs can learn to identify the most important regions in the data, which potentially can reduce the cost of tomography by guiding adaptive data collection. Secondly, we demonstrate reconstruction of quantum-state density matrices using neural networks that incorporate quantum-physics knowledge. The knowledge is implemented as custom neural-network layers that convert outputs from standard feedforward neural networks to valid descriptions of quantum states. Any standard feed-forward neural-network architecture can be adapted for quantum state tomography (QST) with our method. We present further demonstrations of our proposed [arXiv:2008.03240] QST technique with conditional generative adversarial networks (QST-CGAN). We motivate our choice of a learnable loss function within an adversarial framework by demonstrating that the QST-CGAN outperforms, across a range of scenarios, generative networks trained with standard loss functions. For pure states with additive or convolutional Gaussian noise, the QST-CGAN is able to adapt to the noise and reconstruct the underlying state. The QST-CGAN reconstructs states using up to two orders of magnitude fewer iterative steps than a standard iterative maximum likelihood (iMLE) method. Further, the QST-CGAN can reconstruct both pure and mixed states from two orders of magnitude fewer randomly chosen data points than iMLE. △ Less

Submitted 3 December, 2020; originally announced December 2020.

Comments: 40 pages, 20 figures, 5 tables, code will be available at https://github.com/quantshah/qst-nn

Journal ref: Phys. Rev. Research 3, 033278 (2021)

Quantum State Tomography with Conditional Generative Adversarial Networks

Authors: Shahnawaz Ahmed, Carlos Sánchez Muñoz, Franco Nori, Anton Frisk Kockum

Abstract: Quantum state tomography (QST) is a challenging task in intermediate-scale quantum devices. Here, we apply conditional generative adversarial networks (CGANs) to QST. In the CGAN framework, two duelling neural networks, a generator and a discriminator, learn multi-modal models from data. We augment a CGAN with custom neural-network layers that enable conversion of output from any standard neural n… ▽ More Quantum state tomography (QST) is a challenging task in intermediate-scale quantum devices. Here, we apply conditional generative adversarial networks (CGANs) to QST. In the CGAN framework, two duelling neural networks, a generator and a discriminator, learn multi-modal models from data. We augment a CGAN with custom neural-network layers that enable conversion of output from any standard neural network into a physical density matrix. To reconstruct the density matrix, the generator and discriminator networks train each other on data using standard gradient-based methods. We demonstrate that our QST-CGAN reconstructs optical quantum states with high fidelity orders of magnitude faster, and from less data, than a standard maximum-likelihood method. We also show that the QST-CGAN can reconstruct a quantum state in a single evaluation of the generator network if it has been pre-trained on similar quantum states. △ Less

Submitted 4 December, 2020; v1 submitted 7 August, 2020; originally announced August 2020.

Comments: 5 pages, 5 figures, code will be available at https://github.com/quantshah/qst-cgan; v2: minor updates; see also the companion paper arXiv:2012.02185

Journal ref: Phys. Rev. Lett. 127, 140502 (2021)

Automatic generation and verification of test-stable floating-point code

Authors: Laura Titolo, Mariano Moscato, Cesar A. Muñoz

Abstract: Test instability in a floating-point program occurs when the control flow of the program diverges from its ideal execution assuming real arithmetic. This phenomenon is caused by the presence of round-off errors that affect the evaluation of arithmetic expressions occurring in conditional statements. Unstable tests may lead to significant errors in safety-critical applications that depend on numeri… ▽ More Test instability in a floating-point program occurs when the control flow of the program diverges from its ideal execution assuming real arithmetic. This phenomenon is caused by the presence of round-off errors that affect the evaluation of arithmetic expressions occurring in conditional statements. Unstable tests may lead to significant errors in safety-critical applications that depend on numerical computations. Writing programs that take into consideration test instability is a difficult task that requires expertise on finite precision computations and rounding errors. This paper presents a toolchain to automatically generate and verify a provably correct test-stable floating-point program from a functional specification in real arithmetic. The input is a real-valued program written in the Prototype Verification System (PVS) specification language and the output is a transformed floating-point C program annotated with ANSI/ISO C Specification Language (ACSL) contracts. These contracts relate the floating-point program to its functional specification in real arithmetic. The transformed program detects if unstable tests may occur and, in these cases, issues a warning and terminate. An approach that combines the Frama-C analyzer, the PRECiSA round-off error estimator, and PVS is proposed to automatically verify that the generated program code is correct in the sense that, if the program terminates without a warning, it follows the same computational path as its real-valued functional specification. △ Less

Submitted 7 January, 2020; originally announced January 2020.

Comments: 32 pages. arXiv admin note: text overlap with arXiv:1808.04289

An Integrated Development Environment for the Prototype Verification System

Authors: Paolo Masci, César A. Muñoz

Abstract: The steep learning curve of formal technologies is a well-known barrier to the adoption of formal verification tools in industry. This paper presents VSCode-PVS, a modern integrated development environment for the Prototype Verification System (PVS). This new environment integrates the editing and proof management functionalities of PVS in Visual Studio Code, a popular code editor widely used by s… ▽ More The steep learning curve of formal technologies is a well-known barrier to the adoption of formal verification tools in industry. This paper presents VSCode-PVS, a modern integrated development environment for the Prototype Verification System (PVS). This new environment integrates the editing and proof management functionalities of PVS in Visual Studio Code, a popular code editor widely used by software developers. VSCode-PVS provides functionalities that developers expect to find in modern verification tools, but are not available in the standard Emacs front-end of PVS, such as auto-completion, point-and-click navigation of definitions, live diagnostics for errors, and literate programming. The main features and architecture of the environment are presented, along with a comparison with other similar tools. △ Less

Submitted 23 December, 2019; originally announced December 2019.

Comments: In Proceedings F-IDE 2019, arXiv:1912.09611

ACM Class: D.2.6 Integrated Environments; D.2.4 Software/Program Verification

Journal ref: EPTCS 310, 2019, pp. 35-49

Eliminating Unstable Tests in Floating-Point Programs

Authors: Laura Titolo, Cesar A. Muñoz, Marco A. Feliu, Mariano M. Moscato

Abstract: Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. This problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in r… ▽ More Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. This problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. The output of this transformation is a floating-point program that is guaranteed to return either the result of the original floating-point program when it can be assured that both its real and its floating-point flows agree or a warning when these flows may diverge. The proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems. △ Less

Submitted 30 November, 2018; v1 submitted 13 August, 2018; originally announced August 2018.

Comments: Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326)

Report number: LOPSTR/2018/1

I(FIB)F: Iterated Bloom Filters for Routing in Named Data Networks

Authors: Cristina Muñoz, Liang Wang, Eduardo Solana, Jon Crowcroft

Abstract: Named Data Networks provide a clean-slate redesign of the Future Internet for efficient content distribution. Because Internet of Things are expected to compose a significant part of Future Internet, most content will be managed by constrained devices. Such devices are often equipped with limited CPU, memory, bandwidth, and energy supply. However, the current Named Data Networks design neglects th… ▽ More Named Data Networks provide a clean-slate redesign of the Future Internet for efficient content distribution. Because Internet of Things are expected to compose a significant part of Future Internet, most content will be managed by constrained devices. Such devices are often equipped with limited CPU, memory, bandwidth, and energy supply. However, the current Named Data Networks design neglects the specific requirements of Internet of Things scenarios and many data structures need to be further optimised. The purpose of this research is to provide an efficient strategy to route in Named Data Networks by constructing a Forwarding Information Base using Iterated Bloom Filters defined as I(FIB)F. We propose the use of content names based on iterative hashes. This strategy leads to reduce the overhead of packets. Moreover, the memory and the complexity required in the forwarding strategy are lower than in current solutions. We compare our proposal with solutions based on hierarchical names and Standard Bloom Filters. We show how to further optimise I(FIB)F by exploiting the structure information contained in hierarchical content names. Finally, two strategies may be followed to reduce: (i) the overall memory for routing or (ii) the probability of false positives. △ Less

Submitted 8 September, 2016; originally announced September 2016.

Proceedings of the Eleventh International Workshop on Developments in Computational Models

Authors: César A. Muñoz, Jorge A. Pérez

Abstract: This volume contains the proceedings of DCM 2015, the 11th International Workshop on Developments in Computational Models held on October 28, 2015 in Cali, Colombia. DCM 2015 was organized as a one-day satellite event of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015). Several new models of computation have emerged in the last few years, and many developments o… ▽ More This volume contains the proceedings of DCM 2015, the 11th International Workshop on Developments in Computational Models held on October 28, 2015 in Cali, Colombia. DCM 2015 was organized as a one-day satellite event of the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015). Several new models of computation have emerged in the last few years, and many developments of traditional computational models have been proposed with the aim of taking into account the new demands of computer systems users and the new capabilities of computation engines. A new computational model, or a new feature in a traditional one, usually is reflected in a new family of programming languages, and new paradigms of software development. The aim of the DCM workshop series is to bring together researchers who are currently develo** new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. Topics of interest include all abstract models of computation and their applications to the development of programming languages and systems. △ Less

Submitted 1 March, 2016; originally announced March 2016.

Journal ref: EPTCS 204, 2016

Design of a Novel Network Architecture for Distributed Event-Based Systems Using Directional Random Walks in an Ubiquitous Sensing Scenario

Authors: Cristina Muñoz, Pierre Leone

Abstract: Ubiquitous sensing devices frequently disseminate data among them. The use of a distributed event-based system that decouples publishers from subscribers arises as an ideal candidate to implement the dissemination process. In this paper, we present a network architecture that merges the network and overlay layers of typical structured event-based systems. Directional random walks are used for the… ▽ More Ubiquitous sensing devices frequently disseminate data among them. The use of a distributed event-based system that decouples publishers from subscribers arises as an ideal candidate to implement the dissemination process. In this paper, we present a network architecture that merges the network and overlay layers of typical structured event-based systems. Directional random walks are used for the construction of this merged layer. Our strategy avoids using a specific network protocol that provides point-to-point communication. This implies that the topology of the network is not maintained, so that nodes not involved in the system are able to save energy and computing resources. We evaluate the performance of the overlay layer using directional random walks and pure random walks for its construction. Our results show that directional random walks are more efficient because: (1) they use less nodes of the network for the establishment of the active path of the overlay layer and (2) they have a more reliable performance. Furthermore, as the number of nodes in the network increases, so do the number of nodes in the active path of the overlay layer for the same number of publishers and subscribers. Finally, we discard any correlation between the number of nodes that form the overlay layer and the maximum Euclidean distance traversed by the walkers. △ Less

Submitted 26 January, 2015; originally announced January 2015.

Comments: 10 pages. arXiv admin note: text overlap with arXiv:1408.3033

Journal ref: International Journal on Advances in Networks and Services, 2014 vol 7 nr 3&4

A Network Architecture for Distributed Event Based Systems in an Ubiquitous Sensing Scenario

Authors: Cristina Muñoz, Pierre Leone

Abstract: Ubiquitous sensing devices frequently disseminate their data between them. The use of a distributed event-based system that decouples publishers of subscribers arises as an ideal candidate to implement the dissemination process. In this paper, we present a network architecture which merges the network and overlay layers of typical structured event-based systems. Directional Random Walks (DRWs) are… ▽ More Ubiquitous sensing devices frequently disseminate their data between them. The use of a distributed event-based system that decouples publishers of subscribers arises as an ideal candidate to implement the dissemination process. In this paper, we present a network architecture which merges the network and overlay layers of typical structured event-based systems. Directional Random Walks (DRWs) are used for the construction of this merged layer. Our first results show that DRWs are suitable to balance the load using a few nodes in the network to construct the dissemination path. As future work, we propose to study the properties of this new layer and to work on the design of Bloom filters to manage broker nodes. △ Less

Submitted 13 August, 2014; originally announced August 2014.

Comments: 5 pages, 6 figures

Proceedings International Workshop on Strategies in Rewriting, Proving, and Programming

Authors: Hélène Kirchner, César Muñoz

Abstract: This volume contains selected papers from the proceedings of the First International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), which was held on July 9, 2010, in Edinburgh, UK. Strategies are ubiquitous in programming languages, automated deduction and reasoning systems. In the two communities of Rewriting and Programming on one side, and of Deduction and Proof engi… ▽ More This volume contains selected papers from the proceedings of the First International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), which was held on July 9, 2010, in Edinburgh, UK. Strategies are ubiquitous in programming languages, automated deduction and reasoning systems. In the two communities of Rewriting and Programming on one side, and of Deduction and Proof engines (Provers, Assistants, Solvers) on the other side, workshops have been launched to make progress towards a deeper understanding of the nature of strategies, their descriptions, their properties, and their usage, in all kinds of computing and reasoning systems. Since more recently, strategies are also playing an important role in rewrite-based programming languages, verification tools and techniques like SAT/SMT engines or termination provers. Moreover strategies have come to be viewed more generally as expressing complex designs for control in computing, modeling, proof search, program transformation, and access control. IWS 2010 was organized as a satellite workshop of FLoC 2010. FLoC 2010 provided an excellent opportunity to foster exchanges between the communities of Rewriting and Programming on one side, and of Deduction and Proof engines on the other side. IWS2010 was a joint follow-up of two series of worshops, held since 1997: the Strategies workshops held by the CADE-IJCAR community and the Workshops on Reduction Strategies (WRS) held by the RTA-RDP community. △ Less

Submitted 23 December, 2010; originally announced December 2010.

Journal ref: EPTCS 44, 2010

Rewriting Logic Semantics of a Plan Execution Language

Authors: Gilles Dowek, César Muñoz, Camilo Rocha

Abstract: The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a high-performance logical engine. The rewriting logic semantics is by itself a formal interpreter of the language and can be used as a semantic benchmark for the implementation of PLEXI… ▽ More The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a high-performance logical engine. The rewriting logic semantics is by itself a formal interpreter of the language and can be used as a semantic benchmark for the implementation of PLEXIL executives. The implementation in Maude has the additional benefit of making available to PLEXIL designers and developers all the formal analysis and verification tools provided by Maude. The formalization of the PLEXIL semantics in rewriting logic poses an interesting challenge due to the synchronous nature of the language and the prioritized rules defining its semantics. To overcome this difficulty, we propose a general procedure for simulating synchronous set relations in rewriting logic that is sound and, for deterministic relations, complete. We also report on two issues at the design level of the original PLEXIL semantics that were identified with the help of the executable specification in Maude. △ Less

Submitted 15 February, 2010; originally announced February 2010.

Journal ref: EPTCS 18, 2010, pp. 77-91

Verified Real Number Calculations: A Library for Interval Arithmetic

Authors: Marc Daumas, David Lester, César Muñoz

Abstract: Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a r… ▽ More Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction. △ Less

Submitted 28 August, 2007; originally announced August 2007.