11 research outputs found
Data-driven Abstractions with Probabilistic Guarantees for Linear PETC Systems
No full textWe employ the scenario approach to compute probably approximately correct (PAC) bounds on the average inter-sample time (AIST) generated by an unknown PETC system, based on a finite number of samples. We extend the scenario optimisation to multiclass SVM algorithms in order to construct a PAC map between the concrete state-space and the inter-sample times. We then build a traffic model applying an l-complete relation and find, in the underlying graph, the cycles of minimum and maximum average weight: these provide lower and upper bounds on the AIST. Numerical benchmarks show the practical applicability of our method, which is compared against model-based state-of-the-art tools.Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.Team Manuel Mazo J
Data-driven Abstractions for Verification of Linear Systems
No full textWe introduce a novel approach for the construction of symbolic abstractions - simpler, finite-state models - which mimic the behaviour of a system of interest, and are commonly utilized to verify complex logic specifications. Such abstractions require an exhaustive knowledge of the concrete model, which can be difficult to obtain in real-world applications. To overcome this, we propose to sample finite length trajectories of an unknown system and build an abstraction based on the concept of ℓ -completeness. To this end, we introduce the notion of probabilistic behavioural inclusion. We provide probably approximately correct (PAC) guarantees that such an abstraction, constructed from experimental symbolic trajectories of finite length, includes all behaviours of the concrete system, for both finite and infinite time horizon. Finally, our method is displayed with numerical examples.Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.Team Manuel Mazo J
Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models
No full textThis paper presents Fossil 2.0, a new major release of a software tool for the synthesis of certificates (e.g., Lyapunov and barrier functions) for dynamical systems modelled as ordinary differential and difference equations. Fossil 2.0 is much improved from its original release, including new interfaces, a significantly expanded certificate portfolio, controller synthesis and enhanced extensibility. We present these new features as part of this tool paper. Fossil implements a counterexample-guided inductive synthesis (CEGIS) loop ensuring the soundness of the method. Our tool uses neural networks as templates to generate candidate functions, which are then formally proven by an satisfiability modulo theories solver acting as an assertion verifier. Improvements with respect to the first release include a wider range of certificates, synthesis of control laws, and support for discrete-time models.Team Manuel Mazo J
Augmented Neural Lyapunov Control
No full textMachine learning-based methodologies have recently been adapted to solve control problems. The Neural Lyapunov Control (NLC) method is one such example. This approach combines Artificial Neural Networks (ANNs) with Satisfiability Modulo Theories (SMT) solvers to synthesise stabilising control laws and to prove their formal correctness. The ANNs are trained over a dataset of state-space samples to generate candidate control and Lyapunov functions, while the SMT solvers are tasked with certifying the correctness of the Lyapunov function over a continuous domain or by returning a counterexample. Despite the approach’s attractiveness, issues can occur due to subsequent calls of the SMT module at times returning similar counterexamples, which can turn out to be uninformative and may lead to dataset overfitting. Additionally, the control network weights are usually initialised with pre-computed gains from state-feedback controllers, e.g. Linear-Quadratic Regulators. To properly perform the initialisation requires user time and control expertise. In this work, we present an Augmented NLC method that mitigates these drawbacks, removes the need for the control initialisation and further improves counterexample generation. As a result, the proposed method allows the synthesis of nonlinear (as well as linear) control laws with the sole requirement being the knowledge of the system dynamics. The ANLC is tested over challenging benchmarks such as the Lorenz attractor and outperformed existing methods in terms of successful synthesis rate. The developed framework is released open-source at: https://github.com/grande-dev/Augmented-Neural-Lyapunov-Control
Italian citizenship. Legal institution and reflections on some more recent problematic aspects
No full textThe author discusses the concept of citizenship beginning from the condition of submission up to the need of participating in the sovereign entity. There follows a discussion on the classical criteria for obtaining citizenship and an in-depth study of gaining it by marriage and by being a permanent member of the community. The last section deals with practical and procedural aspects for obtaining Italian citizenship.Si analizza la nozione di cittadinanza partendo dalla condizione di sottomissione fino all’esigenza di partecipazione all’ente sovrano. Vengono quindi illustrati i criteri classici per l’acquisto della cittadinanza ed approfonditi i casi di acquisizione in seguito a matrimonio e all’appartenenza in maniera stabile alla comunità. Nella parte conclusiva sono enunciati aspetti pratici e procedurali per l’acquisizione della cittadinanza italiana.Se analiza el concepto de ciudadanía a partir de la condición de sumisión para llegar a la exigencia de participación en la entidad soberana. Se ilustran los criterios clásicos para la adquisición de la ciudadanía y se profundizan los casos de adquisición de la misma a través del matrimonio y de la pertenencia a la comunidad de manera estable. En la sección final, se establecen los aspectos prácticos y de procedimiento para la adquisición de la nacionalidad italiana
Passive Fault-Tolerant Augmented Neural Lyapunov Control: A method to synthesise control functions for marine vehicles affected by actuators faults
No full textClosed-loop stability of control systems can be undermined by actuator faults. Redundant actuator sets and Fault-Tolerant Control (FTC) strategies can be exploited to enhance system resiliency to loss of actuator efficiency, complete failures or jamming. Passive FTC methods entail designing a fixed-gain control law that can preserve the stability of the closed-loop system when faults occur, by compromising on the performance of the faultless system. The use of Passive FTC methods is of particular interest in the case of underwater autonomous platforms, where the use of extensive sensoring to monitor the status of the actuator is limited by strict space and energy constraints. In this work, a machine learning-based method is formulated to systematically synthesise control laws for systems affected by actuator faults, encompassing partial and total loss of actuator efficiency and control surfaces jamming. Differently from other methods in this category, the closed-loop stability is formally certified. The learning architecture encompasses two Artificial Neural Networks, one representing the control law, and the other resembling a Control Lyapunov Function (CLF). Periodically, a Satisfiability Modulo Theory solver is employed to verify that the synthesised CLF formally satisfies the theoretical Lyapunov conditions associated to both the nominal and faulty dynamics. The method is applied to three marine test cases: first, an Autonomous Underwater Vehicle performing planar motion and subjected to full loss of actuator efficiency is investigated. Next, a study is conducted on a hybrid Underwater Glider with a pair of independent twin stern planes jamming at a fixed position. Finally, partial loss of effectiveness is considered. In all three scenarios, the system is able to synthesise stabilising control laws with performance degradation prescribed by the user. Unlike other machine-learning based techniques, this method offers formal stability certificates and relies on limited computational resources rendering it possible to be run on unassuming office laptops. An open-source software tool is developed and released at: https://github.com/grande-dev/pFT-ANLC.Team Manuel Mazo J
Comparison between autogenous saphenous vein and heparin-bonded expanded polytetrafluoroethylene for below-the-knee popliteal and tibial bypasses in patients with critical limb ischemia
No full textUnusual iatrogenic common femoral artery injury during penile prosthesis placement in gender-confirming surgery
No full textThe primary visual cortex of Cetartiodactyls: organization, cytoarchitectonics and comparison with perissodactyls and primates.
No full textCetartiodactyls include terrestrial and marine species, all generally endowed with a comparatively lateral position of their eyes and a relatively limited binocular field of vision. To this day, our understanding of the visual system in mammals beyond the few studied animal models remains limited. In the present study, we examined the primary visual cortex of Cetartiodactyls that live on land (sheep, Père David deer, giraffe); in the sea (bottlenose dolphin, Risso's dolphin, long-finned pilot whale, Cuvier's beaked whale, sperm whale and fin whale); or in an amphibious environment (hippopotamus). We also sampled and studied the visual cortex of the horse (a closely related perissodactyl) and two primates (chimpanzee and pig-tailed macaque) for comparison. Our histochemical and immunohistochemical results indicate that the visual cortex of Cetartiodactyls is characterized by a peculiar organization, structure, and complexity of the cortical column. We noted a general lesser lamination compared to simians, with diminished density, and an apparent simplification of the intra- and extra-columnar connections. The presence and distribution of calcium-binding proteins indicated a notable absence of parvalbumin in water species and a strong reduction of layer 4, usually enlarged in the striated cortex, seemingly replaced by a more diffuse distribution in neighboring layers. Consequently, thalamo-cortical inputs are apparently directed to the higher layers of the column. Computer analyses and statistical evaluation of the data confirmed the results and indicated a substantial correlation between eye placement and cortical structure, with a markedly segregated pattern in cetaceans compared to other mammals. Furthermore, cetacean species showed several types of cortical lamination which may reflect differences in function, possibly related to depth of foraging and consequent progressive disappearance of light, and increased importance of echolocation. [Abstract copyright: © 2021. The Author(s).
