arXiv subjects

Simone Martini

Publications and source records attributed to Simone Martini.

At least 19 recordsLinked to original sources

arXiv2026

Universal Extremum Seeking Mechanism for Lift Variation in Soaring Birds Flight: A New Paradigm in Computational Physics and Biology

In this letter, we reveal a universal, very simple extremum seeking natural feedback law and mechanism that governs, adapts, and generates in real-time, optimized lift variations for successful energy gain flight in presence of wind shear. The introduced law/mechanism, which is computationally minimal and needs only sensory information of the wind or local energy rate (i.e., model-free and data-driven) is able to characterize and replicate dynamic soaring optimized flight physics of windward climb in real-time for a variety of soaring birds species, namely wandering albatross, black-browed albatross and grey-headed albatross. We confirm the effectiveness of this new simple, real-time law by successful comparisons with sophisticated non-real-time optimal control solver and reported biological data. Our results establish the proposed mechanism as a new paradigm in soaring flight physics. That is, our results substantially advance the computational physics/biology aspects of the problem while providing a biologically plausible theory for avian soaring behavior.

physics.bio-ph↗

arXiv2025

Model-Free Optimization and Control of Rigid Body Dynamics: An Extremum Seeking for Vibrational Stabilization Approach

In this paper, we introduce a model-free, real-time, dynamic optimization and control method for a class of rigid body dynamics. Our method is based on a recent extremum seeking control for vibrational stabilization (ESC-VS) approach that is applicable to a class of second-order mechanical systems. The new ESC-VS method is able to stabilize a rigid body dynamic system about the optimal state of an objective function that can be unknown expression-wise, but assessable through measurements; the ESC-VS is operable by using only one perturbation/vibrational signal. We demonstrate the effectiveness and the applicability of our ESC-VS approach via three rigid-body systems: (1) satellite attitude dynamics, (2) quadcopter attitude dynamics, and (3) acceleration-controlled unicycle dynamics. The results, including simulations with and without measurement delays/noise, illustrate the ability of our ESC-VS to operate successfully as a new methodology of optimization and control for rigid body dynamics.

math.OC↗

arXiv2025

First Experimental Demonstration of Natural Hovering Extremum Seeking: A New Paradigm in Flapping Flight Physics

In this letter, we report the first experimental demonstration of the recently emerged new paradigm in hovering and flapping flight physics called (Natural Hovering Extremum Seeking (NH-ES)) [doi.org/10.1103/4dm4-kc4g], which theorized that stable hovering flight physics observed in nature by flapping insects and hummingbirds can be generated via a model-free, real-time, computationally-basic, sensory-based feedback mechanism that only needs the built-in natural oscillations of the flapping wing as both the control and the propulsive input. We run experiments of moth-like, light source-seeking, on a flapping-wing body in a total model-free setting that is agnostic to morphological parameters and body/aerodynamic models. We show that the flapping body using NH-ES gains altitude and stabilizes autonomously the servos responsible for flapping, including with pitching dynamics (believed in literature to be a main reason of instability in open-loop hovering). The flapping body effectively/stably hovers about the light source, needing only feedback of local measurements of light intensity. Our results were also achieved under delay/noise effects, supporting earlier observations that NH-ES is robust against potential processing delays and noisy-sensations.

cs.RO↗

arXiv2025

Dimensionality Reduction with Koopman Generalized Eigenfunctions

This paper presents a methodology to achieve lower-dimensional Koopman quasi-linear representations of nonlinear system dynamics using Koopman generalized eigenfunctions. The proposed approach considers the analytically derived Koopman formulation of rigid body dynamics, but it can be extended to any data-driven or analytically derived generalized eigenfunction set. It achieves a representation for which the number of Koopman observables matches the number of inputs allowing for Koopman linearization control solutions rather than resorting to the least squares approximation method adopted in high dimensional Koopman formulations. Through a linear combination of Koopman generalized eigenfunctions a new set of Koopman generalized eigenfunction is constructed so that the zero order truncation approximate a Koopman eigenfunction which can be used to design linear control strategies to steer the dynamics of the original nonlinear system. The proposed methodology is tested by designing a linear quadratic (LQ) flight controller for a quadrotor UAV. Numerical and Hardware-in-the-loop (HIL) simulations validate the applicability and real-time implementability of the proposed approach in the presence of noise and sensor delays. The main advantage of the proposed method is the realization of a fully actuated Koopman based model which, in the case of the underactuated quadrotor system, allows to achieve trajectory tracking through a single linear control loop.

eess.SY↗

arXiv2025

Reinforcement Learning Based Prediction of PID Controller Gains for Quadrotor UAVs

A reinforcement learning (RL) based methodology is proposed and implemented for online fine-tuning of PID controller gains, thus, improving quadrotor effective and accurate trajectory tracking. The RL agent is first trained offline on a quadrotor PID attitude controller and then validated through simulations and experimental flights. RL exploits a Deep Deterministic Policy Gradient (DDPG) algorithm, which is an off-policy actor-critic method. Training and simulation studies are performed using Matlab/Simulink and the UAV Toolbox Support Package for PX4 Autopilots. Performance evaluation and comparison studies are performed between the hand-tuned and RL-based tuned approaches. The results show that the controller parameters based on RL are adjusted during flights, achieving the smallest attitude errors, thus significantly improving attitude tracking performance compared to the hand-tuned approach.

eess.SY↗

arXiv2024

Koopman Analytical Modeling of Position and Attitude Dynamics: a Case Study for Quadrotor Control

This research presents a novel, analytical, Koopman Operator based formulation for position and attitude dynamics which can be used to derive control strategies for underactuated systems. Compared to data driven Koopman based techniques, the analytical approach presented in this work is model based and allows for an exact linear representation of the original nonlinear position and attitude dynamics. In fact, the resulting infinite dimensional model, defined in the lifted state space, is linear in the autonomous component and state dependent in the control. A boundary study is carried on to define the range of validity of the finite truncation of the Koopman based model followed by a controllability and stabilizability analysis to show the feasibility of employing the derived model for control system design. Compared to existing literature formulation, the presented model results in a better approximation of the original dyanmics using a more compact truncation of the lifted state space. Moreover, the model is derived using the Koopman approach on the entirety of the dynamics and does not require the need of angular velocity dynamic compensation. A case study involving an underactuated quadrotor unmanned aerial vehicle (UAV) is provided to show that, for practical use, a truncated subset of the infinite dimensional model, embeds most of the original nonlinear dynamics and can be used to design linear control strategies in the lifted space which results in nonlinear controllers in the original state space. The main advantages of the presented approach reside in the effective use of linear control strategies for nonlinear plats and the solution of the underactuation problem employing a single control loop.

eess.SY↗

arXiv2023

Correction to Euler Lagrange Multirotor Model with Euler Angles Generalized Coordinates

This technical note proves analytically how the exact equivalence of the Newton-Euler and Euler-Lagrange modeling formulations as applied to multirotor UAVs is achieved. This is done by deriving a revised Euler-Lagrange multirotor attitude dynamics model. A review of the published literature reveals that the commonly adopted Euler-Lagrange multirotor dynamics model is equivalent to the Newton-Euler model only when it comes to the position dynamics, but not in the attitude dynamics. Step-by-step derivations and calculations are provided to show how modeling equivalence to the Newton-Euler formulation is proven. The modeling equivalence is then verified by obtaining identical results in numerical simulation studies. Simulation results also illustrate that when using the revised model for feedback linearization, controller stability at high gains is improved.

eess.SY↗

arXiv2021

Online Unplugged and Block-Based Cryptography in Grade 10

We report our experience of an extracurricular online intervention on cryptography principles in 10th grade. This paper's first goal is to present the learning path we designed, influenced by cryptography core ideas rather than technical knowledge. We will detail how we used Snap! (a visual programming language) to realize hands-on activities: programming playgrounds to experiment with cryptosystems and their limits, and interactive support for an unplugged activity on the Diffie-Hellman key exchange. The second goal is to evaluate our intervention in terms of both student perceptions and learning of core cryptography ideas. The students appreciated the course and felt that, despite being remote, it was fun, interesting, and engaging. They said the course helped them understand the role of cryptography, CS, and Math in society and sparked their interest, especially in cryptography and CS. The third goal is to discuss what worked well and areas of improvement. Pedagogically, remote teaching caused high "instructor blindness" and prevented us from giving the optimal amount of guidance during the exploration activities with Snap! playgrounds, making them sometimes too challenging for total programming novices. On the other hand, the "remote-unplugged" Diffie-Hellman worked well: it embodies a coherent metaphor that engaged the students and made them grasp this groundbreaking protocol. The students praised the activities as engaging, even when challenging. The final assessment showed that the core cryptography ideas were well understood.

cs.CR↗

arXiv2020

From 2-sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics

We extend to natural deduction the approach of Linear Nested Sequents and of 2-sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction -- only one introduction and one elimination rule per connective, no additional (structural) rule, no explicit reference to the accessibility relation of the intended Kripke models. We give systems for the normal modal logics from K to S4. For the intuitionistic versions of the systems, we define proof reduction, and prove proof normalization, thus obtaining a syntactical proof of consistency. For logics K and K4 we use existence predicates (following Scott) for formulating sound deduction rules.

cs.LO↗

arXiv2020

A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic

Extending and generalizing the approach of 2-sequents (Masini, 1992), we present sequent calculi for the classical modal logics in the K, D, T, S4 spectrum. The systems are presented in a uniform way-different logics are obtained by tuning a single parameter, namely a constraint on the applicability of a rule. Cut-elimination is proved only once, since the proof goes through independently from the constraints giving rise to the different systems. A sequent calculus for the discrete linear temporal logic ltl is also given and proved complete. Leitmotiv of the paper is the formal analogy between modality and first-order quantification.

cs.LO↗

arXiv2017

Quantum Turing Machines Computations and Measurements

Contrary to the classical case, the relation between quantum programming languages and quantum Turing Machines (QTM) has not being fully investigated. In particular, there are features of QTMs that have not been exploited, a notable example being the intrinsic infinite nature of any quantum computation. In this paper we propose a definition of QTM, which extends and unifies the notions of Deutsch and Bernstein and Vazirani. In particular, we allow both arbitrary quantum input, and meaningful superpositions of computations, where some of them are "terminated" with an "output", while others are not. For some infinite computations an "output" is obtained as a limit of finite portions of the computation. We propose a natural and robust observation protocol for our QTMs, that does not modify the probability of the possible outcomes of the machines. Finally, we use QTMs to define a class of quantum computable functions---any such function is a mapping from a general quantum state to a probability distribution of natural numbers. We expect that our class of functions, when restricted to classical input-output, will be not different from the set of the recursive functions.

cs.LO↗

arXiv2015

Several types of types in programming languages

Types are an important part of any modern programming language, but we often forget that the concept of type we understand nowadays is not the same it was perceived in the sixties. Moreover, we conflate the concept of "type" in programming languages with the concept of the same name in mathematical logic, an identification that is only the result of the convergence of two different paths, which started apart with different aims. The paper will present several remarks (some historical, some of more conceptual character) on the subject, as a basis for a further investigation. The thesis we will argue is that there are three different characters at play in programming languages, all of them now called types: the technical concept used in language design to guide implementation; the general abstraction mechanism used as a modelling tool; the classifying tool inherited from mathematical logic. We will suggest three possible dates ad quem for their presence in the programming language literature, suggesting that the emergence of the concept of type in computer science is relatively independent from the logical tradition, until the Curry-Howard isomorphism will make an explicit bridge between them.

cs.PL↗

arXiv2015

Towards A Theory Of Quantum Computability

We propose a definition of quantum computable functions as mappings between superpositions of natural numbers to probability distributions of natural numbers. Each function is obtained as a limit of an infinite computation of a quantum Turing machine. The class of quantum computable functions is recursively enumerable, thus opening the door to a quantum computability theory which may follow some of the classical developments.

cs.LO↗

arXiv2012

On Constructor Rewrite Systems and the Lambda-Calculus (Long Version)

We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In particular, weak call-by-value beta-reduction can be simulated by an orthogonal constructor term rewrite system in the same number of reduction steps. Conversely, each reduction in a term rewrite system can be simulated by a constant number of beta-reduction steps. This is relevant to implicit computational complexity, because the number of beta steps to normal form is polynomially related to the actual cost (that is, as performed on a Turing machine) of normalization, under weak call-by-value reduction. Orthogonal constructor term rewrite systems and lambda-calculus are thus both polynomially related to Turing machines, taking as notion of cost their natural parameters.

cs.PL↗

arXiv2012

On Constructor Rewrite Systems and the Lambda Calculus

We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In particular, weak call-by- value beta-reduction can be simulated by an orthogonal constructor term rewrite system in the same number of reduction steps. Conversely, each reduction in a term rewrite system can be simulated by a constant number of beta-reduction steps. This is relevant to implicit computational complexity, because the number of beta steps to normal form is polynomially related to the actual cost (that is, as performed on a Turing machine) of normalization, under weak call-by-value reduction. Orthogonal constructor term rewrite systems and lambda-calculus are thus both polynomially related to Turing machines, taking as notion of cost their natural parameters.

cs.PL↗

arXiv2010

Light Logics and Higher-Order Processes

We show that the techniques for resource control that have been developed in the so-called "light logics" can be fruitfully applied also to process algebras. In particular, we present a restriction of Higher-Order pi-calculus inspired by Soft Linear Logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

cs.LO↗

arXiv2010

General Ramified Recurrence is Sound for Polynomial Time

Leivant's ramified recurrence is one of the earliest examples of an implicit characterization of the polytime functions as a subalgebra of the primitive recursive functions. Leivant's result, however, is originally stated and proved only for word algebras, i.e. free algebras whose constructors take at most one argument. This paper presents an extension of these results to ramified functions on any free algebras, provided the underlying terms are represented as graphs rather than trees, so that sharing of identical subterms can be exploited.

cs.LO↗

arXiv2005

An Invariant Cost Model for the Lambda Calculus

We define a new cost model for the call-by-value lambda-calculus satisfying the invariance thesis. That is, under the proposed cost model, Turing machines and the call-by-value lambda-calculus can simulate each other within a polynomial time overhead. The model only relies on combinatorial properties of usual beta-reduction, without any reference to a specific machine or evaluator. In particular, the cost of a single beta reduction is proportional to the difference between the size of the redex and the size of the reduct. In this way, the total cost of normalizing a lambda term will take into account the size of all intermediate results (as well as the number of steps to normal form).

cs.LO↗