-
Automatic facial axes standardization of 3D fetal ultrasound images
Authors:
Antonia Alomar,
Ricardo Rubio,
Laura Salort,
Gerard Albaiges,
Antoni Payà,
Gemma Piella,
Federico Sukno
Abstract:
Craniofacial anomalies indicate early developmental disturbances and are usually linked to many genetic syndromes. Early diagnosis is critical, yet ultrasound (US) examinations often fail to identify these features. This study presents an AI-driven tool to assist clinicians in standardizing fetal facial axes/planes in 3D US, reducing sonographer workload and facilitating the facial evaluation. Our…
▽ More
Craniofacial anomalies indicate early developmental disturbances and are usually linked to many genetic syndromes. Early diagnosis is critical, yet ultrasound (US) examinations often fail to identify these features. This study presents an AI-driven tool to assist clinicians in standardizing fetal facial axes/planes in 3D US, reducing sonographer workload and facilitating the facial evaluation. Our network, structured into three blocks-feature extractor, rotation and translation regression, and spatial transformer-processes three orthogonal 2D slices to estimate the necessary transformations for standardizing the facial planes in the 3D US. These transformations are applied to the original 3D US using a differentiable module (the spatial transformer block), yielding a standardized 3D US and the corresponding 2D facial standard planes. The dataset used consists of 1180 fetal facial 3D US images acquired between weeks 20 and 35 of gestation. Results show that our network considerably reduces inter-observer rotation variability in the test set, with a mean geodesic angle difference of 14.12$^{\circ}$ $\pm$ 18.27$^{\circ}$ and an Euclidean angle error of 7.45$^{\circ}$ $\pm$ 14.88$^{\circ}$. These findings demonstrate the network's ability to effectively standardize facial axes, crucial for consistent fetal facial assessments. In conclusion, the proposed network demonstrates potential for improving the consistency and accuracy of fetal facial assessments in clinical settings, facilitating early evaluation of craniofacial anomalies.
△ Less
Submitted 4 September, 2024;
originally announced September 2024.
-
Validity of contextual formulas (extended version)
Authors:
Javier Esparza,
Rubén Rubio
Abstract:
Many well-known logical identities are naturally written as equivalences between contextual formulas. A simple example is the Boole-Shannon expansion $c[p] \equiv (p \wedge c[\mathrm{true}] ) \vee (\neg\, p \wedge c[\mathrm{false}] )$, where $c$ denotes an arbitrary formula with possibly multiple occurrences of a "hole", called a context, and $c[\varphi]$ denotes the result of "filling" all holes…
▽ More
Many well-known logical identities are naturally written as equivalences between contextual formulas. A simple example is the Boole-Shannon expansion $c[p] \equiv (p \wedge c[\mathrm{true}] ) \vee (\neg\, p \wedge c[\mathrm{false}] )$, where $c$ denotes an arbitrary formula with possibly multiple occurrences of a "hole", called a context, and $c[\varphi]$ denotes the result of "filling" all holes of $c$ with the formula $\varphi$. Another example is the unfolding rule $μX. c[X] \equiv c[μX. c[X]]$ of the modal $μ$-calculus.
We consider the modal $μ$-calculus as overarching temporal logic and, as usual, reduce the problem whether $\varphi_1 \equiv \varphi_2$ holds for contextual formulas $\varphi_1, \varphi_2$ to the problem whether $\varphi_1 \leftrightarrow \varphi_2$ is valid . We show that the problem whether a contextual formula of the $μ$-calculus is valid for all contexts can be reduced to validity of ordinary formulas. Our first result constructs a canonical context such that a formula is valid for all contexts if{}f it is valid for this particular one. However, the ordinary formula is exponential in the nesting-depth of the context variables. In a second result we solve this problem, thus proving that validity of contextual formulas is EXP-complete, as for ordinary equivalences. We also prove that both results hold for CTL and LTL as well. We conclude the paper with some experimental results. In particular, we use our implementation to automatically prove the correctness of a set of six contextual equivalences of LTL recently introduced by Esparza et al. for the normalization of LTL formulas. While Esparza et al. need several pages of manual proof, our tool only needs milliseconds to do the job and to compute counterexamples for incorrect variants of the equivalences.
△ Less
Submitted 10 July, 2024;
originally announced July 2024.
-
The Maude strategy language
Authors:
Steven Eker,
Narciso Martí-Oliet,
José Meseguer,
Rubén Rubio,
Alberto Verdejo
Abstract:
Rewriting logic is a natural and expressive framework for the specification of concurrent systems and logics. The Maude specification language provides an implementation of this formalism that allows executing, verifying, and analyzing the represented systems. These specifications declare their objects by means of terms and equations, and provide rewriting rules to represent potentially non-determ…
▽ More
Rewriting logic is a natural and expressive framework for the specification of concurrent systems and logics. The Maude specification language provides an implementation of this formalism that allows executing, verifying, and analyzing the represented systems. These specifications declare their objects by means of terms and equations, and provide rewriting rules to represent potentially non-deterministic local transformations on the state. Sometimes a controlled application of these rules is required to reduce non-determinism, to capture global, goal-oriented or efficiency concerns, or to select specific executions for their analysis. That is what we call a strategy. In order to express them, respecting the separation of concerns principle, a Maude strategy language was proposed and developed. The first implementation of the strategy language was done in Maude itself using its reflective features. After ample experimentation, some more features have been added and, for greater efficiency, the strategy language has been implemented in C++ as an integral part of the Maude system.
This paper describes the Maude strategy language along with its semantics, its implementation decisions, and several application examples from various fields.
△ Less
Submitted 31 January, 2024;
originally announced February 2024.
-
Metalevel transformation of strategies
Authors:
Rubén Rubio,
Narciso Martí-Oliet,
Isabel Pita,
Alberto Verdejo
Abstract:
In the reflective Maude specification language, based on rewriting logic, a strategy language has been introduced to control rule rewriting while avoiding complex and verbose metalevel programs. However, just as multiple levels of reflection are required for some metaprogramming tasks, reflective manipulation and generation of strategies are convenient in multiple situations. Some examples of refl…
▽ More
In the reflective Maude specification language, based on rewriting logic, a strategy language has been introduced to control rule rewriting while avoiding complex and verbose metalevel programs. However, just as multiple levels of reflection are required for some metaprogramming tasks, reflective manipulation and generation of strategies are convenient in multiple situations. Some examples of reflective strategy transformations are presented, which implement special forms of evaluation or extend the strategy language while preserving its advantages.
△ Less
Submitted 15 January, 2024;
originally announced January 2024.
-
Simulating and model checking membrane systems using strategies in Maude
Authors:
Rubén Rubio,
Narciso Martí-Oliet,
Isabel Pita,
Alberto Verdejo
Abstract:
Membrane systems are a biologically-inspired computational model based on the structure of biological cells and the way chemicals interact and traverse their membranes. Although their dynamics are described by rules, encoding membrane systems into rewriting logic is not straightforward due to its complex control mechanisms. Multiple alternatives have been proposed in the literature and implemented…
▽ More
Membrane systems are a biologically-inspired computational model based on the structure of biological cells and the way chemicals interact and traverse their membranes. Although their dynamics are described by rules, encoding membrane systems into rewriting logic is not straightforward due to its complex control mechanisms. Multiple alternatives have been proposed in the literature and implemented in the Maude specification language. The recent release of the Maude strategy language and its associated strategy-aware model checker allow specifying these systems more easily, so that they become executable and verifiable for free. An easily-extensible interactive environment transforms membrane specifications into rewrite theories controlled by appropriate strategies, and allows simulating and verifying membrane computations by means of them.
△ Less
Submitted 15 January, 2024;
originally announced January 2024.
-
Strategies, model checking and branching-time properties in Maude
Authors:
Rubén Rubio,
Narciso Martí-Oliet,
Isabel Pita,
Alberto Verdejo
Abstract:
Rewriting logic and its implementation Maude are a natural and expressive framework for the specification of concurrent systems and logics. Its nondeterministic local transformations are described by rewriting rules, which can be controlled at a higher level using a builtin strategy language added to Maude~3. This specification resource would not be of much interest without tools to analyze their…
▽ More
Rewriting logic and its implementation Maude are a natural and expressive framework for the specification of concurrent systems and logics. Its nondeterministic local transformations are described by rewriting rules, which can be controlled at a higher level using a builtin strategy language added to Maude~3. This specification resource would not be of much interest without tools to analyze their models, so in a previous work, we extended the Maude LTL model checker to verify strategy-controlled systems. In this paper, CTL* and $μ$-calculus are added to the repertoire of supported logics, after discussing which adaptations are needed for branching-time properties. The new extension relies on some external model checkers that are exposed the Maude models through general and efficient connections, profitable for future extensions and further applications. The performance of these model checkers is compared.
△ Less
Submitted 15 January, 2024;
originally announced January 2024.
-
Model checking strategy-controlled systems in rewriting logic
Authors:
Rubén Rubio,
Narciso Martí-Oliet,
Isabel Pita,
Alberto Verdejo
Abstract:
Rewriting logic and its implementation Maude are an expressive framework for the formal specification and verification of software and other kinds of systems. Concurrency is naturally represented by nondeterministic local transformations produced by the application of rewriting rules over algebraic terms in an equational theory. Some aspects of the global behavior of the systems or additional cons…
▽ More
Rewriting logic and its implementation Maude are an expressive framework for the formal specification and verification of software and other kinds of systems. Concurrency is naturally represented by nondeterministic local transformations produced by the application of rewriting rules over algebraic terms in an equational theory. Some aspects of the global behavior of the systems or additional constraints sometimes require restricting this nondeterminism. Rewriting strategies are used as a higher-level and modular resource to cleanly capture these requirements, which can be easily expressed in Maude with an integrated strategy language. However, strategy-aware specifications cannot be verified with the builtin LTL model checker, making strategies less useful and attractive.
In this paper, we discuss model checking for strategy-controlled systems, and present a strategy-aware extension of the Maude LTL model checker. The expressivity of the strategy language is discussed in relation to model checking, the model checker is illustrated with multiple application examples, and its performance is compared.
△ Less
Submitted 15 January, 2024;
originally announced January 2024.
-
Efficient Normalization of Linear Temporal Logic
Authors:
Javier Esparza,
Rubén Rubio,
Salomon Sickert
Abstract:
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F}\, \varphi_i \vee \mathbf{F}\mathbf{G}\, ψ_i $, where $\varphi_i$ and $ψ_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this resu…
▽ More
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F}\, \varphi_i \vee \mathbf{F}\mathbf{G}\, ψ_i $, where $\varphi_i$ and $ψ_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalization procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present direct and purely syntactic normalization procedures for LTL, yielding a normal form very similar to the one by Chang, Manna, and Pnueli, that exhibit only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalizes the formula, translates it into a special very weak alternating automaton, and applies a simple determinization procedure, valid only for these special automata.
△ Less
Submitted 27 February, 2024; v1 submitted 19 October, 2023;
originally announced October 2023.
-
A Simple Rewrite System for the Normalization of Linear Temporal Logic
Authors:
Javier Esparza,
Ruben Rubio,
Salomon Sickert
Abstract:
In the mid 80s, Lichtenstein, Pnueli, and Zuck showed that every formula of Past LTL (the extension of Linear Temporal Logic with past operators) is equivalent to a conjunction of formulas of the form $\mathbf{G}\mathbf{F} \varphi \vee \mathbf{F}\mathbf{G} ψ$, where $\varphi$ and $ψ$ contain only past operators. Some years later, Chang, Manna, and Pnueli derived a similar normal form for LTL. Both…
▽ More
In the mid 80s, Lichtenstein, Pnueli, and Zuck showed that every formula of Past LTL (the extension of Linear Temporal Logic with past operators) is equivalent to a conjunction of formulas of the form $\mathbf{G}\mathbf{F} \varphi \vee \mathbf{F}\mathbf{G} ψ$, where $\varphi$ and $ψ$ contain only past operators. Some years later, Chang, Manna, and Pnueli derived a similar normal form for LTL. Both normalization procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. In 2020, Sickert and Esparza presented a direct and purely syntactic normalization procedure for LTL yielding a normal form similar to the one by Chang, Manna, and Pnueli, with a single exponential blow-up, and applied it to the problem of constructing a succinct deterministic $ω$-automaton for a given formula. However, their procedure had exponential time complexity in the best case. In particular, it does not perform better for formulas that are almost in normal form. In this paper we present an alternative normalization procedure based on a simple set of rewrite rules.
△ Less
Submitted 18 April, 2023;
originally announced April 2023.
-
Framework para Caracterizar Fake News en Terminos de Emociones
Authors:
Luis Rojas Rubio,
Claudio Meneses Villegas
Abstract:
Social networks have become one of the main information channels for human beings due to the immediate and social interactivity they offer, allowing in some cases to publish what each user considers relevant. This has brought with it the generation of false news or Fake News, publications that only seek to generate uncertainty, misinformation or skew the opinion of readers. It has been shown that…
▽ More
Social networks have become one of the main information channels for human beings due to the immediate and social interactivity they offer, allowing in some cases to publish what each user considers relevant. This has brought with it the generation of false news or Fake News, publications that only seek to generate uncertainty, misinformation or skew the opinion of readers. It has been shown that the human being is not capable of fully identifying whether an article is really a fact or a Fake News, due to this it is that models arise that seek to characterize and identify articles based on data mining and machine learning. This article proposes a three-layer framework, the main objective of which is to characterize the emotions present in Fake News and to be a tool for future work that identifies the emotional state and intentional state of the public.
△ Less
Submitted 13 December, 2021;
originally announced December 2021.
-
Robust Federated Learning for execution time-based device model identification under label-flipping attack
Authors:
Pedro Miguel Sánchez Sánchez,
Alberto Huertas Celdrán,
José Rafael Buendía Rubio,
Gérôme Bovet,
Gregorio Martínez Pérez
Abstract:
The computing device deployment explosion experienced in recent years, motivated by the advances of technologies such as Internet-of-Things (IoT) and 5G, has led to a global scenario with increasing cybersecurity risks and threats. Among them, device spoofing and impersonation cyberattacks stand out due to their impact and, usually, low complexity required to be launched. To solve this issue, seve…
▽ More
The computing device deployment explosion experienced in recent years, motivated by the advances of technologies such as Internet-of-Things (IoT) and 5G, has led to a global scenario with increasing cybersecurity risks and threats. Among them, device spoofing and impersonation cyberattacks stand out due to their impact and, usually, low complexity required to be launched. To solve this issue, several solutions have emerged to identify device models and types based on the combination of behavioral fingerprinting and Machine/Deep Learning (ML/DL) techniques. However, these solutions are not appropriated for scenarios where data privacy and protection is a must, as they require data centralization for processing. In this context, newer approaches such as Federated Learning (FL) have not been fully explored yet, especially when malicious clients are present in the scenario setup. The present work analyzes and compares the device model identification performance of a centralized DL model with an FL one while using execution time-based events. For experimental purposes, a dataset containing execution-time features of 55 Raspberry Pis belonging to four different models has been collected and published. Using this dataset, the proposed solution achieved 0.9999 accuracy in both setups, centralized and federated, showing no performance decrease while preserving data privacy. Later, the impact of a label-flipping attack during the federated model training is evaluated, using several aggregation mechanisms as countermeasure. Zeno and coordinate-wise median aggregation show the best performance, although their performance greatly degrades when the percentage of fully malicious clients (all training samples poisoned) grows over 50%.
△ Less
Submitted 29 November, 2021;
originally announced November 2021.
-
A Comparison of Humanoid Robot Simulators: A Quantitative Approach
Authors:
Angel Ayala,
Francisco Cruz,
Diego Campos,
Rodrigo Rubio,
Bruno Fernandes,
Richard Dazeley
Abstract:
Research on humanoid robotic systems involves a considerable amount of computational resources, not only for the involved design but also for its development and subsequent implementation. For robotic systems to be implemented in real-world scenarios, in several situations, it is preferred to develop and test them under controlled environments in order to reduce the risk of errors and unexpected b…
▽ More
Research on humanoid robotic systems involves a considerable amount of computational resources, not only for the involved design but also for its development and subsequent implementation. For robotic systems to be implemented in real-world scenarios, in several situations, it is preferred to develop and test them under controlled environments in order to reduce the risk of errors and unexpected behavior. In this regard, a more accessible and efficient alternative is to implement the environment using robotic simulation tools. This paper presents a quantitative comparison of Gazebo, Webots, and V-REP, three simulators widely used by the research community to develop robotic systems. To compare the performance of these three simulators, elements such as CPU, memory footprint, and disk access are used to measure and compare them to each other. In order to measure the use of resources, each simulator executes 20 times a robotic scenario composed by a NAO robot that must navigate to a goal position avoiding a specific obstacle. In general terms, our results show that Webots is the simulator with the lowest use of resources, followed by V-REP, which has advantages over Gazebo, mainly because of the CPU use.
△ Less
Submitted 11 August, 2020;
originally announced August 2020.
-
Leveraging Energy Saving Capabilities of Current EEE Interfaces via Pre-Coalescing
Authors:
Miguel Rodríguez Pérez,
Sergio Herrería Alonso,
Raúl F. Rodríguez Rubio,
José Carlos López Ardao
Abstract:
The low power idle mode implemented by Energy Efficient Ethernet (EEE) allows network interfaces to save up to 90% of their nominal energy consumption when idling. There is an ample body of research that recommends the use of frame coalescing algorithms---that enter the low power mode as soon as there is no more traffic waiting to be sent, and delay the exit from this mode until there is an accept…
▽ More
The low power idle mode implemented by Energy Efficient Ethernet (EEE) allows network interfaces to save up to 90% of their nominal energy consumption when idling. There is an ample body of research that recommends the use of frame coalescing algorithms---that enter the low power mode as soon as there is no more traffic waiting to be sent, and delay the exit from this mode until there is an acceptable amount of traffic queued---to minimize energy usage while maintaining an acceptable performance. However, EEE capable hardware from several manufactures delays the entrance to the low power mode for a considerable amount of time (hysteresis). In this paper we augment existing EEE energy models to account for the hysteresis delay and show that, using the configuration ranges provided by manufacturers, most existing EEE networking devices are unable to obtain significant energy savings. To improve their energy efficiency, we propose to implement frame coalescing directly at traffic sources, before reaching the network interface. We also derive the optimum coalescing parameters to obtain a given target energy consumption at the EEE device when its configuration parameters are known in advance.
△ Less
Submitted 6 June, 2020; v1 submitted 27 May, 2020;
originally announced May 2020.
-
Programming and Symbolic Computation in Maude
Authors:
Francisco Durán,
Steven Eker,
Santiago Escobar,
Narciso Martí-Oliet,
José Meseguer,
Rubén Rubio,
Carolyn Talcott
Abstract:
Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurr…
▽ More
Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurrent systems and for increasing the power of formal tools. We present several new symbolic features of Maude that enhance formal reasoning about Maude programs and the effectiveness of formal tools. They include: (i) very general unification modulo user-definable equational theories, and (ii) symbolic reachability analysis of concurrent systems using narrowing. The paper does not focus just on symbolic features: it also describes several other new Maude features, including: (iii) Maude's strategy language for controlling rewriting, and (iv) external objects that allow flexible interaction of Maude object-based concurrent systems with the external world. In particular, meta-interpreters are external objects encapsulating Maude interpreters that can interact with many other objects. To make the paper self-contained and give a reasonably complete language overview, we also review the basic Maude features for equational rewriting and rewriting with rules, Maude programming of concurrent object systems, and reflection. Furthermore, we include many examples illustrating all the Maude notions and features described in the paper.
△ Less
Submitted 18 October, 2019;
originally announced October 2019.
-
Unirational fields of transcendence degree one and functional decomposition
Authors:
Jaime Gutierrez,
Rosario Rubio,
David Sevilla
Abstract:
In this paper we present an algorithm to compute all unirational fields of transcendence degree one containing a given finite set of multivariate rational functions. In particular, we provide an algorithm to decompose a multivariate rational function f of the form f=g(h), where g is a univariate rational function and h a multivariate one.
In this paper we present an algorithm to compute all unirational fields of transcendence degree one containing a given finite set of multivariate rational functions. In particular, we provide an algorithm to decompose a multivariate rational function f of the form f=g(h), where g is a univariate rational function and h a multivariate one.
△ Less
Submitted 15 May, 2008;
originally announced May 2008.
-
Computing the fixing group of a rational function
Authors:
Jaime Gutierrez,
Rosario Rubio,
David Sevilla
Abstract:
Let G=Aut_K (K(x)) be the Galois group of the transcendental degree one pure field extension K(x)/K. In this paper we describe polynomial time algorithms for computing the field Fix(H) fixed by a subgroup H < G and for computing the fixing group G_f of a rational function f in K(x).
Let G=Aut_K (K(x)) be the Galois group of the transcendental degree one pure field extension K(x)/K. In this paper we describe polynomial time algorithms for computing the field Fix(H) fixed by a subgroup H < G and for computing the fixing group G_f of a rational function f in K(x).
△ Less
Submitted 15 May, 2008;
originally announced May 2008.
