Showing 1–50 of 142 results for author: Filho, L

ESBMC-Python: A Bounded Model Checker for Python Programs

Authors: Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho, Youcheng Sun, Lucas C. Cordeiro

Abstract: This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this… ▽ More This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification. △ Less

Submitted 3 July, 2024; originally announced July 2024.

Usefulness of Quantum Entanglement for Enhancing Precision in Frequency Estimation

Authors: Marco A. Rodríguez-García, Ruynet L. de Matos Filho, Pablo Barberis-Blostein

Abstract: We investigate strategies for reaching the ultimate limit on the precision of frequency estimation when the number of probes used in each run of the experiment is fixed. That limit is set by the quantum Cramér-Rao bound (QCRB), which predicts that the use of maximally entangled probes enhances the estimation precision, when compared with the use of independent probes. However, the bound is only ac… ▽ More We investigate strategies for reaching the ultimate limit on the precision of frequency estimation when the number of probes used in each run of the experiment is fixed. That limit is set by the quantum Cramér-Rao bound (QCRB), which predicts that the use of maximally entangled probes enhances the estimation precision, when compared with the use of independent probes. However, the bound is only achievable if the statistical model used in the estimation remains identifiable throughout the procedure. This in turn sets different limits on the maximal sensing time used in each run of the estimation procedure, when entangled and independent probes are used. When those constraints are taken into account, one can show that, when the total number of probes and the total duration of the estimation process are counted as fixed resources, the use of entangled probes is, in fact, disadvantageous when compared with the use of independent probes. In order to counteract the limitations imposed on the sensing time by the requirement of identifiability of the statistical model, we propose a time-adaptive strategy, in which the sensing time is adequately increased at each step of the estimation process, calculate an attainable error bound for the strategy and discuss how to optimally choose its parameters in order to minimize that bound. We show that the proposed strategy leads to much better scaling of the estimation uncertainty with the total number of probes and the total sensing time than the traditional fixed-sensing-time strategy. We also show that, when the total number of probes and the total sensing time are counted as resources, independent probes and maximally entangled ones have now the same performance, in contrast to the non-adaptive strategy, where the use of independent is more advantageous than the use of maximally entangled ones. △ Less

Submitted 10 May, 2024; originally announced May 2024.

Comments: 15 pages

Sharp conditions for energy balance in two-dimensional incompressible ideal flow with external force

Authors: Fabian **, Samuel Lanthaler, Milton C. Lopes Filho, Helena J. Nussenzveig Lopes

Abstract: Smooth solutions of the forced incompressible Euler equations satisfy an energy balance, where the rate-of-change in time of the kinetic energy equals the work done by the force per unit time. Interesting phenomena such as turbulence are closely linked with rough solutions which may exhibit {\it inviscid dissipation}, or, in other words, for which energy balance does not hold. This article provi… ▽ More Smooth solutions of the forced incompressible Euler equations satisfy an energy balance, where the rate-of-change in time of the kinetic energy equals the work done by the force per unit time. Interesting phenomena such as turbulence are closely linked with rough solutions which may exhibit {\it inviscid dissipation}, or, in other words, for which energy balance does not hold. This article provides a characterization of energy balance for physically realizable weak solutions of the forced incompressible Euler equations, i.e. solutions which are obtained in the limit of vanishing viscosity. More precisely, we show that, in the two-dimensional periodic setting, strong convergence of the zero-viscosity limit is both necessary and sufficient for energy balance of the limiting solution, under suitable conditions on the external force. As a consequence, we prove energy balance for a general class of solutions with initial vorticity belonging to rearrangement-invariant spaces, and going beyond Onsager's critical regularity. △ Less

Submitted 18 April, 2024; originally announced April 2024.

MSC Class: 35Q31; 35Q30; 76D05; 76B99; 76F99

Thermal Casimir effect for a Dirac field on flat space with a nontrivial circular boundary condition

Authors: Joás Venâncio, Lameque Filho, Herondy Mota, Azadeh Mohammadi

Abstract: This work investigates the thermal Casimir effect associated with a massive spinor field defined on a four-dimensional flat space with a circularly compactified spatial dimension whose periodicity is oriented along a vector in $xy$-plane. We employ the generalized zeta function method to establish a finite definition for the vacuum free energy density. This definition conveniently separates into t… ▽ More This work investigates the thermal Casimir effect associated with a massive spinor field defined on a four-dimensional flat space with a circularly compactified spatial dimension whose periodicity is oriented along a vector in $xy$-plane. We employ the generalized zeta function method to establish a finite definition for the vacuum free energy density. This definition conveniently separates into the zero-temperature Casimir energy density and additional terms accounting for temperature corrections. The structure of existing divergences is analyzed from the asymptotic behavior of the spinor heat kernel function and removed in the renormalization by subtracting scheme. The only non-null heat coefficient is the one associated with the Euclidean divergence. We also address the need for a finite renormalization to treat the ambiguity in the zeta function regularization prescription \text{associated} with this Euclidean heat kernel coefficient and ensure that the renormalization procedure is unique. The high- and low-temperature asymptotic limits are also explored. In particular, we explicitly show that free energy density lacks a classical limit at high temperatures, and the entropy density agrees with the Nernst heat theorem at low temperatures. △ Less

Submitted 8 April, 2024; originally announced April 2024.

A Review on the Analysis and Optimal Control of Chemotaxis-Consumption Models

Authors: André Luiz Corrêa Vianna Filho, Francisco Guillén-González

Abstract: In the present review we focus on the chemotaxis-consumption model $\partial_t u - Δu = - \nabla \cdot (u \nabla v)$ and $\partial_t v - Δv = - u^s v$ in $(0,T) \times Ω$, for any fixed $s \geq 1$, endowed with isolated boundary conditions and nonnegative initial conditions, where $(u,v)$ model cell density and chemical signal concentration. Our objective is to present an overview of the related l… ▽ More In the present review we focus on the chemotaxis-consumption model $\partial_t u - Δu = - \nabla \cdot (u \nabla v)$ and $\partial_t v - Δv = - u^s v$ in $(0,T) \times Ω$, for any fixed $s \geq 1$, endowed with isolated boundary conditions and nonnegative initial conditions, where $(u,v)$ model cell density and chemical signal concentration. Our objective is to present an overview of the related literature and latest results on the aforementioned model concerning the following three distinct research lines we have obtained in [12,24-26]: the mathematical analysis, the numerical analysis and the related optimal control theory with a bilinear control acting on the chemical equation. △ Less

Submitted 9 February, 2024; originally announced February 2024.

MSC Class: 35A01; 35Q92; 65M12; 49J20; 49K20; 92C17

Towards a process-based approach to consciousness and collapse in quantum mechanics

Authors: Raoni Arroyo, Lauro de Matos Nunes Filho, Frederik Moreira dos Santos

Abstract: According to a particular interpretation of quantum mechanics, the causal role of human consciousness in the measuring process is called upon to solve a foundational problem called the "measurement problem". Traditionally, this interpretation is tied up with the metaphysics of substance dualism. As such, this interpretation of quantum mechanics inherits the dualist's mind-body problem. Our working… ▽ More According to a particular interpretation of quantum mechanics, the causal role of human consciousness in the measuring process is called upon to solve a foundational problem called the "measurement problem". Traditionally, this interpretation is tied up with the metaphysics of substance dualism. As such, this interpretation of quantum mechanics inherits the dualist's mind-body problem. Our working hypothesis is that a process-based approach to the consciousness causes collapse interpretation (CCCI) -- leaning on Whitehead's solution to the mind-body problem -- offers a better metaphysical understanding of consciousness and its role in interpreting quantum mechanics. This article is the kickoff for such a research program in the metaphysics of science. △ Less

Submitted 6 February, 2024; originally announced February 2024.

Comments: Forthcoming in Manuscrito vol. 47, n.1, 2024. Special issue: "Scientific Process Ontology and Metaphysics". Url: https://www.scielo.br/j/man/i/2024.v47n1

Improved regularity and analyticity of Cannone-Karch solutions of the three-dimensional Navier-Stokes equations on the torus

Authors: David M. Ambrose, Milton C. Lopes Filho, Helena J. Nussenzveig Lopes

Abstract: We consider the three-dimensional Navier-Stokes equations, with initial data having second derivatives in the space of pseudomeasures. Solutions of this system with such data have been shown to exist previously by Cannone and Karch. As the Navier-Stokes equations are a parabolic system, the solutions gain regularity at positive times. We demonstrate an improved gain of regularity at positive times… ▽ More We consider the three-dimensional Navier-Stokes equations, with initial data having second derivatives in the space of pseudomeasures. Solutions of this system with such data have been shown to exist previously by Cannone and Karch. As the Navier-Stokes equations are a parabolic system, the solutions gain regularity at positive times. We demonstrate an improved gain of regularity at positive times as compared to that demonstrated by Cannone and Karch. We further demonstrate that the solutions are analytic at all positive times, with lower bounds given for the radius of analyticity. △ Less

Submitted 1 February, 2024; originally announced February 2024.

Comments: 14 pages

MSC Class: 76D05 35B65 35K45 76D03

Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking

Authors: Janislley Oliveira de Sousa, Bruno Carvalho de Farias, Thales Araujo da Silva, Eddie Batista de Lima Filho, Lucas C. Cordeiro

Abstract: Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an app… ▽ More Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an approach struggles to scale up and verify extensive code bases. Consequently, we have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker. In particular, we pre-process input source-code files and guide the respective model checker to explore them systematically. Moreover, the proposed scheme includes a function-wise prioritization strategy, which readily provides results for code entities according to a scale of importance. Experimental results using a real implementation of the proposed methodology show that it can efficiently verify large software systems. Besides, it presented low peak memory allocation when executed. We have evaluated our approach by verifying twelve popular open-source C projects, where we have found real software vulnerabilities that their developers confirmed. △ Less

Submitted 9 November, 2023; originally announced November 2023.

Comments: 27 pages, submitted to STTT journal

Quantum advantage of time-reversed ancilla-based metrology of absorption parameters

Authors: Jiaxuan Wang, Ruynet. L. de Matos Filho, Girish S. Agarwal, Luiz Davidovich

Abstract: Quantum estimation of parameters defining open-system dynamics may be enhanced by using ancillas that are entangled with the probe but are not submitted to the dynamics. Here we consider the important problem of estimation of transmission of light by a sample, with losses due to absorption and scattering. We show, through the determination of the quantum Fisher information, that the ancilla strate… ▽ More Quantum estimation of parameters defining open-system dynamics may be enhanced by using ancillas that are entangled with the probe but are not submitted to the dynamics. Here we consider the important problem of estimation of transmission of light by a sample, with losses due to absorption and scattering. We show, through the determination of the quantum Fisher information, that the ancilla strategy leads to the best possible precision in single-mode estimation, the one obtained for a Fock state input, through joint photon-counting of probe and ancilla, which are modes of a bimodal squeezed state produced by an optical parametric amplifier. This proposal overcomes the challenge of producing and detecting high photon-number Fock states, and it is quite robust against additional noise: we show that it is immune to phase noise and the precision does not change if the incoming state gets disentangled. Furthermore, the quantum gain is still present under moderate photon losses of the input beams. We also discuss an alternative to joint photon counting, which is readily implementable with present technology, and approaches the quantum Fisher information result for weak absorption, even with moderate photons losses of the input beams before the sample is probed: a time-reversal procedure, placing the sample between two optical parametric amplifiers, with the second undoing the squeezing produced by the first one. The precision of estimation of the loss parameter is obtained from the average outgoing total photon number and its variance. In both procedures, the state of the probe and the detection procedure are independent of the value of the parameter. △ Less

Submitted 6 December, 2023; v1 submitted 9 October, 2023; originally announced October 2023.

Comments: 14 pages, 7 figures

Report number: Phys. Rev. Research 6, 013034

Existence and analyticity of solutions of the Kuramoto-Sivashinsky equation with singular data

Authors: David M. Ambrose, Milton C. Lopes Filho, Helena J. Nussenzveig Lopes

Abstract: We prove existence of solutions to the Kuramoto-Sivashinsky equation with low-regularity data, in function spaces based on the Wiener algebra and in pseudomeasure spaces. In any spatial dimension, we allow the data to have its antiderivative in the Wiener algebra. In one spatial dimension, we also allow data which is in a pseudomeasure space of negative order. In two spatial dimensions, we also al… ▽ More We prove existence of solutions to the Kuramoto-Sivashinsky equation with low-regularity data, in function spaces based on the Wiener algebra and in pseudomeasure spaces. In any spatial dimension, we allow the data to have its antiderivative in the Wiener algebra. In one spatial dimension, we also allow data which is in a pseudomeasure space of negative order. In two spatial dimensions, we also allow data which is in a pseudomeasure space one derivative more regular than in the one-dimensional case. In the course of carrying out the existence arguments, we show a parabolic gain of regularity of the solutions as compared to the data. Subsequently, we show that the solutions are in fact analytic at any positive time in the interval of existence. △ Less

Submitted 15 August, 2023; originally announced August 2023.

Comments: 26 pages

Noncommutative Derivation of the Planck's Radiation Law

Authors: M. A. De Andrade, L. G. Ferreira Filho, C. Neves

Abstract: The Planck's radiation law for the blackbody radiation spectrum was capable to explain the experimentally-measured blackbody spectrum. In order to get this result, Planck proposed his radiation law in a two-fold way: 1) by an \textit{ad hoc} modification of the assumed connection between energy and entropy for thermal radiation; 2) by assuming that the calculation of the entropy of an oscillator i… ▽ More The Planck's radiation law for the blackbody radiation spectrum was capable to explain the experimentally-measured blackbody spectrum. In order to get this result, Planck proposed his radiation law in a two-fold way: 1) by an \textit{ad hoc} modification of the assumed connection between energy and entropy for thermal radiation; 2) by assuming that the calculation of the entropy of an oscillator in thermal equilibrium with radiation is carried out by discrete units of energy. As a consequence, the energy quantization, linear in frequency, was thus introduced into physics. However, the energy quantization of the simple harmonic oscillator was originally postulated by Planck in an incomplete way, i.e., the ground state energy was not assumed to be null. Of course, this issue has been solved in different ways over time. Despite of this, we propose an alternative way to fix this issue by describing harmonic oscillators at noncommutative(NC) framework, where the non-null ground state energy naturally arises as a NC contribution. With this approach, the Planck's quantum theory is updated and, consequently, becomes compatible with the quantum mechanics inaugurated in 1925. △ Less

Submitted 4 April, 2023; originally announced April 2023.

Journal ref: Revista Brasileira De Ensino De Física, 45, e20230093 (2023)

Large time behavior for the 3D Navier-Stokes with Navier boundary conditions

Authors: James P. Kelliher, Christophe Lacave, Milton C. Lopes Filho, Helena J. Nussenzveig Lopes, Edriss S. Titi

Abstract: We study the three-dimensional incompressible Navier-Stokes equations in a smooth bounded domain $Ω$ with initial velocity $u_0$ square-integrable, divergence-free and tangent to $\partial Ω$. We supplement the equations with the Navier friction boundary conditions $u \cdot n = 0$ and $[(2Su)n + αu]_{\rm tang} = 0$, where $n$ is the unit exterior normal to $\partial Ω$, $Su = (Du + (Du)^t)/2$,… ▽ More We study the three-dimensional incompressible Navier-Stokes equations in a smooth bounded domain $Ω$ with initial velocity $u_0$ square-integrable, divergence-free and tangent to $\partial Ω$. We supplement the equations with the Navier friction boundary conditions $u \cdot n = 0$ and $[(2Su)n + αu]_{\rm tang} = 0$, where $n$ is the unit exterior normal to $\partial Ω$, $Su = (Du + (Du)^t)/2$, $α\in C^0(\partialΩ)$ is the boundary friction coefficient and $[\cdot]_{\rm tang}$ is the projection of its argument onto the tangent space of $\partial Ω$. We prove global existence of a weak Leray-type solution to the resulting initial-boundary value problem and exponential decay in energy norm of these solutions when friction is positive. We also prove exponential decay if friction is non-negative and the domain is not a solid of revolution. In addition, in the frictionless case $α= 0$, we prove convergence of the solution to a steady rigid rotation, if the domain is a solid of revolution. We use the Galerkin method for existence, Poincaré-type inequalities, with suitable adaptations to account for the differential geometry of the boundary, and a global-in-time, integral Gronwall-type inequality. △ Less

Submitted 27 March, 2024; v1 submitted 6 March, 2023; originally announced March 2023.

GraphLED: A graph-based approach to process and visualise linked engineering documents

Authors: Vanessa Telles da Silva, Lucas de Angelo Martins Ribeiro, Willian Borges de Lemos, Sílvia Silva da Costa Botelho, Nelson Lopes Duarte Filho, Marcelo Rita Pias

Abstract: The architecture, engineering and construction (AEC) sector extensively uses documents supporting product and process development. As part of this, organisations should handle big data of hundreds, or even thousands, of technical documents strongly linked together, including CAD design of industrial plants, equipment purchase orders, quality certificates, and part material analysis. However, analy… ▽ More The architecture, engineering and construction (AEC) sector extensively uses documents supporting product and process development. As part of this, organisations should handle big data of hundreds, or even thousands, of technical documents strongly linked together, including CAD design of industrial plants, equipment purchase orders, quality certificates, and part material analysis. However, analysing such records is daunting for users because it gets complicated to sift through hundreds of documents to establish valuable relationships. This paper addresses how knowledge extracted from linked engineering documents contributes to industrial digitalisation under IT/OT convergence. The proposed GraphLED is a system tasked with data processing, graph-based modelling, and colourful visualisation of related documents. The graph-based approach ensures an improved understanding of linked information because the graph structure offers a promising tool to model the underlying data properties of engineering documents. Preliminary system validation indicates quality improvements are possible in the OCR-based data (85.9% of ambiguous text data removed). This work has the potential to benefit the industry by improving the reliability and resilience of industrial production systems through automated summaries of large quantities of documents and their linkage. △ Less

Submitted 15 February, 2023; originally announced February 2023.

An optimal control problem subject to strong solutions of chemotaxis-consumption models

Authors: Francisco Guillén-González, André Luiz Corrêa Vianna Filho

Abstract: We consider a bilinear optimal control problem associated to the following chemotaxis-consumption model in a bounded domain $Ω\subset \mathbb{R}^3$ during a time interval $(0,T)$: $$\partial_t u - Δu = - \nabla \cdot (u \nabla v), \quad \partial_t v - Δv = - u^s v + f v 1_{Ω_c},$$ with $s \geq 1$, endowed with isolated boundary conditions and initial conditions for $(u,v)$, $u$ being the cell dens… ▽ More We consider a bilinear optimal control problem associated to the following chemotaxis-consumption model in a bounded domain $Ω\subset \mathbb{R}^3$ during a time interval $(0,T)$: $$\partial_t u - Δu = - \nabla \cdot (u \nabla v), \quad \partial_t v - Δv = - u^s v + f v 1_{Ω_c},$$ with $s \geq 1$, endowed with isolated boundary conditions and initial conditions for $(u,v)$, $u$ being the cell density, $v$ the chemical concentration and $f$ the bilinear control acting in a subdomain $Ω_c \subset Ω$. The existence of weak solutions $(u,v)$ to this model given $f \in L^q((0,T) \times Ω)$, for some $q > 5/2$, has been proved in [F. Guillén-González and A. L. Corrêa Vianna Filho, Optimal Control Related to Weak Solutions of a Chemotaxis-Consumption Model, arXiv:2211.14612, 2022]. In this paper, we study a related optimal control problem in the strong solution setting. First, imposing the regularity criterion $u ^s \in L^q((0,T) \times Ω)$ ($q > 5/2$) for a given weak solution, we prove existence and uniqueness of global-in-time strong solutions. Then, the existence of a global optimal solution can be deduced. Finally, using a Lagrange multipliers theorem, we establish first order optimality conditions for any local optimal solution, proving existence, uniqueness and regularity of the associated Lagrange multipliers. △ Less

Submitted 25 October, 2023; v1 submitted 15 February, 2023; originally announced February 2023.

MSC Class: 49J20; 49K20; 49N60; 35Q92; 92C17

Generalized Uncertainty Principle for Entangled States of Two Identical Particles

Authors: K. C. Lemos Filho, B. B. Dilem, R. O. Francisco, J. C. Fabris, J. A. Nogueira

Abstract: In this work we determine the consequences of the quantum entanglement of a system of two identical particles when a generalized uncertainty principle (GUP) is considered. GUP's are usually associated with the existence of a minimal length. We focus on the main GUP's (KMM, ADV, Pedram and Nouicer) and then we determine the minimal uncertainties in position induced by those modified GUP's. Our resu… ▽ More In this work we determine the consequences of the quantum entanglement of a system of two identical particles when a generalized uncertainty principle (GUP) is considered. GUP's are usually associated with the existence of a minimal length. We focus on the main GUP's (KMM, ADV, Pedram and Nouicer) and then we determine the minimal uncertainties in position induced by those modified GUP's. Our results point out that the minimal uncertainty is reduced by half of its usual value independently of the GUP employed. This implies that the minimal length is also reduced by half. On the other hand, it is generally expected that the minimal length must not depend on physical system. We overcome this apparent paradox by realizing that the entangled system is composed by two particles so that an effective parameter related to the minimal length must be employed. △ Less

Submitted 5 July, 2024; v1 submitted 27 January, 2023; originally announced January 2023.

Comments: Accepted for publication in the International Journal of Modern Physics D (IJMPD)

A reappraisal of the principle of equivalent time based on physicochemical methods

Authors: Matheus Rufino, Arnaldo Luis Lixandrão Filho, Sandro Guedes

Abstract: The main feature of the Fission-Track Thermochronology is its ability to infer the thermal histories of mineral samples in regions of interest for geological studies. The ingredients that make the thermal history inference possible are the annealing models, which capture the annealing kinetics of fission tracks for isothermal heating experiments, and the Principle of Equivalent Time (PET), which a… ▽ More The main feature of the Fission-Track Thermochronology is its ability to infer the thermal histories of mineral samples in regions of interest for geological studies. The ingredients that make the thermal history inference possible are the annealing models, which capture the annealing kinetics of fission tracks for isothermal heating experiments, and the Principle of Equivalent Time (PET), which allows the application of the annealing models to variable temperatures. It turns out that the PET only applies to specific types of annealing models describing single activation energy annealing mechanisms (parallel models). However, the PET has been extensively applied to models related to multiple activation energy mechanisms (fanning models). This procedure is an approximation that has been overlooked due to the lack of a suitable alternative. To deal with this difficult, a formalism, based on physicochemical techniques, that allows to quantify the effects of annealing on the fission tracks for variable temperatures, is developed. It is independent of the annealing mechanism and, therefore, is applicable to any annealing model. In the cases in which the PET is valid, parallel models, the proposed method and the PET predict the same degrees of annealing. However, deviations appear when the methods are applied to the fanning models, with the PET underestimating annealing effects. The consequences for the inference of thermal histories are discussed. △ Less

Submitted 6 January, 2023; originally announced January 2023.

Comments: 16 pages, 4 figures, 3 tables. Manuscript submitted to Chemical Geology

Optimal control related to weak solutions of a chemotaxis-consumption model

Authors: Francisco Guillén-González, André Luiz Corrêa Vianna Filho

Abstract: In the present work we investigate an optimal control problem related to the following chemotaxis-consumption model in a bounded domain $Ω\subset \mathbb{R}^3$: $$\partial_t u - Δu = - \nabla \cdot (u \nabla v), \quad \partial_t v - Δv = - u^s v + f \,v\, 1_{Ω_c},$$ with $s \geq 1$, endowed with isolated boundary conditions and initial conditions for $(u,v)$, being $u$ the cell density, $v$ th… ▽ More In the present work we investigate an optimal control problem related to the following chemotaxis-consumption model in a bounded domain $Ω\subset \mathbb{R}^3$: $$\partial_t u - Δu = - \nabla \cdot (u \nabla v), \quad \partial_t v - Δv = - u^s v + f \,v\, 1_{Ω_c},$$ with $s \geq 1$, endowed with isolated boundary conditions and initial conditions for $(u,v)$, being $u$ the cell density, $v$ the chemical concentration and $f$ the control acting in the $v$-equation through the bilinear term $f \,v\, 1_{Ω_c}$, in a subdomain $Ω_c \subset Ω$. We address the existence of optimal control restricted to a weak solution setting, where, in particular, uniqueness of state $(u,v)$ given a control $f$ is not clear. Then by considering weak solutions satisfying an adequate energy inequality, we prove the existence of optimal control subject to uniformly bounded controls. Finally, we discuss the relation between the considered control problem and two other related ones, where the existence of optimal solution can not be proved. △ Less

Submitted 9 February, 2024; v1 submitted 26 November, 2022; originally announced November 2022.

MSC Class: 35K51; 35Q92; 49J20; 92C17

Fractal signature as a rotational modulation and stellar noise classifier based on the active Kepler stars

Authors: Paulo Cleber Farias da Silva Filho, Jose Ribamar Dantas Silveira Junior, Bricio Warney de Freitas Alves, Fernando Jose Silva Lima Filho, Vitor Marcelo Belo Ferreira, Luiz Daniel Alves Rios, Thiago de Melo Santiago, Daniel Brito de Freitas

Abstract: In this study, we report on the analysis of 701 stars in a solar vicinity defined in three categories namely subsolar, solar, and supersolar with rotation periods between 1 and 70 days, based on rotational modulation signatures inferred from time series from the Kepler mission's Public Archives. In our analysis, we performed an initial selection based on the rotation period and position in the per… ▽ More In this study, we report on the analysis of 701 stars in a solar vicinity defined in three categories namely subsolar, solar, and supersolar with rotation periods between 1 and 70 days, based on rotational modulation signatures inferred from time series from the Kepler mission's Public Archives. In our analysis, we performed an initial selection based on the rotation period and position in the period-H diagram, where H denotes the Hurst exponent extracted from fractal analysis. To refine our analysis, we applied a fractal approach known as the R/S method, taking into account the fluctuations of the features associated with photometric modulation at different time intervals and the fractality traces that are present in the time series of our sample. In this sense, we computed the so-called Hurst exponent for the referred stars and found that it can provide a strong discriminant of rotational modulation and background noise behavior, going beyond what can be achieved with solely the rotation period itself. Furthermore, our results emphasize that the rotation period of stars is scaled by the exponent H which increases following the increase in the rotation period. Finally, our approach suggests that the referred exponent may be a powerful rotational modulation and noise classifier. △ Less

Submitted 4 November, 2022; originally announced November 2022.

Comments: 18 pages, 5 figures, submitted to BJD

Multifractal charactarization as a function of timescale in the light curves with planetary signal observed by the kepler mission

Authors: F. J. S. Lima Filho, V. M. B. Ferreira, P. C. F. da Silva Filho, F. O. da Silva Gomes, B. W. de Freitas Alves, S. G. A. Barbosa, T. de Melo Santiago, D. B. de Freitas

Abstract: Astrophysical data, in the domains of time, involve a wide range of stellar variability phenomena, among them the magnetic activity of the order of a few hours until the signature of an extra-solar planet which can cover a scale of time of a few days until tens of years. Numerous instruments are being developed to detect Earth-sized exoplanets. Exoplanets with this dimension challenge scientific i… ▽ More Astrophysical data, in the domains of time, involve a wide range of stellar variability phenomena, among them the magnetic activity of the order of a few hours until the signature of an extra-solar planet which can cover a scale of time of a few days until tens of years. Numerous instruments are being developed to detect Earth-sized exoplanets. Exoplanets with this dimension challenge scientific instrumentation and the field of research in the data processing. In this context, our study offers a powerful framework to explain dynamical properties as a function of timescale in light curves with the planetary signal. For that, we selected the stellar target Kepler-30 to test our methods and procedures. In this sense, we investigate the multifractal behavior of the Kepler-30 system composed of a sun-like star with a rotation period of ~16 days and three planets with masses between 2 Earth and 2.5 Jupiter masses. Furthermore, this system has an orbital period varying from 29 to 143 days and orbits almost coplanar. This system is highly interesting because starspots dynamics are strongly affected by the passing of a planet in front of the star. We used about 1600 days of high-precision photometry collected by the Kepler mission to investigate the quasi-periodic variation caused by the rotation of the star and the effect of spot evolution as a function of timescale. We applied indexes extract from multifractal analysis to model the flux rotational modulation induced by active regions. Our results that stellar flux variations in Kepler-30 star caused by rotational modulation can be replicated in detail with just four recent-known multifractal indexes. These indexes will greatly simplify spot modelling of current TESS and future PLATO data. △ Less

Submitted 9 September, 2022; originally announced September 2022.

Comments: 20 pages, 1 table, 5 figures (submitted to BJD)

Convergence of a time discrete scheme for a chemotaxis-consumption model

Authors: Francisco Guillén-González, André Luiz Corrêa Vianna Filho

Abstract: In the present work we propose and study a time discrete scheme for the following chemotaxis-consumption model (for any $s\ge 1$), $$ \partial_t u - Δu = - \nabla \cdot (u \nabla v), \quad \partial_t v - Δv = - u^s v \quad \hbox{in $(0,T)\times Ω$,}$$ endowed with isolated boundary conditions and initial conditions, where $(u,v)… ▽ More In the present work we propose and study a time discrete scheme for the following chemotaxis-consumption model (for any $s\ge 1$), $$ \partial_t u - Δu = - \nabla \cdot (u \nabla v), \quad \partial_t v - Δv = - u^s v \quad \hbox{in $(0,T)\times Ω$,}$$ endowed with isolated boundary conditions and initial conditions, where $(u,v)$ model cell density and chemical signal concentration. The proposed scheme is defined via a reformulation of the model, using the auxiliary variable $z = \sqrt{v + α^2}$ combined with a Backward Euler scheme for the $(u,z)$-problem and a upper truncation of $u$ in the nonlinear chemotaxis and consumption terms. Then, two different ways of retrieving an approximation for the function $v$ are provided. We prove the existence of solution to the time discrete scheme and establish uniform in time \emph{a priori} estimates, yielding the convergence of the scheme towards a weak solution $(u,v)$ of the chemotaxis-consumption model. △ Less

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

MSC Class: 35K51; 35K55; 35Q92; 65M12; 92C17

Existence and analyticity of the Lei-Lin solution of the Navier-Stokes equations on the torus

Authors: D. M. Ambrose, M. C. Lopes Filho, H. J. Nussenzveig Lopes

Abstract: Lei and Lin have recently given a proof of a global mild solution of the three-dimensional Navier-Stokes equations in function spaces based on the Wiener algebra. An alternative proof of existence of these solutions was then developed by Bae, and this new proof allowed for an estimate of the radius of analyticity of the solutions at positive times. We adapt the Bae proof to prove existence of the… ▽ More Lei and Lin have recently given a proof of a global mild solution of the three-dimensional Navier-Stokes equations in function spaces based on the Wiener algebra. An alternative proof of existence of these solutions was then developed by Bae, and this new proof allowed for an estimate of the radius of analyticity of the solutions at positive times. We adapt the Bae proof to prove existence of the Lei-Lin solution in the spatially periodic setting, finding an improved bound for the radius of analyticity in this case. △ Less

Submitted 24 May, 2022; originally announced May 2022.

Comments: 15 pages

MSC Class: 35Q30; 76D03; 35A20

Double-GEM based thermal neutron detector prototype

Authors: L. A. Serra Filho, R. Felix dos Santos, G. G. A. de Souza, M. M. M. Paulino, F. A. Souza, M. Moralles, H. Natal da Luz, M. Bregant, M. G. Munhoz, Chung-Chuan Lai, Carina Höglund, Per-Olof Svensson, Linda Robinson, Richard Hall-Wilton

Abstract: The Helium-3 shortage and the growing interest in neutron science constitute a driving factor in develo** new neutron detection technologies. In this work, we report the development of a double-GEM detector prototype that uses a $^{10}$B$_4$C layer as a neutron converter material. GEANT4 simulations were performed predicting an efficiency of 3.14(10) %, agreeing within 2.7 $σ$ with the experimen… ▽ More The Helium-3 shortage and the growing interest in neutron science constitute a driving factor in develo** new neutron detection technologies. In this work, we report the development of a double-GEM detector prototype that uses a $^{10}$B$_4$C layer as a neutron converter material. GEANT4 simulations were performed predicting an efficiency of 3.14(10) %, agreeing within 2.7 $σ$ with the experimental and analytic detection efficiencies obtained by the detector when tested in a 41.8 meV thermal neutron beam. The detector is position sensitive, equipped with a 256+256 strip readout connected to resistive chains, and achieves a spatial resolution better than 3 mm. The gain stability over time was also measured with a fluctuation of about 0.2 %h$^{-1}$ of the signal amplitude. A simple data acquisition with only 5 electronic channels is sufficient to operate this detector. △ Less

Submitted 19 July, 2022; v1 submitted 14 May, 2022; originally announced May 2022.

Comments: Prepared for submission to JINST

Journal ref: JINST 17 P09018 (2022)

Development of a fast simulator for GEM-based neutron detectors

Authors: R. Felix dos Santos, M. G. Munhoz, M. Moralles, L. A. Serra Filho, M. Bregant, F. A. Souza

Abstract: Gas Electron Multiplier (GEM)-based detectors using a layer of 10B as a neutron converter is becoming popular for thermal neutron detection. A common strategy to simulate this kind of detector is based on two frameworks: Geant4 and Garfield++. The first one provides the simulation of the nuclear interaction between neutrons and the 10B layer, while the second allows the simulation of the interacti… ▽ More Gas Electron Multiplier (GEM)-based detectors using a layer of 10B as a neutron converter is becoming popular for thermal neutron detection. A common strategy to simulate this kind of detector is based on two frameworks: Geant4 and Garfield++. The first one provides the simulation of the nuclear interaction between neutrons and the 10B layer, while the second allows the simulation of the interaction of the reaction products with the detector gas leading to the ionization and excitation of the gas molecules. Given the high ionizing power of these nuclear reaction products, a full simulation is very time consuming and must be optimized to become viable. In this work, we present a strategy to develop a fast simulator based on these two frameworks that will allow us to generate enough data for a proper evaluation of the expected performance and optimization of this kind of detector. We will show the first results obtained with this tool concentrating on its validation and performance. △ Less

Submitted 24 April, 2022; originally announced May 2022.

Comments: Submitted to Journal of Physics: Conference Series. Proceedings of the International Conference on Technology and Instrumentation in Particle Physics (TIPP 2021)

Uniform in time solutions for a chemotaxis with potential consumption model

Authors: A. L. Corrêa Vianna Filho, Francisco Guillén-González

Abstract: In this work we investigate the following chemo-attraction with consumption model in bounded domains of \, $\mathbb{R}^N$ ($N=1,2,3$): $$ \partial_t u - Δu = - \nabla \cdot (u \nabla v), \quad \partial_t v - Δv = - u^s v $$ where $s\ge 1$, endowed with isolated boundary conditions and initial conditions for $(u,v)$. The main novelty in the model is the nonlinear potential consumption term… ▽ More In this work we investigate the following chemo-attraction with consumption model in bounded domains of \, $\mathbb{R}^N$ ($N=1,2,3$): $$ \partial_t u - Δu = - \nabla \cdot (u \nabla v), \quad \partial_t v - Δv = - u^s v $$ where $s\ge 1$, endowed with isolated boundary conditions and initial conditions for $(u,v)$. The main novelty in the model is the nonlinear potential consumption term $u^sv$. Through the convergence of solutions of an adequate truncated model, two main results are established; existence of uniform in time weak solutions in $3D$ domains, and uniqueness and regularity in $2D$ (or $1D$) domains. Both results are proved imposing minimal regularity assumptions on the boundary of the domain. △ Less

Submitted 16 February, 2023; v1 submitted 18 April, 2022; originally announced April 2022.

MSC Class: 35A01; 35Q92; 35K51; 35K55; 92C17

The incompressible $α$--Euler equations in the exterior of a vanishing disk

Authors: Adriana Valentina Busuioc, Dragos Iftimie, Milton Lopes Filho, Helena Nussenzveig Lopes

Abstract: In this article we consider the $α$--Euler equations in the exterior of a small fixed disk of radius $ε$. We assume that the initial potential vorticity is compactly supported and independent of $ε$, and that the circulation of the unfiltered velocity on the boundary of the disk does not depend on $ε$. We prove that the solution of this problem converges, as $ε\to 0$, to the solution of a modified… ▽ More In this article we consider the $α$--Euler equations in the exterior of a small fixed disk of radius $ε$. We assume that the initial potential vorticity is compactly supported and independent of $ε$, and that the circulation of the unfiltered velocity on the boundary of the disk does not depend on $ε$. We prove that the solution of this problem converges, as $ε\to 0$, to the solution of a modified $α$--Euler equation in the full plane where an additional Dirac located at the center of the disk is imposed in the potential vorticity. △ Less

Submitted 28 March, 2022; originally announced March 2022.

Comments: 23 pages

MSC Class: 35Q35; 76B03

Standing Forest Coin (SFC)

Authors: Marcelo de A. Borges, Guido L. de S. Filho, Cicero Inacio da Silva, Anderson M. P. Barros, Raul V. B. J. Britto, Nivaldo M. de C. Junior, Daniel F. L. de Souza

Abstract: This article describes a proposal to create a digital currency that allows the decentralized collection of resources directed to initiatives and activities that aim to protect the Brazilian Amazon ecosystem by using blockchain and digital contracts. In addition to the digital currency, the goal is to design a smart contract based in oracles to ensure credibility and security for investors and dono… ▽ More This article describes a proposal to create a digital currency that allows the decentralized collection of resources directed to initiatives and activities that aim to protect the Brazilian Amazon ecosystem by using blockchain and digital contracts. In addition to the digital currency, the goal is to design a smart contract based in oracles to ensure credibility and security for investors and donors of financial resources invested in projects within the Standing Forest Coin (SFC - standingforest.org). △ Less

Submitted 4 March, 2022; originally announced March 2022.

Comments: in Portuguese

MSC Class: 58-04 ACM Class: J.7

ESBMC-Solidity: An SMT-Based Model Checker for Solidity Smart Contracts

Authors: Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho, Lucas C. Cordeiro

Abstract: Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which… ▽ More Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool, and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0. △ Less

Submitted 25 November, 2021; originally announced November 2021.

Comments: 4 pages, 2 figures, 2 tables

ACM Class: D.2.4; F.3.1

QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking

Authors: Xidan Song, Edoardo Manino, Luiz Sena, Erickson Alves, Eddie de Lima Filho, Iury Bessa, Mikel Lujan, Lucas Cordeiro

Abstract: QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The novel support for quantization is achieved by employing state-of-the-art software model checking (SMC) techniques. It translates the implementation of neural networks to a decidable fragment of first-order logic based o… ▽ More QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The novel support for quantization is achieved by employing state-of-the-art software model checking (SMC) techniques. It translates the implementation of neural networks to a decidable fragment of first-order logic based on satisfiability modulo theories (SMT). The effects of fixed- and floating-point operations are represented through direct implementations given a hardware-determined precision. Furthermore, QNNVerifier allows to specify bespoke safety properties and verify the resulting model with different verification strategies (incremental and k-induction) and SMT solvers. Finally, QNNVerifier is the first tool that combines invariant inference via interval analysis and discretization of non-linear activation functions to speed up the verification of neural networks by orders of magnitude. A video presentation of QNNVerifier is available at https://youtu.be/7jMgOL41zTY △ Less

Submitted 25 November, 2021; originally announced November 2021.

Comments: Submitted to the Demo track of the ICSE 2022 conference

Monte-Carlo simulations of evolving rotational distributions of low-mass stars in young open clusters. Testing the influence of initial conditions

Authors: Maria Jaqueline Vasconcelos, Jérôme Bouvier, Florian Gallet, Edson A. Luz Filho

Abstract: The rotational evolution of a young stellar population can give informations about the rotation pattern of more evolved clusters. Combined with rotational period values of thousands of young stars and theoretical propositions about the redistribution and loss of stellar angular momentum, it allows us to trace the rotational history of stars according to their mass. We want to investigate how inter… ▽ More The rotational evolution of a young stellar population can give informations about the rotation pattern of more evolved clusters. Combined with rotational period values of thousands of young stars and theoretical propositions about the redistribution and loss of stellar angular momentum, it allows us to trace the rotational history of stars according to their mass. We want to investigate how internal and environmental changes on single stars can change the rotational evolution of a young stellar population. We run Monte Carlo simulations of a young cluster composed by solar mass stars of 0.5, 0.8 and 1.0 M$_\odot$ from 1 to 550 Myr taking into account observational and theoretical parameters. In order to compare our results with the observations we run Kolmogorov-Smirnov tests. Our standard model is able to reproduce some clusters younger than h Per and marginally M37, which is 550 Myr old. Varying the disk fraction or the initial period distribution did not improve the results. However, when we run a model with a finer mass grid the Pleiades can be also reproduced. Changing the initial mass distribution to be similar to the empirical ONC mass function also gives good results. Modeling the evolution of a young synthetic cluster from pre-main sequence to early main sequence considering physical mechanisms of extraction and exchange of angular momentum can not be achieved successfully for all clusters for which we have enough rotational data. Clusters of about the same age present different rotational behaviors due perhaps to differences in their initial conditions. △ Less

Submitted 17 November, 2021; originally announced November 2021.

Comments: 14 pages, 13 figures, 6 tables. Accepted for publication on Monthly Notices of the Royal Astronomical Society (MNRAS)

Performance evaluation in the reconstruction of 2D images of computed tomography using massively parallel programming CUDA

Authors: Alexssandro Ferreira Cordeiro, Pedro Luiz de Paula Filho, Hamilton Pereira da Silva, Arnaldo Candido Junior, Edresson Casanova, Jandrei Sartori Spancerski

Abstract: Analysis of processing time and similarity of images generated between CPU and GPU architectures and sequential and parallel programming. For image processing a computer with AMD FX-8350 processor and an Nvidia GTX 960 Maxwell GPU was used, along with the CUDAFY library and the programming language C\# with the IDE Visual studio. The results of the comparisons indicate that the form of sequential… ▽ More Analysis of processing time and similarity of images generated between CPU and GPU architectures and sequential and parallel programming. For image processing a computer with AMD FX-8350 processor and an Nvidia GTX 960 Maxwell GPU was used, along with the CUDAFY library and the programming language C\# with the IDE Visual studio. The results of the comparisons indicate that the form of sequential programming in a CPU generates reliable images at a high custom of time when compared to the forms of parallel programming in CPU and GPU. While parallel programming generates faster results, but with increased noise in the reconstructed image. For data types float a GPU obtained best result with average time equivalent to 1/3 of the processor, however the data is of type double the parallel CPU approach obtained the best performance. For the float data type, the GPU had the best average time performance, while for the double data type the best average time performance was for the parallel approach CPU. Regarding image quality, the sequential approach obtained similar outputs, while the parallel approaches generated noise in their outputs. △ Less

Submitted 5 September, 2021; originally announced September 2021.

Localization transition induced by programmable disorder

Authors: Jaime L. C. da C. Filho, Zoe Gonzalez Izquierdo, Andreia Saguia, Tameem Albash, Itay Hen, Marcelo S. Sarandy

Abstract: We investigate the occurrence of many-body localization (MBL) on a spin-1/2 transverse-field Ising model defined on a Chimera connectivity graph with random exchange interactions and longitudinal fields. We observe a transition from an ergodic phase to a non-thermal phase for individual energy eigenstates induced by a critical disorder strength for the Ising parameters. Our result follows from the… ▽ More We investigate the occurrence of many-body localization (MBL) on a spin-1/2 transverse-field Ising model defined on a Chimera connectivity graph with random exchange interactions and longitudinal fields. We observe a transition from an ergodic phase to a non-thermal phase for individual energy eigenstates induced by a critical disorder strength for the Ising parameters. Our result follows from the analysis of both the mean half-system block entanglement and the energy level statistics. We identify the critical point associated with this transition using the maximum variance of the block entanglement over the disorder ensemble as a function of the disorder strength. The calculated energy density phase diagram shows the existence of a mobility edge in the energy spectrum. In terms of the energy level statistics, the system changes from the Gaussian orthogonal ensemble for weak disorder to a Poisson distribution limit for strong randomness, which implies localization behavior. We then realize the time-independent disordered Ising Hamiltonian experimentally using a reverse annealing quench-pause-quench protocol on a D-Wave 2000Q programmable quantum annealer. We characterize the transition from the thermal to the localized phase through magnetization measurements at the end of the annealing dynamics, and the results are compatible with our theoretical prediction for the critical point. However, the same behavior can be reproduced using a classical spin-vector Monte Carlo simulation, which suggests that genuine quantum signatures of the phase transition remain out of reach using this experimental platform and protocol. △ Less

Submitted 1 April, 2022; v1 submitted 15 August, 2021; originally announced August 2021.

Comments: 13 pages, 18 figures

Journal ref: Phys. Rev. B 105, 134201 (2022)

Energy balance for forced two-dimensional incompressible ideal fluid flow

Authors: Milton Lopes Filho, Helena Nussenzveig Lopes

Abstract: In [Commun Math Phys 348(1), 129-143, 2016], Cheskidov et al. proved that physically realizable weak solutions of the incompressible 2D Euler equations on a torus conserve kinetic energy. Physically realizable weak solutions are those that can be obtained as limits of vanishing viscosity. The key hypothesis was boundedness of the initial vorticity in $L^p$, $p>1$. In this work we extend their resu… ▽ More In [Commun Math Phys 348(1), 129-143, 2016], Cheskidov et al. proved that physically realizable weak solutions of the incompressible 2D Euler equations on a torus conserve kinetic energy. Physically realizable weak solutions are those that can be obtained as limits of vanishing viscosity. The key hypothesis was boundedness of the initial vorticity in $L^p$, $p>1$. In this work we extend their result, by adding forcing to the flow. △ Less

Submitted 28 July, 2021; originally announced July 2021.

MSC Class: 35Q30; 35Q31; 76B03; 76D05

Verifying Quantized Neural Networks using SMT-Based Model Checking

Authors: Luiz Sena, Xidan Song, Erickson Alves, Iury Bessa, Edoardo Manino, Lucas Cordeiro, Eddie de Lima Filho

Abstract: Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety-critical applications, including autonomous cars and medical diagnosis. However, concerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks. These concerns are amplified when ANNs are deployed on restricted system, which limit the precision of m… ▽ More Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety-critical applications, including autonomous cars and medical diagnosis. However, concerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks. These concerns are amplified when ANNs are deployed on restricted system, which limit the precision of mathematical operations and thus introduce additional quantization errors. Here, we develop and evaluate a novel symbolic verification framework using software model checking (SMC) and satisfiability modulo theories (SMT) to check for vulnerabilities in ANNs. More specifically, we propose several ANN-related optimizations for SMC, including invariant inference via interval analysis, slicing, expression simplifications, and discretization of non-linear activation functions. With this verification framework, we can provide formal guarantees on the safe behavior of ANNs implemented both in floating- and fixed-point arithmetic. In this regard, our verification approach was able to verify and produce adversarial examples for $52$ test cases spanning image classification and general machine learning applications. Furthermore, for small- to medium-sized ANN, our approach completes most of its verification runs in minutes. Moreover, in contrast to most state-of-the-art methods, our approach is not restricted to specific choices regarding activation functions and non-quantized representations. Our experiments show that our approach can analyze larger ANN implementations and substantially reduce the verification time compared to state-of-the-art techniques that use SMT solving. △ Less

Submitted 16 September, 2021; v1 submitted 10 June, 2021; originally announced June 2021.

Comments: Changes with respect to the previous version: improved explanation of our methodology in Section 3; improved and extended experimental evaluation in Section 4; added comparison with the state of the art in Section 4.5

Flow through three-dimensional self-affine fractures

Authors: H. J. Seybold, H. A. Carmona, F. A. Leandro Filho, A. D. Araújo, F. Nepomuceno Filho, J. S. Andrade Jr

Abstract: We investigate through numerical simulations of the Navier-Stokes equations the influence of the surface roughness on the fluid flow through fracture joints. Using the Hurst exponent $H$ to characterize the roughness of the self-affine surfaces that constitute the fracture, our analysis reveal the important interplay between geometry and inertia on the flow. Precisely, for low values of Reynolds n… ▽ More We investigate through numerical simulations of the Navier-Stokes equations the influence of the surface roughness on the fluid flow through fracture joints. Using the Hurst exponent $H$ to characterize the roughness of the self-affine surfaces that constitute the fracture, our analysis reveal the important interplay between geometry and inertia on the flow. Precisely, for low values of Reynolds numbers Re, we use Darcy's law to quantify the hydraulic resistance $G$ of the fracture and show that its dependence on $H$ can be explained in terms of a simple geometrical model for the tortuosity $τ$ of the channel. At sufficiently high values of Re, when inertial effects become relevant, our results reveal that nonlinear corrections up to third-order to Darcy's law are aproximately proportional to $H$. These results imply that the resistance $G$ to the flow follows a universal behavior by simply rescaling it in terms of the fracture resistivity and using an effective Reynolds number, namely, Re/$H$. Our results also reveal the presence of quasi-one-dimensional channeling, even considering the absence of shear displacement between upper and lower surfaces of the self-affine fracture. △ Less

Submitted 8 June, 2020; originally announced June 2020.

Comments: 10 pages, 8 figures

Journal ref: Phys. Rev. Fluids 5, 104101 (2020)

Robust interferometric sensing using two-photon interference

Authors: G. H. Aguilar, R. S. Piera, P. L. Saldanha, R. L. de Matos Filho, S. P. Walborn

Abstract: Precise measurement of the angular deviation of an object is a common task in science and technology. Many methods use light for this purpose. Some of these exploit interference effects to achieve technological advantages, such as amplification effects, or simplified measurement devices. However, all of these schemes require phase stability to be useful. Here we show theoretically and experimental… ▽ More Precise measurement of the angular deviation of an object is a common task in science and technology. Many methods use light for this purpose. Some of these exploit interference effects to achieve technological advantages, such as amplification effects, or simplified measurement devices. However, all of these schemes require phase stability to be useful. Here we show theoretically and experimentally that this drawback can be lifted by utilizing two-photon interference, which is known to be less sensitive to phase fluctuations. Our results show that non-classical interference can provide a path towards robust interferometric sensing, allowing for increased metrological precision in the presence of phase noise. △ Less

Submitted 10 July, 2020; v1 submitted 11 May, 2020; originally announced May 2020.

Comments: Accepted at Physical Review Applied

Journal ref: Phys. Rev. Applied 14, 024028 (2020)

Interferometric sensing of the tilt angle of a Gaussian beam

Authors: S. P. Walborn, G. H. Aguilar, P. L. Saldanha, L. Davidovich, R. L. de Matos Filho

Abstract: We investigate interferometric techniques to estimate the deflection angle of an optical beam and compare them to the direct detection of the beam deflection. We show that quantum metrology methods lead to a unifying treatment for both single photons and classical fields. Using the Fisher information to assess the precision limits of the interferometric schemes, we show that the precision can be i… ▽ More We investigate interferometric techniques to estimate the deflection angle of an optical beam and compare them to the direct detection of the beam deflection. We show that quantum metrology methods lead to a unifying treatment for both single photons and classical fields. Using the Fisher information to assess the precision limits of the interferometric schemes, we show that the precision can be increased by exploiting the initial transverse displacement of the beam. This gain, which is present for both Sagnac and Mach-Zehnder-like configurations, can be considerable when compared to non-interferometric methods. In addition to the fundamental increase in precision, the interferometric schemes have the technical advantage that (i) the precision limits can be saturated by a sole polarization measurement on the field, and that (ii) the detection system can be placed at any longitudinal position along the beam. We also consider position-dependent polarization measurements, and show that in this case the precision increases with the propagation distance, as well as the initial transverse displacement. △ Less

Submitted 7 May, 2020; originally announced May 2020.

Comments: Comments are welcome

Journal ref: Phys. Rev. Research 2, 033191 (2020)

wisardpkg -- A library for WiSARD-based models

Authors: Aluizio S. Lima Filho, Gabriel P. Guarisa, Leopoldo A. D. Lusquino Filho, Luiz F. R. Oliveira, Felipe M. G. Franca, Priscila M. V. Lima

Abstract: In order to facilitate the production of codes using WiSARD-based models, LabZero developed an ML library C++/Python called wisardpkg. This library is an MIT-licensed open-source package hosted on GitHub under the license. In order to facilitate the production of codes using WiSARD-based models, LabZero developed an ML library C++/Python called wisardpkg. This library is an MIT-licensed open-source package hosted on GitHub under the license. △ Less

Submitted 2 May, 2020; originally announced May 2020.

Comments: 9 pages, 2 figures

The limit $α\to 0$ of the $α$-Euler equations in the half plane with no-slip boundary conditions and vortex sheet initial data

Authors: A. V. Busuioc, D. Iftimie, M. C. Lopes Filho, H. J. Nussenzveig Lopes

Abstract: In this article we study the limit when $α\to 0$ of solutions to the $α$-Euler system in the half-plane, with no-slip boundary conditions, to weak solutions of the 2D incompressible Euler equations with non-negative initial vorticity in the space of bounded Radon measures in $H^{-1}$. This result extends the analysis done in arXiv:1611.05300 and arXiv:1403.5682. It requires a substantially distinc… ▽ More In this article we study the limit when $α\to 0$ of solutions to the $α$-Euler system in the half-plane, with no-slip boundary conditions, to weak solutions of the 2D incompressible Euler equations with non-negative initial vorticity in the space of bounded Radon measures in $H^{-1}$. This result extends the analysis done in arXiv:1611.05300 and arXiv:1403.5682. It requires a substantially distinct approach, analogous to that used for Delort's Theorem, and a new detailed investigation of the relation between (no-slip) filtered velocity and potential vorticity in the half-plane. △ Less

Submitted 23 February, 2020; originally announced February 2020.

The dynamics of the early universe in a model with radiation and a generalized Chaplygin gas

Authors: G. A. Monerat, C. G. M. Santos, G. Oliveira-Neto, E. V. Corrêa Silva, L. G. Ferreira Filho

Abstract: The early universe is modeled through the quantization of a Friedmann-Robertson-Walker model with positive curvature of the spatial hypersurfaces. In this model, the universe is filled by two fluids: radiation and a generalized Chaplygin gas. The quantization of this model is made following the prescriptions due to J. A. Wheeler and B. DeWitt. Using the Schutz's formalism, the time notion is recov… ▽ More The early universe is modeled through the quantization of a Friedmann-Robertson-Walker model with positive curvature of the spatial hypersurfaces. In this model, the universe is filled by two fluids: radiation and a generalized Chaplygin gas. The quantization of this model is made following the prescriptions due to J. A. Wheeler and B. DeWitt. Using the Schutz's formalism, the time notion is recovered and the Wheeler-DeWitt equation transforms into a time dependent Schrödinger equation, which rules the dynamics of the early universe, under the action of an effective potential $V_{eff}$. That potential, depends on three parameters. Depending on the values of these parameters, $V_{eff}$ may have two different shapes. $V_{eff}(a)$ may have the shape of a barrier or the shape of a well followed by a barrier. We solve, numerically, the appropriate time dependent Schrödinger equation and obtain the time evolution of an initial wave function, for both cases. These wave functions satisfy suitable boundary conditions. For both shapes of $V_{eff}$, we compute the tunneling probability, which is a function of the mean kinetic energy associated to the radiation energy $E_m$ and of the three parameters of the generalized Chaplygin gas: $α$, $A$ and $B$. The tunneling probabilities, for both shapes of $V_{eff}$, indicates that the universe should nucleate with the highest possible values of $E_m$, $α$, $A$ and $B$. Finally, we study the classical universe evolution after the wavefunction has tunneled $V_{eff}$. The calculations show that the universe may emerge from the Planck era in an inflationary phase. △ Less

Submitted 14 November, 2020; v1 submitted 5 February, 2020; originally announced February 2020.

Comments: In that new version, we removed a section and four figures. It has, now, 30 pages and 13 figures

Journal ref: The European Physical Journal Plus volume 136, Article number: 34 (2021)

Hard-core collisional dynamics in the hamiltonian mean-field model

Authors: Luciano Miranda Filho, Igor Melo, Annibal Figueiredo, Tarcisio Rocha Filho, L Filho, Yves Elskens

Abstract: We consider a modification of the well studied Hamiltonian Mean-Field model by introducing a hard-core point-like repulsive interaction and propose a numerical integration scheme to integrate numerically its dynamics. Our results show that the outcome of the initial violent relaxation is altered, and also that the phase-diagram is modified with a critical temperature at a higher value than in the… ▽ More We consider a modification of the well studied Hamiltonian Mean-Field model by introducing a hard-core point-like repulsive interaction and propose a numerical integration scheme to integrate numerically its dynamics. Our results show that the outcome of the initial violent relaxation is altered, and also that the phase-diagram is modified with a critical temperature at a higher value than in the non-collisional counterpart. △ Less

Submitted 23 April, 2020; v1 submitted 9 September, 2019; originally announced September 2019.

Comments: published in Communications in nonlinear science and num{é}riical simulations

Journal ref: Communications in Nonlinear Science and Numerical Simulation, Elsevier, 2020, 87, pp.105270

Error-run-time trade-off in the adiabatic approximation beyond scaling relations

Authors: M. R. Passos, M. M. Taddei, R. L. de Matos Filho

Abstract: The use of the adiabatic approximation in practical applications, as in adiabatic quantum computation, demands an assessment of the errors made in finite-time evolutions. Aiming at such scenarios, we derive bounds relating error and evolution time in the adiabatic approximation that go beyond typical scaling relations. Using the Adiabatic Perturbation Theory, we obtain leading-order expressions va… ▽ More The use of the adiabatic approximation in practical applications, as in adiabatic quantum computation, demands an assessment of the errors made in finite-time evolutions. Aiming at such scenarios, we derive bounds relating error and evolution time in the adiabatic approximation that go beyond typical scaling relations. Using the Adiabatic Perturbation Theory, we obtain leading-order expressions valid for long evolution time $T$, while explicitly determining the shortest time $T$ and the largest error $\varepsilon$ for which they are valid. In this validity regime, we can make clear and precise statements about the evolution time needed to reach a given error and vice-versa. As an example of practical importance, we apply these results to the adiabatic search, and obtain for the first time an error-run-time trade-off relation that fully reproduces the discrete-Grover-search scaling. We also pioneer the obtention of tight numerical values for $\varepsilon$ and $T$ under the error-reducing strategy ``boundary cancelation''. △ Less

Submitted 20 April, 2020; v1 submitted 8 July, 2019; originally announced July 2019.

Comments: Main text 16 pages, 26 pages total (with appendix), 3 figures

Journal ref: Annals of Physics 418, 168172 (2020)

Contribution of individual degrees of freedom to Lyapunov vectors in many-body systems

Authors: L Filho, M Amato, Y Elskens, T Rocha Filho

Abstract: We use the weight $δ$I, deduced from the estimation of Lyapunov vectors, in order to characterise regions in the kinetic (x, v) space with particles that most contribute to chaoticity. For the paradigmatic model, the cosine Hamiltonian mean field model, we show that this diagnostic highlights the vicinity of the separatrix, even when the latter hardly exists. We use the weight $δ$I, deduced from the estimation of Lyapunov vectors, in order to characterise regions in the kinetic (x, v) space with particles that most contribute to chaoticity. For the paradigmatic model, the cosine Hamiltonian mean field model, we show that this diagnostic highlights the vicinity of the separatrix, even when the latter hardly exists. △ Less

Submitted 22 February, 2019; originally announced February 2019.

Portfolio Theory, Information Theory and Tsallis Statistics

Authors: Marco A. S. Trindade, Sergio Floquet, Lourival M. S. Filho

Abstract: We developed a strategic of optimal portfolio based on information theory and Tsallis statistics. The growth rate of a stock market is defined by using $q$-deformed functions and we find that the wealth after n days with the optimal portfolio is given by a $q$-exponential function. In this context, the asymptotic optimality is investigated on causal portfolios, showing advantages of the optimal po… ▽ More We developed a strategic of optimal portfolio based on information theory and Tsallis statistics. The growth rate of a stock market is defined by using $q$-deformed functions and we find that the wealth after n days with the optimal portfolio is given by a $q$-exponential function. In this context, the asymptotic optimality is investigated on causal portfolios, showing advantages of the optimal portfolio over an arbitrary choice of causal portfolios. Finally, we apply the formulation in a small number of stocks in brazilian stock market $[B]^{3}$ and analyzed the results. △ Less

Submitted 22 October, 2019; v1 submitted 17 November, 2018; originally announced November 2018.

Comments: 17 pages

Vorticity measures and the inviscid limit

Authors: Peter Constantin, Milton Lopes Filho, Helena Nussenzveig Lopes, Vlad Vicol

Abstract: We consider a sequence of Leray-Hopf weak solutions of the 2D Navier-Stokes equations on a bounded domain, in the vanishing viscosity limit. We provide sufficient conditions on the associated vorticity measures, away from the boundary, which ensure that as the viscosity vanishes the sequence converges to a weak solution of the Euler equations. These assumptions are consistent with vortex sheet sol… ▽ More We consider a sequence of Leray-Hopf weak solutions of the 2D Navier-Stokes equations on a bounded domain, in the vanishing viscosity limit. We provide sufficient conditions on the associated vorticity measures, away from the boundary, which ensure that as the viscosity vanishes the sequence converges to a weak solution of the Euler equations. These assumptions are consistent with vortex sheet solutions of the Euler equations. △ Less

Submitted 10 September, 2018; originally announced September 2018.

Comments: 14 pages

The Nice Cube (Nice3) nanosatellite project

Authors: F. Millour, S. Ottogalli, M. Maamri, A. Stibbe, F. Ferrero, L. Rolland, S. Rebeyrolle, A. Marcotto, K. Agabi, M. Beaulieu, M. Benabdesselam, J. -B. Caillau, F. Cauneau, L. Deneire, F. Mady, D. Mary, A. Memin, G. Metris, J. -B. Pomet, O. Preis, R. Staraj, E. Ait Lachgar, D. Baltazar, B. Gao, M. Deroo , et al. (6 additional authors not shown)

Abstract: CubeSats are tiny satellites with increasing capabilities. They have been used for more than a decade by universities to train students on space technologies, in a hands-on project aiming at building, launching and operating a real satellite. Still today, one shortcoming of CubeSats is their poor ability to transmit large amounts of data to the ground. A possible way to overcome this limitation re… ▽ More CubeSats are tiny satellites with increasing capabilities. They have been used for more than a decade by universities to train students on space technologies, in a hands-on project aiming at building, launching and operating a real satellite. Still today, one shortcoming of CubeSats is their poor ability to transmit large amounts of data to the ground. A possible way to overcome this limitation relies on optical communications. Universite Cote d'Azur is studying the feasibility of a student's CubeSat whose main goal is to transmit data with an optical link to the ground at the moderate rate of 1 kb/s (or better). In this paper, we will present the current state of the project and its future developments. △ Less

Submitted 29 August, 2018; originally announced August 2018.

Comments: 12 pages, 4 figures, proceeding from the "complex days" workshop

Decimation analysis in the signal processing of current to detect broken bars in induction machine

Authors: J. S. Moreira, P. C. M. Lamim Filho, L. M. R. Baccarini, E. G. Nepomuceno, P. F. S. Guedes

Abstract: This paper presents a study on the reduction of the sampling frequency of the current signals of an induction motor, the reductions are performed by means time-decimation technique for digital signal processing. We have used the Fast Fourier Transform to obtain the fault signal spectrum of broken bars. The results have shown how the decimation technique significantly reduces the number of operatio… ▽ More This paper presents a study on the reduction of the sampling frequency of the current signals of an induction motor, the reductions are performed by means time-decimation technique for digital signal processing. We have used the Fast Fourier Transform to obtain the fault signal spectrum of broken bars. The results have shown how the decimation technique significantly reduces the number of operations and the time required to calculate the Fast Fourier Transform without loss of information. This approach provides a better performance of embedded systems for fault diagnosis based on characteristic of amplitude signal modulation. △ Less

Submitted 28 July, 2018; originally announced July 2018.

Comments: in Portuguese

Journal ref: CBA 2018 - XXII Congresso Brasileiro de Automatica, Joao Pessoa, p. 1-6

Liquid Argon test of the ARAPUCA device

Authors: E. Segreto, A. A. Machado, L. Paulucci, F. Marinho, D. Galante, S. Guedes, A. Fauth, V. Teixeira, B. Gelli, M. Reggiani-Guzzo, W. Araujo, C. Ambrósio, M. Bissiano, A. L. Lixandrão Filho

Abstract: The ARAPUCA is a novel concept for liquid argon scintillation light detection which has been proposed for the photon detection system of the Deep Underground Neutrino Experiment. The test in liquid argon of one of the first ARAPUCA prototypes is presented in this work, where the working principle is experimentally demonstrated. The prototype has an acceptance window of 9 cm$^2$ and is read-out by… ▽ More The ARAPUCA is a novel concept for liquid argon scintillation light detection which has been proposed for the photon detection system of the Deep Underground Neutrino Experiment. The test in liquid argon of one of the first ARAPUCA prototypes is presented in this work, where the working principle is experimentally demonstrated. The prototype has an acceptance window of 9 cm$^2$ and is read-out by a single SiPM with active area of 0.36 cm$^2$. Its global detection efficiency was estimated by exposing it to a $^{238}U$ $α$ source and to cosmic rays and was found to be 1.15\% $\pm$ 0.15\%, in good agreement with the prediction of a detailed Monte Carlo simulation of the device. Several other ARAPUCA prototypes of bigger dimensions and read-out by arrays of SiPMs have been built and are actually under test. In particular 32 ARAPUCA cells have been installed inside the protoDUNE detector, which is being assembled at CERN and will be operated in the second half of 2018. △ Less

Submitted 1 May, 2018; originally announced May 2018.

$^9$Be+$^{120}$Sn scattering at near-barrier energies within a four body model

Authors: A. Arazi, J. Casal, M. Rodríguez-Gallardo, J. M. Arias, R. Lichtenthäler Filho, D. Abriola, O. A. Capurro, M. A. Cardona, P. F. F. Carnelli, E. de Barbará, J. Fernández Niello, J. M. Figueira, L. Fimiani, D. Hojman, G. V. Martí, D. Martínez Heimman, A. J. Pacheco

Abstract: Cross sections for elastic and inelastic scattering of the weakly-bound $^9$Be nucleus on a $^{120}$Sn target have been measured at seven bombarding energies around and above the Coulomb barrier. The elastic angular distributions are analyzed with a four-body continuum-discretized coupled-channels (CDCC) calculation, which considers $^9$Be as a three-body projectile ($α$ + $α$ + n). An optical mod… ▽ More Cross sections for elastic and inelastic scattering of the weakly-bound $^9$Be nucleus on a $^{120}$Sn target have been measured at seven bombarding energies around and above the Coulomb barrier. The elastic angular distributions are analyzed with a four-body continuum-discretized coupled-channels (CDCC) calculation, which considers $^9$Be as a three-body projectile ($α$ + $α$ + n). An optical model analysis using the São Paulo potential is also shown for comparison. The CDCC analysis shows that the coupling to the continuum part of the spectrum is important for the agreement with experimental data even at energies around the Coulomb barrier, suggesting that breakup is an important process at low energies. At the highest incident energies, two inelastic peaks are observed at 1.19(5) and 2.41(5) MeV. Coupled-channels (CC) calculations using a rotational model confirm that the first inelastic peak corresponds to the excitation of the 2$_1^+$ state in $^{120}$Sn, while the second one likely corresponds to the excitation of the 3$_1^-$ state. △ Less

Submitted 2 April, 2018; originally announced April 2018.

Comments: 11 pages, 9 figures. Accepted as PRC

Journal ref: Phys. Rev. C 97, 044609 (2018)

Ion backflow studies with a triple-GEM stack with increasing hole pitch

Authors: H. Natal da Luz, P. Bhattacharya, L. A. S. Filho, L. E. F. M. França

Abstract: Gas Electron Multipliers have undergone a very consistent development since their invention in 1997. Their production procedures have been tuned in such a way that nowadays it is possible to produce foils with areas of the order of the square meter that can operate at a reasonable gain, uniform over large areas and with a good stability in what concerns electrical discharges. For the third run of… ▽ More Gas Electron Multipliers have undergone a very consistent development since their invention in 1997. Their production procedures have been tuned in such a way that nowadays it is possible to produce foils with areas of the order of the square meter that can operate at a reasonable gain, uniform over large areas and with a good stability in what concerns electrical discharges. For the third run of LHC, they will be included in the CMS and ALICE experiments after significant upgrades of the detectors, confirming that these structures are suitable for very large experiments. In the special case of Time Projection Chambers, the ion backflow and the energy resolution are sensitive issues that must be addressed and the GEM has shown to be able to deal with both of them. In this work, a stack of three GEMs with different pitches has been studied as a possible future approach for ion-backflow suppression to be used in TPCs and other detection concepts. With this approach, an ion backflow of 1 % with an energy resolution of 12 % at 5.9 keV has been achieved with the detector operating in an Ar/CO2 (90/10) mixture at a gain of ~ 2000. △ Less

Submitted 1 June, 2018; v1 submitted 25 March, 2018; originally announced March 2018.

Comments: 15 pages, 11 figures

Confinement of vorticity for the 2D Euler-alpha equations

Authors: David Ambrose, Milton Lopes Filho, Helena Nussenzveig Lopes

Abstract: In this article we consider weak solutions of the Euler-$α$ equations in the full plane. We take, as initial unfiltered vorticity, an arbitrary nonnegative, compactly supported, bounded Radon measure. Global well-posedness for the corresponding initial value problem is due M. Oliver and S. Shkoller. We show that, for all time, the support of the unfiltered vorticity is contained in a disk whose ra… ▽ More In this article we consider weak solutions of the Euler-$α$ equations in the full plane. We take, as initial unfiltered vorticity, an arbitrary nonnegative, compactly supported, bounded Radon measure. Global well-posedness for the corresponding initial value problem is due M. Oliver and S. Shkoller. We show that, for all time, the support of the unfiltered vorticity is contained in a disk whose radius grows no faster than $\mathcal{O}((t\log t)^{1/4})$. This result is an adaptation of the corresponding result for the incompressible 2D Euler equations with initial vorticity compactly supported, nonnegative, and $p$-th power integrable, $p>2$, due to D. Iftimie, T. Sideris and P. Gamblin and, independently, to Ph. Serfati. △ Less

Submitted 27 February, 2018; originally announced February 2018.

MSC Class: 35Q35; 35Q31