arXiv subjects

Carlos Varela

Publications and source records attributed to Carlos Varela.

8 recordsLinked to original sources

arXiv2026

Equational and Inductive Reasoning for Maude in Athena

In the rewriting logic framework, equational-based specifications are used to define deterministic functional behavior, abstract data types, and canonical representations of data. These specifications include a (possibly order-sorted) signature and equations interpreted modulo structural axioms, such as associativity, commutativity, and identity. While equational rewriting provides a powerful basis for execution and symbolic reasoning, it does not by itself offer native support for inductive or deductive reasoning. This paper presents maude2athena, a framework that systematically translates Maude's equational theories into Athena, a theorem proving language designed to support natural deduction proofs over many-sorted first-order logic specifications, including inductive reasoning, equational chaining, case-based reasoning, and proofs by contradiction. The translation supports induction-based reasoning modulo structural axioms with parametric induction rules; it faithfully encodes membership equational logic in a many-sorted setting without exponential blowup under reasonable conditions. This approach preserves the semantics of the original specification, while ensuring that the translation remains compact and amenable to deductive reasoning. This work helps bridge the gap between model checking and theorem proving, enabling formal verification efforts that can benefit from both of these approaches.

cs.LO↗

arXiv2026

Verification of Autonomous Systems with Optimal Controllers

This paper considers the problem of reachability analysis of control systems with optimal controllers, as a first step towards verifying the safety and correctness of such systems. Despite their appeal in guaranteeing task satisfaction through cost minimization, optimal controllers are often challenging to assure. In particular, as system dynamics grow in complexity, solving the resulting optimization problem may be difficult, especially given time and computation constraints on real platforms. Thus, it is essential to verify that, even if the optimal solution is not always found, such controllers still accomplish the high-level control objective. In this paper, we focus on gradient descent algorithms and design a reachability algorithm by treating gradient descent as a separate (digital) dynamical system, embedded in the original (physical) dynamical system, with controls as part of the state. We evaluate the feasibility of the proposed method on two control systems, a two-dimensional quadrotor and a cartpole.

eess.SY↗

arXiv2021

Formal Guarantees of Timely Progress for Distributed Knowledge Propagation

Autonomous air traffic management (ATM) operations for urban air mobility (UAM) will necessitate the use of distributed protocols for decentralized coordination between aircraft. As UAM operations are time-critical, it will be imperative to have formal guarantees of progress for the distributed protocols used in ATM. Under asynchronous settings, message transmission and processing delays are unbounded, making it impossible to provide deterministic bounds on the time required to make progress. We present an approach for formally guaranteeing timely progress in a Two-Phase Acknowledge distributed knowledge propagation protocol by probabilistically modeling the delays using theories of the Multicopy Two-Hop Relay protocol and the M/M/1 queue system. The guarantee states a probabilistic upper bound to the time for progress as a function of the probabilities of the total transmission and processing delays being less than two given values. We also showcase the development of a library of formal theories, that is tailored towards reasoning about timely progress in distributed protocols deployed in airborne networks, in the Athena proof assistant.

cs.DC↗

arXiv2021

An Algorithm for Reconstructing the Orphan Stream Progenitor with MilkyWay@home Volunteer Computing

We have developed a method for estimating the properties of the progenitor dwarf galaxy from the tidal stream of stars that were ripped from it as it fell into the Milky Way. In particular, we show that the mass and radial profile of a progenitor dwarf galaxy evolved along the orbit of the Orphan Stream, including the stellar and dark matter components, can be reconstructed from the distribution of stars in the tidal stream it produced. We use MilkyWay@home, a PetaFLOPS-scale distributed supercomputer, to optimize our dwarf galaxy parameters until we arrive at best-fit parameters. The algorithm fits the dark matter mass, dark matter radius, stellar mass, radial profile of stars, and orbital time. The parameters are recovered even though the dark matter component extends well past the half light radius of the dwarf galaxy progenitor, proving that we are able to extract information about the dark matter halos of dwarf galaxies from the tidal debris. Our simulations assumed that the Milky Way potential, dwarf galaxy orbit, and the form of the density model for the dwarf galaxy were known exactly; more work is required to evaluate the sources of systematic error in fitting real data. This method can be used to estimate the dark matter content in dwarf galaxies without the assumption of virial equilibrium that is required to estimate the mass using line-of-sight velocities. This demonstration is a first step towards building an infrastructure that will fit the Milky Way potential using multiple tidal streams.

astro-ph.GA↗

arXiv2018

A Manifesto for Future Generation Cloud Computing: Research Directions for the Next Decade

The Cloud computing paradigm has revolutionised the computer science horizon during the past decade and has enabled the emergence of computing as the fifth utility. It has captured significant attention of academia, industries, and government bodies. Now, it has emerged as the backbone of modern economy by offering subscription-based services anytime, anywhere following a pay-as-you-go model. This has instigated (1) shorter establishment times for start-ups, (2) creation of scalable global enterprise applications, (3) better cost-to-value associativity for scientific and high performance computing applications, and (4) different invocation/execution models for pervasive and ubiquitous applications. The recent technological developments and paradigms such as serverless computing, software-defined networking, Internet of Things, and processing at network edge are creating new opportunities for Cloud computing. However, they are also posing several new challenges and creating the need for new approaches and research strategies, as well as the re-evaluation of the models that were developed to address issues such as scalability, elasticity, reliability, security, sustainability, and application models. The proposed manifesto addresses them by identifying the major open challenges in Cloud computing, emerging trends, and impact areas. It then offers research directions for the next decade, thus helping in the realisation of Future Generation Cloud Computing.

cs.DC↗

arXiv2014

MilkyWay@home: Harnessing volunteer computers to constrain dark matter in the Milky Way

MilkyWay@home is a volunteer computing project that allows people from every country in the world to volunteer their otherwise idle processors to Milky Way research. Currently, more than 25,000 people (150,000 since November 9, 2007) contribute about half a PetaFLOPS of computing power to our project. We currently run two types of applications: one application fits the spatial density profile of tidal streams using statistical photometric parallax, and the other application finds the N-body simulation parameters that produce tidal streams that best match the measured density profile of known tidal streams. The stream fitting application is well developed and is producing published results. The Sagittarius dwarf leading tidal tail has been fit, and the algorithm is currently running on the trailing tidal tail and bifurcated pieces. We will soon have a self-consistent model for the density of the smooth component of the stellar halo and the largest tidal streams. The $N$-body application has been implemented for fitting dwarf galaxy progenitor properties only, and is in the testing stages. We use an Earth-Mover Distance method to measure goodness-of-fit for density of stars along the tidal stream. We will add additional spatial dimensions as well as kinematic measures in a piecemeal fashion, with the eventual goal of fitting the orbit and parameters of the Milky Way potential (and thus the density distribution of dark matter) using multiple tidal streams.

astro-ph.GA↗

arXiv2013

A Spatial Characterization of the Sagittarius Dwarf Galaxy Tidal Tails

We measure the spatial density of F turnoff stars in the Sagittarius dwarf tidal stream, from Sloan Digital Sky Survey (SDSS) data, using statistical photometric parallax. We find a set of continuous, consistent parameters that describe the leading Sgr stream's position, direction, and width for 15 stripes in the North Galactic Cap, and 3 stripes in the South Galactic Cap. We produce a catalog of stars that has the density characteristics of the dominant leading Sgr tidal stream that can be compared with simulations. We find that the width of the leading (North) tidal tail is consistent with recent triaxial and axisymmetric halo model simulations. The density along the stream is roughly consistent common disruption models in the North, but possibly not in the South. We explore the possibility that one or more of the dominant Sgr streams has been mis-identified, and that one or more of the `bifurcated' pieces is the real Sgr tidal tail, but we do not reach definite conclusions. If two dwarf progenitors are assumed, fits to the planes of the dominant and `bifurcated' tidal tails favor an association of the Sgr dwarf spheroidal galaxy with the dominant Southern stream and the `bifurcated' stream in the North. In the North Galactic Cap, the best fit Hernquist density profile for the smooth component of the stellar halo is oblate, with a flattening parameter q = 0.53, and a scale length of r_0 = 6.73. The Southern data for both the tidal debris and the smooth component of the stellar halo do not match the model fits to the North, although the stellar halo is still overwhelmingly oblate. Finally, we verify that we can reproduce the parameter fits on the asynchronous Milkyway@home volunteer computing platform.

astro-ph.GA↗

arXiv2008

Maximum Likelihood Fitting of Tidal Streams With Application to the Sagittarius Dwarf Tidal Tails

We present a maximum likelihood method for determining the spatial properties of tidal debris and of the Galactic spheroid. With this method we characterize Sagittarius debris using stars with the colors of blue F turnoff stars in SDSS stripe 82. The debris is located at (alpha, delta, R) = (31.37 deg +/- 0.26 deg, 0.0 deg, 29.22 +/- 0.20 kpc), with a (spatial) direction given by the unit vector < -0.991 +/- 0.007 kpc, 0.042 +/- 0.033 kpc, 0.127 +/- 0.046 kpc >, in Galactocentric Cartesian coordinates, and with FWHM = 6.74 +/- 0.06 kpc. This 2.5 degee-wide stripe contains 0.9% as many F turnoff stars as the current Sagittarius dwarf galaxy. Over small spatial extent, the debris is modeled as a cylinder with a density that falls off as a Gaussian with distance from the axis, while the smooth component of the spheroid is modeled with a Hernquist profile. We assume that the absolute magnitude of F turnoff stars is distributed as a Gaussian, which is an improvement over previous methods which fixed the absolute magnitude at Mg0 = 4.2. The effectiveness and correctness of the algorithm is demonstrated on a simulated set of F turnoff stars created to mimic SDSS stripe 82 data, which shows that we have a much greater accuracy than previous studies. Our algorithm can be applied to divide the stellar data into two catalogs: one which fits the stream density profile and one with the characteristics of the spheroid. This allows us to effectively separate tidal debris from the spheroid population, both facilitating the study of the tidal stream dynamics and providing a test of whether a smooth spheroidal population exists.

astro-ph↗