Showing 1–50 of 66 results for author: Farrell, M

Can postgraduate translation students identify machine-generated text?

Authors: Michael Farrell

Abstract: Given the growing use of generative artificial intelligence as a tool for creating multilingual content and bypassing both machine and traditional translation methods, this study explores the ability of linguistically trained individuals to discern machine-generated output from human-written text (HT). After brief training sessions on the textual anomalies typically found in synthetic text (ST), t… ▽ More Given the growing use of generative artificial intelligence as a tool for creating multilingual content and bypassing both machine and traditional translation methods, this study explores the ability of linguistically trained individuals to discern machine-generated output from human-written text (HT). After brief training sessions on the textual anomalies typically found in synthetic text (ST), twenty-three postgraduate translation students analysed excerpts of Italian prose and assigned likelihood scores to indicate whether they believed they were human-written or AI-generated (ChatGPT-4o). The results show that, on average, the students struggled to distinguish between HT and ST, with only two participants achieving notable accuracy. Closer analysis revealed that the students often identified the same textual anomalies in both HT and ST, although features such as low burstiness and self-contradiction were more frequently associated with ST. These findings suggest the need for improvements in the preparatory training. Moreover, the study raises questions about the necessity of editing synthetic text to make it sound more human-like and recommends further research to determine whether AI-generated text is already sufficiently natural-sounding not to require further refinement. △ Less

Submitted 18 April, 2025; v1 submitted 12 April, 2025; originally announced April 2025.

Comments: 10 pages, accepted for MT Summit 2025, Geneva, Switzerland, 23-27 June 2025

Adventures in FRET and Specification

Authors: Marie Farrell, Matt Luckcuck, Rosemary Monahan, Conor Reynolds, Oisín Sheridan

Abstract: This paper gives an overview of previous work in which the authors used NASA's Formal Requirement Elicitation Tool (FRET) to formalise requirements. We discuss four case studies where we used FRET to capture the system's requirements. These formalised requirements subsequently guided the case study specifications in a combination of formal paradigms. For each case study we summarise insights gaine… ▽ More This paper gives an overview of previous work in which the authors used NASA's Formal Requirement Elicitation Tool (FRET) to formalise requirements. We discuss four case studies where we used FRET to capture the system's requirements. These formalised requirements subsequently guided the case study specifications in a combination of formal paradigms. For each case study we summarise insights gained during this process, exploring the expressiveness and the potential interoperability of these approaches. Our experience confirms FRET's suitability as a framework for the elicitation and understanding of requirements and for providing traceability from requirements to specification. △ Less

Submitted 31 March, 2025; originally announced March 2025.

Comments: Published at ISoLA 2024

Treatment Effect Heterogeneity in Regression Discontinuity Designs

Authors: Sebastian Calonico, Matias D. Cattaneo, Max H. Farrell, Filippo Palomba, Rocio Titiunik

Abstract: Empirical studies using Regression Discontinuity (RD) designs often explore heterogeneous treatment effects based on pretreatment covariates. However, the lack of formal statistical methods has led to the widespread use of ad hoc approaches in applications. Motivated by common empirical practice, we develop a unified, theoretically grounded framework for RD heterogeneity analysis. We show that a f… ▽ More Empirical studies using Regression Discontinuity (RD) designs often explore heterogeneous treatment effects based on pretreatment covariates. However, the lack of formal statistical methods has led to the widespread use of ad hoc approaches in applications. Motivated by common empirical practice, we develop a unified, theoretically grounded framework for RD heterogeneity analysis. We show that a fully interacted local linear (in functional parameters) model effectively captures heterogeneity while still being tractable and interpretable in applications. The model structure holds without loss of generality for discrete covariates, while for continuous covariates our proposed (local functional linear-in-parameters) model can be potentially restrictive, but it nonetheless naturally matches standard empirical practice and offers a causal interpretation for RD applications. We establish principled bandwidth selection and robust bias-corrected inference methods to analyze heterogeneous treatment effects and test group differences. We provide companion software to facilitate implementation of our results. An empirical application illustrates the practical relevance of our methods. △ Less

Submitted 26 March, 2025; v1 submitted 17 March, 2025; originally announced March 2025.

Rocketquake Seismology with a Falcon 9 Rocket Source

Authors: Gerard. T. Schuster, Jing Li, Sherif Hanafy, Vaughn Thompson, Jamie Mark Farrell, Daniel Trentman

Abstract: We investigate the feasibility of using rocket launches, specifically rocketquakes, as a seismic source to image subsurface velocity and geology of planetary bodies. Toward this goal, we record the seismic vibrations excited by a Falcon 9 rocket launch from Vandenberg Space Force Base (SFB) near Lompoc, California. Nine passive three-component (3C) seismometers were deployed every 18.75 meters alo… ▽ More We investigate the feasibility of using rocket launches, specifically rocketquakes, as a seismic source to image subsurface velocity and geology of planetary bodies. Toward this goal, we record the seismic vibrations excited by a Falcon 9 rocket launch from Vandenberg Space Force Base (SFB) near Lompoc, California. Nine passive three-component (3C) seismometers were deployed every 18.75 meters along a 45-degree line from the launch site starting at the offset of about 7 km kilometers from the launch pad. Results show that coherent body waves can be recorded with a P-velocity of more than 2.0 km/s and a penetration depth of 1 km or deeper. Stronger Rayleigh waves were also recorded and inverted to give an S-velocity profile to a depth of 60 m. Notably, a 3C recorder placed approximately 15 km from the launch site did not capture any discernible body wave arrivals. The imaging techniques employed for rocketquake seismology integrate inversion methods from earthquake and exploration seismology, yielding the P- and S-velocity profiles of the subsurface. These results suggest that rocket launches as seismic sources will provide unprecedented opportunities for identifying the subsurface hazards, faults, tunnels, water ice, and mineral deposits of planetary bodies and their moons. △ Less

Submitted 4 February, 2025; v1 submitted 3 February, 2025; originally announced February 2025.

Comments: 13 pages; 8 Figures

Distortions in Charged-Particle Images of Laser Direct-Drive Inertial Confinement Fusion Implosions

Authors: P. V. Heuer, J. L. Peebles, J. Kunimune, H. G. Rinderknecht, J. R. Davies, V. Gopalaswamy, J. Frelier, M. Scott, J. Roberts, B. Brannon, H. McClow, R. Fairbanks, S. P. Regan, J. A. Frenje, M. Gatu Johnson, F. H. Séguin, A. J. Crilly, B. D. Appelbe, M. Farrell, J. Stutz

Abstract: Energetic charged particles generated by inertial confinement fusion (ICF) implosions encode information about the spatial morphology of the hot-spot and dense fuel during the time of peak fusion reactions. The knock-on deuteron imager (KoDI) was developed at the Omega Laser Facility to image these particles in order to diagnose low-mode asymmetries in the hot-spot and dense fuel layer of cryogeni… ▽ More Energetic charged particles generated by inertial confinement fusion (ICF) implosions encode information about the spatial morphology of the hot-spot and dense fuel during the time of peak fusion reactions. The knock-on deuteron imager (KoDI) was developed at the Omega Laser Facility to image these particles in order to diagnose low-mode asymmetries in the hot-spot and dense fuel layer of cryogenic deuterium--tritium ICF implosions. However, the images collected are distorted in several ways that prevent reconstruction of the deuteron source. In this paper we describe these distortions and a series of attempts to mitigate or compensate for them. We present several potential mechanisms for the distortions, including a new model for scattering of charged particles in filamentary electric or magnetic fields surrounding the implosion. Particle-tracing is used to create synthetic KoDI data based on the filamentary field model that reproduces the main experimentally observed image distortions. We conclude that the filamentary scattering model best matches the observed image distortions. Finally, we discuss potential impacts of filamentary fields on other charged-particle diagnostics. △ Less

Submitted 7 April, 2025; v1 submitted 4 December, 2024; originally announced December 2024.

Nonlinear Binscatter Methods

Authors: Matias D. Cattaneo, Richard K. Crump, Max H. Farrell, Yingjie Feng

Abstract: Binned scatter plots are a powerful statistical tool for empirical work in the social, behavioral, and biomedical sciences. Available methods rely on a quantile-based partitioning estimator of the conditional mean regression function to primarily construct flexible yet interpretable visualization methods, but they can also be used to estimate treatment effects, assess uncertainty, and test substan… ▽ More Binned scatter plots are a powerful statistical tool for empirical work in the social, behavioral, and biomedical sciences. Available methods rely on a quantile-based partitioning estimator of the conditional mean regression function to primarily construct flexible yet interpretable visualization methods, but they can also be used to estimate treatment effects, assess uncertainty, and test substantive domain-specific hypotheses. This paper introduces novel binscatter methods based on nonlinear, possibly nonsmooth M-estimation methods, covering generalized linear, robust, and quantile regression models. We provide a host of theoretical results and practical tools for local constant estimation along with piecewise polynomial and spline approximations, including (i) optimal tuning parameter (number of bins) selection, (ii) confidence bands, and (iii) formal statistical tests regarding functional form or shape restrictions. Our main results rely on novel strong approximations for general partitioning-based estimators covering random, data-driven partitions, which may be of independent interest. We demonstrate our methods with an empirical application studying the relation between the percentage of individuals without health insurance and per capita income at the zip-code level. We provide general-purpose software packages implementing our methods in Python, R, and Stata. △ Less

Submitted 21 July, 2024; originally announced July 2024.

Preserving the Hermiticity of the One-Body Density Matrix for a Non-Interacting Fermi Gas

Authors: L. M. Farrell, D. Eaton, P. Chitnelawong, K. Bencheikh, B. P. van Zyl

Abstract: The one-body density matrix (ODM) for a zero temperature non-interacting Fermi gas can be approximately obtained in the semiclassical regime through different $\hbar$-expansion techniques. One would expect that each method of approximating the ODM should yield equivalent density matrices which are both Hermitian and idempotent to any order in $\hbar$. However, the Kirzhnits and Wigner-Kirkwood met… ▽ More The one-body density matrix (ODM) for a zero temperature non-interacting Fermi gas can be approximately obtained in the semiclassical regime through different $\hbar$-expansion techniques. One would expect that each method of approximating the ODM should yield equivalent density matrices which are both Hermitian and idempotent to any order in $\hbar$. However, the Kirzhnits and Wigner-Kirkwood methods do not yield these properties, while the Grammaticos-Voros method does. Here we show explicitly, for arbitrary $d$-dimensions through an appropriate change into symmetric coordinates, that each method is indeed identical, Hermitian, and idempotent. This change of variables resolves the inconsistencies between the various methods, showing that the non-Hermitian and non-idempotent behavior of the Kirzhnits and Wigner-Kirkwood methods is an artifact of performing a non-symmetric truncation to the semiclassical $\hbar$-expansions. Our work also provides the first explicit derivation of the $d$-dimensional Grammaticos-Voros ODM, originally proposed by Redjati et al (2019 $\textit{J. Phys. Chem. Solids}$ 134 313-8) based on their $d=1,2,3,4$ expressions. △ Less

Submitted 9 September, 2024; v1 submitted 3 February, 2024; originally announced February 2024.

Comments: 21 pages

Journal ref: J. Phys. A: Math. Theor. 57 395201 (2024)

Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems

Authors: Marie Farrell, Matt Luckcuck, Mario Gleirscher, Maike Schwammberger

Abstract: This EPTCS volume contains the proceedings for the Fifth International Workshop on Formal Methods for Autonomous Systems (FMAS 2023), which was held on the 15th and 16th of November 2023. FMAS 2023 was co-located with 18th International Conference on integrated Formal Methods (iFM) (iFM'22), organised by Leiden Institute of Advanced Computer Science of Leiden University. The workshop itself was he… ▽ More This EPTCS volume contains the proceedings for the Fifth International Workshop on Formal Methods for Autonomous Systems (FMAS 2023), which was held on the 15th and 16th of November 2023. FMAS 2023 was co-located with 18th International Conference on integrated Formal Methods (iFM) (iFM'22), organised by Leiden Institute of Advanced Computer Science of Leiden University. The workshop itself was held at Scheltema Leiden, a renovated 19th Century blanket factory alongside the canal. FMAS 2023 received 25 submissions. We received 11 regular papers, 3 experience reports, 6 research previews, and 5 vision papers. The researchers who submitted papers to FMAS 2023 were from institutions in: Australia, Canada, Colombia, France, Germany, Ireland, Italy, the Netherlands, Sweden, the United Kingdom, and the United States of America. Increasing our number of submissions for the third year in a row is an encouraging sign that FMAS has established itself as a reputable publication venue for research on the formal modelling and verification of autonomous systems. After each paper was reviewed by three members of our Programme Committee we accepted a total of 15 papers: 8 long papers and 7 short papers. △ Less

Submitted 15 November, 2023; originally announced November 2023.

Journal ref: EPTCS 395, 2023

First bromine doped cryogenic implosion at the National Ignition Facility

Authors: A. C. Hayes, G. Kyrala, M. Gooden, J. B. Wilhelmy, L. Kot, P. Volegov, C. Wilde, B. Haines, Gerard Jungman, R. S. Rundberg, D. C. Wilson, C. Velsko, W. Cassata, E. Henry, C. Yeamans, C. Cerjan, T. Ma, T. Doppner, A. Nikroo, O. Hurricane, D. Callahan, D. Hinkel, D. Schneider, B. Bachmann, F. Graziani , et al. (7 additional authors not shown)

Abstract: We report on the first experiment dedicated to the study of nuclear reactions on dopants in a cryogenic capsule at the National Ignition Facility (NIF). This was accomplished using bromine doping in the inner layers of the CH ablator of a capsule identical to that used in the NIF shot N140520. The capsule was doped with 3$\times$10$^{16}$ bromine atoms. The doped capsule shot, N170730, resulted in… ▽ More We report on the first experiment dedicated to the study of nuclear reactions on dopants in a cryogenic capsule at the National Ignition Facility (NIF). This was accomplished using bromine doping in the inner layers of the CH ablator of a capsule identical to that used in the NIF shot N140520. The capsule was doped with 3$\times$10$^{16}$ bromine atoms. The doped capsule shot, N170730, resulted in a DT yield that was 2.6 times lower than the undoped equivalent. The Radiochemical Analysis of Gaseous Samples (RAGS) system was used to collect and detect $^{79}$Kr atoms resulting from energetic deuteron and proton ion reactions on $^{79}$Br. RAGS was also used to detect $^{13}$N produced dominantly by knock-on deuteron reactions on the $^{12}$C in the ablator. High-energy reaction-in-flight neutrons were detected via the $^{209}$Bi(n,4n)$^{206}$Bi reaction, using bismuth activation foils located 50 cm outside of the target capsule. The robustness of the RAGS signals suggest that the use of nuclear reactions on dopants as diagnostics is quite feasible. △ Less

Submitted 7 July, 2023; originally announced July 2023.

Report number: LA-UR-22-28149

Developing Multi-Agent Systems with Degrees of Neuro-Symbolic Integration [A Position Paper]

Authors: Louise Dennis, Marie Farrell, Michael Fisher

Abstract: In this short position paper we highlight our ongoing work on verifiable heterogeneous multi-agent systems and, in particular, the complex (and often non-functional) issues that impact the choice of structure within each agent. In this short position paper we highlight our ongoing work on verifiable heterogeneous multi-agent systems and, in particular, the complex (and often non-functional) issues that impact the choice of structure within each agent. △ Less

Submitted 19 May, 2023; originally announced May 2023.

Higher-order Refinements of Small Bandwidth Asymptotics for Density-Weighted Average Derivative Estimators

Authors: Matias D. Cattaneo, Max H. Farrell, Michael Jansson, Ricardo Masini

Abstract: The density weighted average derivative (DWAD) of a regression function is a canonical parameter of interest in economics. Classical first-order large sample distribution theory for kernel-based DWAD estimators relies on tuning parameter restrictions and model assumptions that imply an asymptotic linear representation of the point estimator. These conditions can be restrictive, and the resulting d… ▽ More The density weighted average derivative (DWAD) of a regression function is a canonical parameter of interest in economics. Classical first-order large sample distribution theory for kernel-based DWAD estimators relies on tuning parameter restrictions and model assumptions that imply an asymptotic linear representation of the point estimator. These conditions can be restrictive, and the resulting distributional approximation may not be representative of the actual sampling distribution of the statistic of interest. In particular, the approximation is not robust to bandwidth choice. Small bandwidth asymptotics offers an alternative, more general distributional approximation for kernel-based DWAD estimators that allows for, but does not require, asymptotic linearity. The resulting inference procedures based on small bandwidth asymptotics were found to exhibit superior finite sample performance in simulations, but no formal theory justifying that empirical success is available in the literature. Employing Edgeworth expansions, this paper shows that small bandwidth asymptotic approximations lead to inference procedures with higher-order distributional properties that are demonstrably superior to those of procedures based on asymptotic linear approximations. △ Less

Submitted 15 February, 2024; v1 submitted 31 December, 2022; originally announced January 2023.

Proceedings Fourth International Workshop on Formal Methods for Autonomous Systems (FMAS) and Fourth International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE)

Authors: Matt Luckcuck, Marie Farrell

Abstract: This EPTCS volume contains the joint proceedings for the fourth international workshop on Formal Methods for Autonomous Systems (FMAS 2022) and the fourth international workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE 2022), which were held on the 26th and 27th of September 2022. FMAS 2022 and ASYDE 2022 were held in conjunction with 20th International Conference on Software… ▽ More This EPTCS volume contains the joint proceedings for the fourth international workshop on Formal Methods for Autonomous Systems (FMAS 2022) and the fourth international workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE 2022), which were held on the 26th and 27th of September 2022. FMAS 2022 and ASYDE 2022 were held in conjunction with 20th International Conference on Software Engineering and Formal Methods (SEFM'22), at Humboldt University in Berlin. For FMAS, this year's workshop was our return to having in-person attendance after two editions of FMAS that were entirely online because of the restrictions necessitated by COVID-19. We were also keen to ensure that FMAS 2022 remained easily accessible to people who were unable to travel, so the workshop facilitated remote presentation and attendance. The goal of FMAS is to bring together leading researchers who are using formal methods to tackle the unique challenges presented by autonomous systems, to share their recent and ongoing work. Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the real world. As such, they exhibit the properties of safety-critical, cyber-physical, hybrid, and real-time systems. We are interested in work that uses formal methods to specify, model, or verify autonomous and/or robotic systems; in whole or in part. We are also interested in successful industrial applications and potential directions for this emerging application of formal methods. △ Less

Submitted 27 September, 2022; originally announced September 2022.

Journal ref: EPTCS 371, 2022

Logarithmic catastrophes and Stokes's phenomenon in waves at horizons

Authors: L. M. Farrell, C. J. Howls, D. H. J. O'Dell

Abstract: Waves propagating near an event horizon display interesting features including logarithmic phase singularities and caustics. We consider an acoustic horizon in a flowing Bose-Einstein condensate where the elementary excitations obey the Bogoliubov dispersion relation. In the hamiltonian ray theory the solutions undergo a broken pitchfork bifurcation near the horizon and one might therefore expect… ▽ More Waves propagating near an event horizon display interesting features including logarithmic phase singularities and caustics. We consider an acoustic horizon in a flowing Bose-Einstein condensate where the elementary excitations obey the Bogoliubov dispersion relation. In the hamiltonian ray theory the solutions undergo a broken pitchfork bifurcation near the horizon and one might therefore expect the associated wave structure to be given by a Pearcey function, this being the universal wave function that dresses catastrophes with two control parameters. However, the wave function is in fact an Airy-type function supplemented by a logarithmic phase term, a novel type of wave catastrophe. Similar wave functions arise in aeroacoustic flows from jet engines and also gravitational horizons if dispersion which violates Lorentz symmetry in the UV is included. The approach we take differs from previous authors in that we analyze the behaviour of the integral representation of the wave function using exponential coordinates. This allows for a different treatment of the branches that gives rise to an analysis based purely on saddlepoint expansions, which resolve the multiple real and complex waves that interact at the horizon and its companion caustic. We find that the horizon is a physical manifestation of a Stokes surface, marking the place where a wave is born, and that the horizon and the caustic do not in general coincide: the finite spatial region between them delineates a broadened horizon. △ Less

Submitted 28 February, 2023; v1 submitted 22 September, 2022; originally announced September 2022.

Comments: 34 pages, 12 figures

Journal ref: J. Phys. A: Math. Theor. 56, 044001 (2023)

A Compositional Approach to Verifying Modular Robotic Systems

Authors: Matt Luckcuck, Marie Farrell, Angelo Ferrando, Rafael C. Cardoso, Louise A. Dennis, Michael Fisher

Abstract: Robotic systems used in safety-critical industrial situations often rely on modular software architectures, and increasingly include autonomous components. Verifying that these modular robotic systems behave as expected requires approaches that can cope with, and preferably take advantage of, this inherent modularity. This paper describes a compositional approach to specifying the nodes in robotic… ▽ More Robotic systems used in safety-critical industrial situations often rely on modular software architectures, and increasingly include autonomous components. Verifying that these modular robotic systems behave as expected requires approaches that can cope with, and preferably take advantage of, this inherent modularity. This paper describes a compositional approach to specifying the nodes in robotic systems built using the Robotic Operating System (ROS), where each node is specified using First-Order Logic (FOL) assume-guarantee contracts that link the specification to the ROS implementation. We introduce inference rules that facilitate the composition of these node-level contracts to derive system-level properties. We also present a novel Domain-Specific Language, the ROS Contract Language, which captures a node's FOL specification and links this contract to its implementation. RCL contracts can be automatically translated, by our tool Vanda, into executable monitors; which we use to verify the contracts at runtime. We illustrate our approach through the specification and verification of an autonomous rover engaged in the remote inspection of a nuclear site, and finish with smaller examples that illustrate other useful features of our framework. △ Less

Submitted 30 November, 2023; v1 submitted 10 August, 2022; originally announced August 2022.

Comments: Version submitted to RAS

Modelling the Turtle Python library in CSP

Authors: Dara MacConville, Marie Farrell, Matt Luckcuck, Rosemary Monahan

Abstract: Software verification is an important tool in establishing the reliability of critical systems. One potential area of application is in the field of robotics, as robots take on more tasks in both day-to-day areas and highly specialised domains. Robots are usually given a plan to follow, if there are errors in this plan the robot will not perform reliably. The capability to check plans for errors i… ▽ More Software verification is an important tool in establishing the reliability of critical systems. One potential area of application is in the field of robotics, as robots take on more tasks in both day-to-day areas and highly specialised domains. Robots are usually given a plan to follow, if there are errors in this plan the robot will not perform reliably. The capability to check plans for errors in advance could prevent this. Python is a popular programming language in the robotics domain, through the use of the Robot Operating System (ROS) and various other libraries. Python's Turtle package provides a mobile agent, which we formally model here using Communicating Sequential Processes (CSP). Our interactive toolchain CSP2Turtle with CSP model and Python components, enables Turtle plans to be verified in CSP before being executed in Python. This means that certain classes of errors can be avoided, and provides a starting point for more detailed verification of Turtle programs and more complex robotic systems. We illustrate our approach with examples of robot navigation and obstacle avoidance in a 2D grid-world. △ Less

Submitted 20 July, 2022; originally announced July 2022.

Comments: In Proceedings AREA 2022, arXiv:2207.09058

Journal ref: EPTCS 362, 2022, pp. 15-22

Distributed Generalized Wirtinger Flow for Interferometric Imaging on Networks

Authors: Sean M. Farrell, Ashok Veeraraghavan, Ashutosh Sabharwal, César A. Uribe

Abstract: We study the problem of decentralized interferometric imaging over networks, where agents have access to a subset of local radar measurements and can compute pair-wise correlations with their neighbors. We propose a primal-dual distributed algorithm named Distributed Generalized Wirtinger Flow (DGWF). We use the theory of low rank matrix recovery to show when the interferometric imaging problem sa… ▽ More We study the problem of decentralized interferometric imaging over networks, where agents have access to a subset of local radar measurements and can compute pair-wise correlations with their neighbors. We propose a primal-dual distributed algorithm named Distributed Generalized Wirtinger Flow (DGWF). We use the theory of low rank matrix recovery to show when the interferometric imaging problem satisfies the Regularity Condition, which implies the Polyak-Lojasiewicz inequality. Moreover, we show that DGWF converges geometrically for smooth functions. Numerical simulations for single-scattering radar interferometric imaging demonstrate that DGWF can achieve the same mean-squared error image reconstruction quality as its centralized counterpart for various network connectivity and size. △ Less

Submitted 8 June, 2022; originally announced June 2022.

Comments: 6 pages, 3 figures, accepted to IFAC 2022 Conference on Networked Systems (NecSys22)

Why just FRET when you can Refactor? Retuning FRETISH Requirements

Authors: Matt Luckcuck, Marie Farrell, Oisín Sheridan

Abstract: Formal verification of a software system relies on formalising the requirements to which it should adhere, which can be challenging. While formalising requirements from natural-language, we have dependencies that lead to duplication of information across many requirements, meaning that a change to one requirement causes updates in several places. We propose to adapt code refactorings for NASA's Fo… ▽ More Formal verification of a software system relies on formalising the requirements to which it should adhere, which can be challenging. While formalising requirements from natural-language, we have dependencies that lead to duplication of information across many requirements, meaning that a change to one requirement causes updates in several places. We propose to adapt code refactorings for NASA's Formal Requirements Elicitation Tool (FRET), our tool-of-choice. Refactoring is the process of reorganising software to improve its internal structure without altering its external behaviour; it can also be applied to requirements, to make them more manageable by reducing repetition. FRET automatically translates requirements (written in its input language Fretish) into Temporal Logic, which enables us to formally verify that refactoring has preserved the requirements' underlying meaning. In this paper, we present four refactorings for Fretish requirements and explain their utility. We describe the application of one of these refactorings to the requirements of a civilian aircraft engine software controller, to decouple the dependencies from the duplication, and analyse how this changes the number of requirements and the number of repetitions. We evaluate our approach using Spot, a tool for checking equivalence of Temporal Logic specifications. △ Less

Submitted 11 February, 2022; originally announced February 2022.

Towards Refactoring FRETish Requirements

Authors: Marie Farrell, Matt Luckcuck, Oisin Sheridan, Rosemary Monahan

Abstract: Like software, requirements evolve and change frequently during the development process. Refactoring is the process of reorganising software without changing its behaviour, to make it easier to understand and modify. We propose refactoring for formalised requirements to reduce repetition in the requirement set so that they are easier to maintain as the system and requirements evolve. This work-in-… ▽ More Like software, requirements evolve and change frequently during the development process. Refactoring is the process of reorganising software without changing its behaviour, to make it easier to understand and modify. We propose refactoring for formalised requirements to reduce repetition in the requirement set so that they are easier to maintain as the system and requirements evolve. This work-in-progress paper describes our motivation for and initial approach to refactoring requirements in NASA's Formal Requirements Elicitation Tool (FRET). This work was directly triggered by our experience with an industrial aircraft engine software controller use case. In this paper, we reflect on the requirements that were obtained and, with a view to their maintainability, propose and outline functionality for refactoring FRETISH requirements. △ Less

Submitted 12 January, 2022; originally announced January 2022.

FRETting about Requirements: Formalised Requirements for an Aircraft Engine Controller

Authors: Marie Farrell, Matt Luckcuck, Oisin Sheridan, Rosemary Monahan

Abstract: [Context & motivation] Eliciting requirements that are detailed and logical enough to be amenable to formal verification is a difficult task. Multiple tools exist for requirements elicitation and some of these also support formalisation of requirements in a way that is useful for formal methods. [Question/problem] This paper reports on our experience of using the FRET alongside our industrial part… ▽ More [Context & motivation] Eliciting requirements that are detailed and logical enough to be amenable to formal verification is a difficult task. Multiple tools exist for requirements elicitation and some of these also support formalisation of requirements in a way that is useful for formal methods. [Question/problem] This paper reports on our experience of using the FRET alongside our industrial partner. The use case that we investigate is an aircraft engine controller. In this context, we evaluate the use of FRET to bridge the communication gap between formal methods experts and aerospace industry specialists. [Principal ideas/results] We describe our journey from ambiguous, natural-language requirements to concise, formalised FRET requirements. We include our analysis of the formalised requirements from the perspective of patterns, translation into other formal methods and the relationship between parent-child requirements in this set. We also provide insight into lessons learned throughout this process and identify future improvements to FRET. [Contribution] Previous experience reports have been published by the FRET team, but this is the first such report of an industrial use case that was written by researchers that have not been involved FRET's development. △ Less

Submitted 2 February, 2022; v1 submitted 8 December, 2021; originally announced December 2021.

Comments: 22 pages, 3 figures

Proceedings Third Workshop on Formal Methods for Autonomous Systems

Authors: Marie Farrell, Matt Luckcuck

Abstract: Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the real world. As such, they exhibit the properties of safety-critical, cyber-physical, hybrid, and real-time systems. This EPTCS volume contains the proceedings fo… ▽ More Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the real world. As such, they exhibit the properties of safety-critical, cyber-physical, hybrid, and real-time systems. This EPTCS volume contains the proceedings for the third workshop on Formal Methods for Autonomous Systems (FMAS 2021), which was held virtually on the 21st and 22nd of October 2021. Like the previous workshop, FMAS 2021 was an online, stand-alone event, as an adaptation to the ongoing COVID-19 restrictions. Despite the challenges this brought, we were determined to build on the success of the previous two FMAS workshops. The goal of FMAS is to bring together leading researchers who are tackling the unique challenges of autonomous systems using formal methods, to present recent and ongoing work. We are interested in the use of formal methods to specify, model, or verify autonomous and/or robotic systems; in whole or in part. We are also interested in successful industrial applications and potential future directions for this emerging application of formal methods. △ Less

Submitted 21 October, 2021; originally announced October 2021.

Journal ref: EPTCS 348, 2021

A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements

Authors: Matt Luckcuck, Marie Farrell, Oisín Sheridan, Rosemary Monahan

Abstract: Verification of complex, safety-critical systems is a significant challenge. Manual testing and simulations are often used, but are only capable of exploring a subset of the system's reachable states. Formal methods are mathematically-based techniques for the specification and development of software, which can provide proofs of properties and exhaustive checks over a system's state space. In this… ▽ More Verification of complex, safety-critical systems is a significant challenge. Manual testing and simulations are often used, but are only capable of exploring a subset of the system's reachable states. Formal methods are mathematically-based techniques for the specification and development of software, which can provide proofs of properties and exhaustive checks over a system's state space. In this paper, we present a formal requirements-driven methodology, applied to a model of an aircraft engine controller that has been provided by our industrial partner. Our methodology begins by formalising the controller's natural-language requirements using the (pre-existing) Formal Requirements Elicitation Tool (FRET), iteratively, in consultation with our industry partner. Once formalised, FRET can automatically translate the requirements to enable their verification alongside a Simulink model of the aircraft engine controller; the requirements can also guide formal verification using other approaches. These two parallel streams in our methodology seek to combine the results from formal requirements elicitation, classical verification approaches, and runtime verification; to support the verification of aerospace systems modelled in Simulink, from the requirements phase through to execution. Our methodology harnesses the power of formal methods in a way that complements existing verification techniques, and supports the traceability of requirements throughout the verification process. This methodology streamlines the process of developing verifiable aircraft engine controllers, by ensuring that the requirements are formalised up-front and useable during development. In this paper we give an overview of (FRET), describe our methodology and work to-date on the formalisation and verification of the requirements, and outline future work using our methodology. △ Less

Submitted 18 October, 2021; originally announced October 2021.

Comments: Submitted to AeroConf 2022

Capacity of Group-invariant Linear Readouts from Equivariant Representations: How Many Objects can be Linearly Classified Under All Possible Views?

Authors: Matthew Farrell, Blake Bordelon, Shubhendu Trivedi, Cengiz Pehlevan

Abstract: Equivariance has emerged as a desirable property of representations of objects subject to identity-preserving transformations that constitute a group, such as translations and rotations. However, the expressivity of a representation constrained by group equivariance is still not fully understood. We address this gap by providing a generalization of Cover's Function Counting Theorem that quantifies… ▽ More Equivariance has emerged as a desirable property of representations of objects subject to identity-preserving transformations that constitute a group, such as translations and rotations. However, the expressivity of a representation constrained by group equivariance is still not fully understood. We address this gap by providing a generalization of Cover's Function Counting Theorem that quantifies the number of linearly separable and group-invariant binary dichotomies that can be assigned to equivariant representations of objects. We find that the fraction of separable dichotomies is determined by the dimension of the space that is fixed by the group action. We show how this relation extends to operations such as convolutions, element-wise nonlinearities, and global and local pooling. While other operations do not change the fraction of separable dichotomies, local pooling decreases the fraction, despite being a highly nonlinear operation. Finally, we test our theory on intermediate representations of randomly initialized and fully trained convolutional neural networks and find perfect agreement. △ Less

Submitted 5 February, 2022; v1 submitted 14 October, 2021; originally announced October 2021.

Comments: Version accepted to ICLR 2022

Network embedding unveils the hidden interactions in the mammalian virome

Authors: Timothée Poisot, Marie-Andrée Ouellet, Nardus Mollentze, Maxwell J. Farrell, Daniel J. Becker, Liam Brierly, Gregory F. Albery, Rory J. Gibb, Stephanie N. Seifert, Colin J. Carlson

Abstract: At most 1-2% of the global virome has been sampled to date. Recent work has shown that predicting which host-virus interactions are possible but undiscovered or unrealized is, fundamentally, a network science problem. Here, we develop a novel method that combines a coarse recommender system (Linear Filtering; LF) with an imputation algorithm based on low-rank graph embedding (Singular Value Decomp… ▽ More At most 1-2% of the global virome has been sampled to date. Recent work has shown that predicting which host-virus interactions are possible but undiscovered or unrealized is, fundamentally, a network science problem. Here, we develop a novel method that combines a coarse recommender system (Linear Filtering; LF) with an imputation algorithm based on low-rank graph embedding (Singular Value Decomposition; SVD) to infer host-virus associations. This combination of techniques results in informed initial guesses based on directly measurable network properties (density, degree distribution) that are refined through SVD (which is able to leverage emerging features). Using this method, we recovered highly plausible undiscovered interactions with a strong signal of viral coevolutionary history, and revealed a global hotspot of unusually unique but unsampled (or unrealized) host-virus interactions in the Amazon rainforest. We develop several tests for quantifying the bias and realism of these predictions, and show that the LF-SVD method is robust in each aspect. We finally show that graph embedding of the imputed network can be used to improve predictions of human infection from viral genome features, showing that the global structure of the mammal-virus network provides additional insights into human disease emergence. △ Less

Submitted 24 March, 2022; v1 submitted 31 May, 2021; originally announced May 2021.

Comments: 35 pages, 2 figures, 9 extended data figures, 7 extended data tables

Building Specifications in the Event-B Institution

Authors: Marie Farrell, Rosemary Monahan, James F. Power

Abstract: This paper describes a formal semantics for the Event-B specification language using the theory of institutions. We define an institution for Event-B, EVT, and prove that it meets the validity requirements for satisfaction preservation and model amalgamation. We also present a series of functions that show how the constructs of the Event-B specification language can be mapped into our institution.… ▽ More This paper describes a formal semantics for the Event-B specification language using the theory of institutions. We define an institution for Event-B, EVT, and prove that it meets the validity requirements for satisfaction preservation and model amalgamation. We also present a series of functions that show how the constructs of the Event-B specification language can be mapped into our institution. Our semantics sheds new light on the structure of the Event-B language, allowing us to clearly delineate three constituent sub-languages: the superstructure, infrastructure and mathematical languages. One of the principal goals of our semantics is to provide access to the generic modularisation constructs available in institutions, including specification-building operators for parameterisation and refinement. We demonstrate how these features subsume and enhance the corresponding features already present in Event-B through a detailed study of their use in a worked example. We have implemented our approach via a parser and translator for Event-B specifications, EBtoEVT, which also provides a gateway to the Hets toolkit for heterogeneous specification. △ Less

Submitted 8 November, 2022; v1 submitted 19 March, 2021; originally announced March 2021.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 4 (November 9, 2022) lmcs:7286

Will the Mars Helicopter Induce Local Martian Atmospheric Breakdown?

Authors: W. M. Farrell, J. L. McLain, J. R. Marshall, A. Wang

Abstract: Any rotorcraft on Mars will fly in a low pressure and dusty environment. It is well known that helicopters on Earth become highly-charged due, in part, to triboelectric effects when flying in sandy conditions. We consider the possibility that the Mars Helicopter Scout (MHS), called Ingenuity, flying at Mars as part of the Mars2020 Perseverance mission, will also become charged due to grain-rotor t… ▽ More Any rotorcraft on Mars will fly in a low pressure and dusty environment. It is well known that helicopters on Earth become highly-charged due, in part, to triboelectric effects when flying in sandy conditions. We consider the possibility that the Mars Helicopter Scout (MHS), called Ingenuity, flying at Mars as part of the Mars2020 Perseverance mission, will also become charged due to grain-rotor triboelectric interactions. Given the low Martian atmospheric pressure of ~ 5 Torr, the tribocharge on the blade could become intense enough to stimulate gas breakdown near the surface of the rotorcraft. We modeled the grain-blade interaction as a line of current that forms along the blade edge in the region where grain-blade contacts are the greatest. This current then spreads throughout the entire connected quasi-conductive regions of the rotorcraft. Charge builds up on the craft and the dissipative pathway to remove charge is back into the atmosphere. We find that for blade tribocharging currents that form in an ambient atmospheric dust load, system current balance and charge dissipation can be accomplished via the nominal atmospheric conductive currents. However, at takeoff and landing, the rotorcraft could be in a rotor-created particulate cloud, leading to local atmospheric electrical breakdown near the rotorcraft. We especially note that the atmospheric currents in the breakdown are not large enough to create any hazard to Ingenuity itself, but Ingenuity operations can be considered a unique experiment that provides a test of the electrical properties of the Martian near-surface atmosphere. △ Less

Submitted 8 February, 2021; originally announced February 2021.

Comments: 23 pages, 5 figures, Accepted in Planetary Science Journal, AAS28294R1

Report number: NASA STRIVES # 20210009674

Lunar Volatiles and Solar System Science

Authors: Parvathy Prem, Ákos Kereszturi, Ariel N. Deutsch, Charles A. Hibbitts, Carl A. Schmidt, Cesare Grava, Casey I. Honniball, Craig J. Hardgrove, Carlé M. Pieters, David B. Goldstein, Donald C. Barker, Debra H. Needham, Dana M. Hurley, Erwan Mazarico, Gerardo Dominguez, G. Wesley Patterson, Georgiana Y. Kramer, Julie Brisset, Jeffrey J. Gillis-Davis, Julie L. Mitchell, Jamey R. Szalay, Jasper S. Halekas, James T. Keane, James W. Head, Kathleen E. Mandt , et al. (16 additional authors not shown)

Abstract: Understanding the origin and evolution of the lunar volatile system is not only compelling lunar science, but also fundamental Solar System science. This white paper (submitted to the US National Academies' Decadal Survey in Planetary Science and Astrobiology 2023-2032) summarizes recent advances in our understanding of lunar volatiles, identifies outstanding questions for the next decade, and dis… ▽ More Understanding the origin and evolution of the lunar volatile system is not only compelling lunar science, but also fundamental Solar System science. This white paper (submitted to the US National Academies' Decadal Survey in Planetary Science and Astrobiology 2023-2032) summarizes recent advances in our understanding of lunar volatiles, identifies outstanding questions for the next decade, and discusses key steps required to address these questions. △ Less

Submitted 9 December, 2020; originally announced December 2020.

On the Effect of Magnetospheric Shielding on the Lunar Hydrogen Cycle

Authors: Orenthal J. Tucker, William M. Farrell, Andrew R. Poppe

Abstract: We examine how water is produced globally over the lunar surface as it orbits in/out of the magnetotail. Due to the interaction of the solar wind (SW) with Earth's magnetic field, upstream the magnetic field is compressed down to ~10 Earth radii. However, the diverted stream of SW around Earth's magnetic field results in an extended depleted region of SW protons (positively charged hydrogen) out t… ▽ More We examine how water is produced globally over the lunar surface as it orbits in/out of the magnetotail. Due to the interaction of the solar wind (SW) with Earth's magnetic field, upstream the magnetic field is compressed down to ~10 Earth radii. However, the diverted stream of SW around Earth's magnetic field results in an extended depleted region of SW protons (positively charged hydrogen) out to 1000's of Earth radii, referred to as the magnetotail. The Moon orbits at a distance of ~40 Earth radii; therefore, upstream it is within the SW, but downstream it is partially shielded while in the magnetotail during full Moon. SW protons penetrate lunar soil particles and some H atoms can chemical react with oxygen to form water-like molecules such as OH/H2O. Most of the H atoms bounce around within grains until finding another hydrogen atom, chemically combine, and then escape the grain as H2 into the thin atmosphere. We developed a model to calculate the global distribution of OH produced in the lunar surface and H2 released to the atmosphere as the Moon orbits in/out of Earth's magnetotail. The model results are in good agreement with available observations. △ Less

Submitted 7 December, 2020; originally announced December 2020.

Comments: Under review with JGR

Towards Compositional Verification for Modular Robotic Systems

Authors: Rafael C. Cardoso, Louise A. Dennis, Marie Farrell, Michael Fisher, Matt Luckcuck

Abstract: Software engineering of modular robotic systems is a challenging task, however, verifying that the developed components all behave as they should individually and as a whole presents its own unique set of challenges. In particular, distinct components in a modular robotic system often require different verification techniques to ensure that they behave as expected. Ensuring whole system consistenc… ▽ More Software engineering of modular robotic systems is a challenging task, however, verifying that the developed components all behave as they should individually and as a whole presents its own unique set of challenges. In particular, distinct components in a modular robotic system often require different verification techniques to ensure that they behave as expected. Ensuring whole system consistency when individual components are verified using a variety of techniques and formalisms is difficult. This paper discusses how to use compositional verification to integrate the various verification techniques that are applied to modular robotic software, using a First-Order Logic (FOL) contract that captures each component's assumptions and guarantees. These contracts can then be used to guide the verification of the individual components, be it by testing or the use of a formal method. We provide an illustrative example of an autonomous robot used in remote inspection. We also discuss a way of defining confidence for the verification associated with each component. △ Less

Submitted 2 December, 2020; originally announced December 2020.

Comments: In Proceedings FMAS 2020, arXiv:2012.01176

Journal ref: EPTCS 329, 2020, pp. 15-22

Proceedings Second Workshop on Formal Methods for Autonomous Systems

Authors: Matt Luckcuck, Marie Farrell

Abstract: Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the real world. As such, they exhibit the properties of safety-critical, cyber-physical, hybrid, and real-time systems. The goal of FMAS is to bring together leading… ▽ More Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the real world. As such, they exhibit the properties of safety-critical, cyber-physical, hybrid, and real-time systems. The goal of FMAS is to bring together leading researchers who are tackling the unique challenges of autonomous systems using formal methods, to present recent and ongoing work. We are interested in the use of formal methods to specify, model, or verify autonomous or robotic systems; in whole or in part. We are also interested in successful industrial applications and potential future directions for this emerging application of formal methods. △ Less

Submitted 2 December, 2020; originally announced December 2020.

Journal ref: EPTCS 329, 2020

Defying the Circadian Rhythm: Clustering Participant Telemetry in the UK Biobank Data

Authors: Nikola Pocuca, Mark Farrell, Paul D. McNicholas

Abstract: The UK Biobank dataset follows over 500,000 volunteers and contains a diverse set of information related to societal outcomes. Among this vast collection, a large quantity of telemetry collected from wrist-worn accelerometers provides a snapshot of participant activity. Using this data, a population of shift workers, subjected to disrupted circadian rhythms, is analysed using a mixture model-based… ▽ More The UK Biobank dataset follows over 500,000 volunteers and contains a diverse set of information related to societal outcomes. Among this vast collection, a large quantity of telemetry collected from wrist-worn accelerometers provides a snapshot of participant activity. Using this data, a population of shift workers, subjected to disrupted circadian rhythms, is analysed using a mixture model-based approach to yield protective effects from physical activity on survival outcomes. In this paper, we develop a scalable, standardized, and unique methodology that efficiently clusters a vast quantity of participant telemetry. By building upon the work of Doherty et al. (2017), we introduce a standardized, low-dimensional feature for clustering purposes. Participants are clustered using a matrix variate mixture model-based approach. Once clustered, survival analysis is performed to demonstrate distinct lifetime outcomes for individuals within each cluster. In summary, we process, cluster, and analyse a subset of UK Biobank participants to show the protective effects from physical activity on circadian disrupted individuals. △ Less

Submitted 16 November, 2020; originally announced November 2020.

Comments: 28 pages, 23 figures

Deep Learning for Individual Heterogeneity

Authors: Max H. Farrell, Tengyuan Liang, Sanjog Misra

Abstract: This paper integrates deep neural networks (DNNs) into structural economic models to increase flexibility and capture rich heterogeneity while preserving interpretability. Economic structure and machine learning are complements in empirical modeling, not substitutes: DNNs provide the capacity to learn complex, non-linear heterogeneity patterns, while the structural model ensures the estimates rema… ▽ More This paper integrates deep neural networks (DNNs) into structural economic models to increase flexibility and capture rich heterogeneity while preserving interpretability. Economic structure and machine learning are complements in empirical modeling, not substitutes: DNNs provide the capacity to learn complex, non-linear heterogeneity patterns, while the structural model ensures the estimates remain interpretable and suitable for decision making and policy analysis. We start with a standard parametric structural model and then enrich its parameters into fully flexible functions of observables, which are estimated using a particular DNN architecture whose structure reflects the economic model. We illustrate our framework by studying demand estimation in consumer choice. We show that by enriching a standard demand model we can capture rich heterogeneity, and further, exploit this heterogeneity to create a personalized pricing strategy. This type of optimization is not possible without economic structure, but cannot be heterogeneous without machine learning. Finally, we provide theoretical justification of each step in our proposed methodology. We first establish non-asymptotic bounds and convergence rates of our structural deep learning approach. Next, a novel and quite general influence function calculation allows for feasible inference via double machine learning in a wide variety of contexts. These results may be of interest in many other contexts, as they generalize prior work. △ Less

Submitted 24 April, 2025; v1 submitted 27 October, 2020; originally announced October 2020.

Rooting Formal Methods within Higher Education Curricula for Computer Science and Software Engineering -- A White Paper

Authors: Antonio Cerone, Markus Roggenbach, James Davenport, Casey Denner, Marie Farrell, Magne Haveraaen, Faron Moller, Philipp Koerner, Sebastian Krings, Peter Olveczky, Bernd-Holger Schlingloff, Nikolay Shilov, Rustam Zhumagambetov

Abstract: This white paper argues that formal methods need to be better rooted in higher education curricula for computer science and software engineering programmes of study. To this end, it advocates (i) improved teaching of formal methods; (ii) systematic highlighting of formal methods within existing, `classical' computer science courses; and (iii) the inclusion of a compulsory formal methods course in… ▽ More This white paper argues that formal methods need to be better rooted in higher education curricula for computer science and software engineering programmes of study. To this end, it advocates (i) improved teaching of formal methods; (ii) systematic highlighting of formal methods within existing, `classical' computer science courses; and (iii) the inclusion of a compulsory formal methods course in computer science and software engineering curricula. These recommendations are based on the observations that (a) formal methods are an essential and cost-effective means to increase software quality; however (b) computer science and software engineering programmes typically fail to provide adequate training in formal methods; and thus (c) there is a lack of computer science graduates who are qualified to apply formal methods in industry. This white paper is the result of a collective effort by authors and participants of the 1st International Workshop on "Formal Methods, Fun for Everybody" which was held in Bergen, Norway, 2-3 December 2019. As such, it represents insights based on learning and teaching computer science and software engineering (with or without formal methods) at various universities across Europe. △ Less

Submitted 12 October, 2020; originally announced October 2020.

Heterogeneous Verification of an Autonomous Curiosity Rover

Authors: Rafael C. Cardoso, Marie Farrell, Matt Luckcuck, Angelo Ferrando, Michael Fisher

Abstract: The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to th… ▽ More The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4--24 minutes for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance. △ Less

Submitted 20 July, 2020; originally announced July 2020.

Regulating Safety and Security in Autonomous Robotic Systems

Authors: Matt Luckcuck, Marie Farrell

Abstract: Autonomous Robotics Systems are inherently safety-critical and have complex safety issues to consider (for example, a safety failure can lead to a safety failure). Before they are deployed, these systems of have to show evidence that they adhere to a set of regulator-defined rules for safety and security. Formal methods provide robust approaches to proving a system obeys given rules, but formalisi… ▽ More Autonomous Robotics Systems are inherently safety-critical and have complex safety issues to consider (for example, a safety failure can lead to a safety failure). Before they are deployed, these systems of have to show evidence that they adhere to a set of regulator-defined rules for safety and security. Formal methods provide robust approaches to proving a system obeys given rules, but formalising (usually natural language) rules can prove difficult. Regulations specifically for autonomous systems are still being developed, but the safety rules for a human operator are a good starting point when trying to show that an autonomous system is safe. For applications of autonomous systems like driverless cars and pilotless aircraft, there are clear rules for human operators, which have been formalised and used to prove that an autonomous system obeys some or all of these rules. However, in the space and nuclear sectors applications are more likely to differ, so a set of general safety principles has developed. This allows novel applications to be assessed for their safety, but are difficult to formalise. To improve this situation, we are collaborating with regulators and the community in the space and nuclear sectors to develop guidelines for autonomous and robotic systems that are amenable to robust (formal) verification. These activities also have the benefit of bridging the gaps in knowledge within both the space or nuclear communities and academia. △ Less

Submitted 9 July, 2020; originally announced July 2020.

Comments: Experience Report, reported in BCS FACS Facts

Modular Verification of Autonomous Space Robotics

Authors: Marie Farrell, Rafael C. Cardoso, Louise A. Dennis, Clare Dixon, Michael Fisher, Georgios Kourtis, Alexei Lisitsa, Matt Luckcuck, Matt Webster

Abstract: Ensuring that autonomous space robot control software behaves as it should is crucial, particularly as software failure in space often equates to mission failure and could potentially endanger nearby astronauts and costly equipment. To minimise mission failure caused by software errors, we can utilise a variety of tools and techniques to verify that the software behaves as intended. In particular,… ▽ More Ensuring that autonomous space robot control software behaves as it should is crucial, particularly as software failure in space often equates to mission failure and could potentially endanger nearby astronauts and costly equipment. To minimise mission failure caused by software errors, we can utilise a variety of tools and techniques to verify that the software behaves as intended. In particular, distinct nodes in a robotic system often require different verification techniques to ensure that they behave as expected. This paper introduces a method for integrating the various verification techniques that are applied to robotic software, via a First-Order Logic (FOL) specification that captures each node's assumptions and guarantees. These FOL specifications are then used to guide the verification of the individual nodes, be it by testing or the use of a formal method. We also outline a way of measuring our confidence in the verification of the entire system in terms of the verification techniques used. △ Less

Submitted 28 August, 2019; originally announced August 2019.

Dimensionality compression and expansion in Deep Neural Networks

Authors: Stefano Recanatesi, Matthew Farrell, Madhu Advani, Timothy Moore, Guillaume Lajoie, Eric Shea-Brown

Abstract: Datasets such as images, text, or movies are embedded in high-dimensional spaces. However, in important cases such as images of objects, the statistical structure in the data constrains samples to a manifold of dramatically lower dimensionality. Learning to identify and extract task-relevant variables from this embedded manifold is crucial when dealing with high-dimensional problems. We find that… ▽ More Datasets such as images, text, or movies are embedded in high-dimensional spaces. However, in important cases such as images of objects, the statistical structure in the data constrains samples to a manifold of dramatically lower dimensionality. Learning to identify and extract task-relevant variables from this embedded manifold is crucial when dealing with high-dimensional problems. We find that neural networks are often very effective at solving this task and investigate why. To this end, we apply state-of-the-art techniques for intrinsic dimensionality estimation to show that neural networks learn low-dimensional manifolds in two phases: first, dimensionality expansion driven by feature generation in initial layers, and second, dimensionality compression driven by the selection of task-relevant features in later layers. We model noise generated by Stochastic Gradient Descent and show how this noise balances the dimensionality of neural representations by inducing an effective regularization term in the loss. We highlight the important relationship between low-dimensional compressed representations and generalization properties of the network. Our work contributes by shedding light on the success of deep neural networks in disentangling data in high-dimensional space while achieving good generalization. Furthermore, it invites new learning strategies focused on optimizing measurable geometric properties of learned representations, beginning with their intrinsic dimensionality. △ Less

Submitted 27 October, 2019; v1 submitted 2 June, 2019; originally announced June 2019.

Comments: Submitted to NeurIPS 2019. First two authors contributed equally

lspartition: Partitioning-Based Least Squares Regression

Authors: Matias D. Cattaneo, Max H. Farrell, Yingjie Feng

Abstract: Nonparametric partitioning-based least squares regression is an important tool in empirical work. Common examples include regressions based on splines, wavelets, and piecewise polynomials. This article discusses the main methodological and numerical features of the R software package lspartition, which implements modern estimation and inference results for partitioning-based least squares (series)… ▽ More Nonparametric partitioning-based least squares regression is an important tool in empirical work. Common examples include regressions based on splines, wavelets, and piecewise polynomials. This article discusses the main methodological and numerical features of the R software package lspartition, which implements modern estimation and inference results for partitioning-based least squares (series) regression estimation. This article discusses the main methodological and numerical features of the R software package lspartition, which implements results for partitioning-based least squares (series) regression estimation and inference from Cattaneo and Farrell (2013) and Cattaneo, Farrell, and Feng (2019). These results cover the multivariate regression function as well as its derivatives. First, the package provides data-driven methods to choose the number of partition knots optimally, according to integrated mean squared error, yielding optimal point estimation. Second, robust bias correction is implemented to combine this point estimator with valid inference. Third, the package provides estimates and inference for the unknown function both pointwise and uniformly in the conditioning variables. In particular, valid confidence bands are provided. Finally, an extension to two-sample analysis is developed, which can be used in treatment-control comparisons and related problems △ Less

Submitted 8 August, 2019; v1 submitted 1 June, 2019; originally announced June 2019.

Journal ref: R Journal 12(1): 172-187, 2020

nprobust: Nonparametric Kernel-Based Estimation and Robust Bias-Corrected Inference

Authors: Sebastian Calonico, Matias D. Cattaneo, Max H. Farrell

Abstract: Nonparametric kernel density and local polynomial regression estimators are very popular in Statistics, Economics, and many other disciplines. They are routinely employed in applied work, either as part of the main empirical analysis or as a preliminary ingredient entering some other estimation or inference procedure. This article describes the main methodological and numerical features of the sof… ▽ More Nonparametric kernel density and local polynomial regression estimators are very popular in Statistics, Economics, and many other disciplines. They are routinely employed in applied work, either as part of the main empirical analysis or as a preliminary ingredient entering some other estimation or inference procedure. This article describes the main methodological and numerical features of the software package nprobust, which offers an array of estimation and inference procedures for nonparametric kernel-based density and local polynomial regression methods, implemented in both the R and Stata statistical platforms. The package includes not only classical bandwidth selection, estimation, and inference methods (Wand and Jones, 1995; Fan and Gijbels, 1996), but also other recent developments in the statistics and econometrics literatures such as robust bias-corrected inference and coverage error optimal bandwidth selection (Calonico, Cattaneo and Farrell, 2018, 2019). Furthermore, this article also proposes a simple way of estimating optimal bandwidths in practice that always delivers the optimal mean square error convergence rate regardless of the specific evaluation point, that is, no matter whether it is implemented at a boundary or interior point. Numerical performance is illustrated using an empirical application and simulated data, where a detailed numerical comparison with other R packages is given. △ Less

Submitted 1 June, 2019; originally announced June 2019.

Journal ref: Journal of Statistical Software, 91(8): 1-33, 2019

The R-Process Alliance: Discovery of a low-alpha, r-Process-Enhanced Metal-Poor Star in the Galactic Halo

Authors: Charli M. Sakari, Ian U. Roederer, Vinicius M. Placco, Timothy C. Beers, Rana Ezzeddine, Anna Frebel, Terese Hansen, Christopher Sneden, John J. Cowan, George Wallerstein, Elizabeth M. Farrell, Kim A. Venn, Gal Matijevic, Rosemary F. G. Wyse, Joss Bland-Hawthorn, Cristina Chiappini, Kenneth C. Freeman, Brad K. Gibson, Eva K. Grebel, Amina Helmi, Georges Kordopatis, Andrea Kunder, Julio Navarro, Warren Reid, George Seabroke , et al. (2 additional authors not shown)

Abstract: A new moderately r-process-enhanced metal-poor star, RAVE J093730.5-062655, has been identified in the Milky Way halo as part of an ongoing survey by the R-Process Alliance. The temperature and surface gravity indicate that J0937-0626 is likely a horizontal branch star. At [Fe/H] = -1.86, J0937-0626 is found to have subsolar [X/Fe] ratios for nearly every light, alpha, and Fe-peak element. The low… ▽ More A new moderately r-process-enhanced metal-poor star, RAVE J093730.5-062655, has been identified in the Milky Way halo as part of an ongoing survey by the R-Process Alliance. The temperature and surface gravity indicate that J0937-0626 is likely a horizontal branch star. At [Fe/H] = -1.86, J0937-0626 is found to have subsolar [X/Fe] ratios for nearly every light, alpha, and Fe-peak element. The low [alpha/Fe] ratios can be explained by an ~0.6 dex excess of Fe; J0937-0626 is therefore similar to the subclass of "iron-enhanced" metal-poor stars. A comparison with Milky Way field stars at [Fe/H] = -2.5 suggests that J0937-0626 was enriched in material from an event, possibly a Type Ia supernova, that created a significant amount of Cr, Mn, Fe, and Ni and smaller amounts of Ca, Sc, Ti, and Zn. The r-process enhancement of J0937-0626 is likely due to a separate event, which suggests that its birth environment was highly enriched in r-process elements. The kinematics of J0937-0626, based on Gaia DR2 data, indicate a retrograde orbit in the Milky Way halo; J0937-0626 was therefore likely accreted from a dwarf galaxy that had significant r-process enrichment. △ Less

Submitted 4 March, 2019; originally announced March 2019.

Comments: Accepted for publication in the Astrophysical Journal

Binscatter Regressions

Authors: Matias D. Cattaneo, Richard K. Crump, Max H. Farrell, Yingjie Feng

Abstract: We introduce the package Binsreg, which implements the binscatter methods developed by Cattaneo, Crump, Farrell, and Feng (2024b,a). The package includes seven commands: binsreg, binslogit, binsprobit, binsqreg, binstest, binspwc, and binsregselect. The first four commands implement binscatter plotting, point estimation, and uncertainty quantification (confidence intervals and confidence bands) fo… ▽ More We introduce the package Binsreg, which implements the binscatter methods developed by Cattaneo, Crump, Farrell, and Feng (2024b,a). The package includes seven commands: binsreg, binslogit, binsprobit, binsqreg, binstest, binspwc, and binsregselect. The first four commands implement binscatter plotting, point estimation, and uncertainty quantification (confidence intervals and confidence bands) for least squares linear binscatter regression (binsreg) and for nonlinear binscatter regression (binslogit for Logit regression, binsprobit for Probit regression, and binsqreg for quantile regression). The next two commands focus on pointwise and uniform inference: binstest implements hypothesis testing procedures for parametric specifications and for nonparametric shape restrictions of the unknown regression function, while binspwc implements multi-group pairwise statistical comparisons. Finally, the command binsregselect implements data-driven number of bins selectors. The commands offer binned scatter plots, and allow for covariate adjustment, weighting, clustering, and multi-sample analysis, which is useful when studying treatment effect heterogeneity in randomized and observational studies, among many other features. △ Less

Submitted 24 July, 2024; v1 submitted 25 February, 2019; originally announced February 2019.

On Binscatter

Authors: Matias D. Cattaneo, Richard K. Crump, Max H. Farrell, Yingjie Feng

Abstract: Binscatter is a popular method for visualizing bivariate relationships and conducting informal specification testing. We study the properties of this method formally and develop enhanced visualization and econometric binscatter tools. These include estimating conditional means with optimal binning and quantifying uncertainty. We also highlight a methodological problem related to covariate adjustme… ▽ More Binscatter is a popular method for visualizing bivariate relationships and conducting informal specification testing. We study the properties of this method formally and develop enhanced visualization and econometric binscatter tools. These include estimating conditional means with optimal binning and quantifying uncertainty. We also highlight a methodological problem related to covariate adjustment that can yield incorrect conclusions. We revisit two applications using our methodology and find substantially different results relative to those obtained using prior informal binscatter methods. General purpose software in Python, R, and Stata is provided. Our technical work is of independent interest for the nonparametric partition-based estimation literature. △ Less

Submitted 30 April, 2024; v1 submitted 25 February, 2019; originally announced February 2019.

Journal ref: American Economic Review, 114(5) 1488-1514, 2024

Kinematics of Type II Cepheids of the Galactic Halo

Authors: George Wallerstein, Elizabeth M. Farrell

Abstract: In a step toward understanding the origin of the Galactic Halo, we have reexamined Type II Cepheids (T2C) in the field with new input from the second data release (DR2) of Gaia. For 45 T2C with periods from 1 to 20 days, parallaxes, proper motions, and [Fe/H] values are available for 25 stars. Only 5 show [Fe/H] < -1.5, while the remaining stars show thick disk kinematics and [Fe/H] > -0.90. We ha… ▽ More In a step toward understanding the origin of the Galactic Halo, we have reexamined Type II Cepheids (T2C) in the field with new input from the second data release (DR2) of Gaia. For 45 T2C with periods from 1 to 20 days, parallaxes, proper motions, and [Fe/H] values are available for 25 stars. Only 5 show [Fe/H] < -1.5, while the remaining stars show thick disk kinematics and [Fe/H] > -0.90. We have compared the T2C stars of the field with their cousins in the globular clusters of the Halo and found that the globular clusters with T2C stars show metallicities and kinematics of a pure Halo population. The globulars may have formed during the overall collapse of the Galaxy while the individual thick disk T2C stars may have been captured from small systems that self-enriched prior to capture. The relationship of these two populations to the micro-galaxies currently recognized as surrounding the Galaxy is unclear. △ Less

Submitted 5 November, 2018; originally announced November 2018.

Comments: 7 pages, 3 figures, 4 tables

Deep Neural Networks for Estimation and Inference

Authors: Max H. Farrell, Tengyuan Liang, Sanjog Misra

Abstract: We study deep neural networks and their use in semiparametric inference. We establish novel rates of convergence for deep feedforward neural nets. Our new rates are sufficiently fast (in some cases minimax optimal) to allow us to establish valid second-step inference after first-step estimation with deep learning, a result also new to the literature. Our estimation rates and semiparametric inferen… ▽ More We study deep neural networks and their use in semiparametric inference. We establish novel rates of convergence for deep feedforward neural nets. Our new rates are sufficiently fast (in some cases minimax optimal) to allow us to establish valid second-step inference after first-step estimation with deep learning, a result also new to the literature. Our estimation rates and semiparametric inference results handle the current standard architecture: fully connected feedforward neural networks (multi-layer perceptrons), with the now-common rectified linear unit activation function and a depth explicitly diverging with the sample size. We discuss other architectures as well, including fixed-width, very deep networks. We establish nonasymptotic bounds for these deep nets for a general class of nonparametric regression-type loss functions, which includes as special cases least squares, logistic regression, and other generalized linear models. We then apply our theory to develop semiparametric inference, focusing on causal parameters for concreteness, such as treatment effects, expected welfare, and decomposition effects. Inference in many other semiparametric contexts can be readily obtained. We demonstrate the effectiveness of deep learning with a Monte Carlo analysis and an empirical application to direct mail marketing. △ Less

Submitted 18 September, 2019; v1 submitted 26 September, 2018; originally announced September 2018.

Journal ref: Econometrica, vol 89, no 1, 181-213, 2021

The R-Process Alliance: First Release from the Northern Search for r-Process Enhanced Metal-Poor Stars in the Galactic Halo

Authors: Charli M. Sakari, Vinicius M. Placco, Elizabeth M. Farrell, Ian U. Roederer, George Wallerstein, Timothy C. Beers, Rana Ezzeddine, Anna Frebel, Terese Hansen, Erika M. Holmbeck, Christopher Sneden, John J. Cowan, Kim A. Venn, Christopher Evan Davis, Gal Matijevic, Rosemary F. G. Wyse, Joss Bland-Hawthorn, Cristina Chiappini, Kenneth C. Freeman, Brad K. Gibson, Eva K. Grebel, Amina Helmi, Georges Kordopatis, Andrea Kunder, Julio Navarro , et al. (4 additional authors not shown)

Abstract: This paper presents the detailed abundances and r-process classifications of 126 newly identified metal-poor stars as part of an ongoing collaboration, the R-Process Alliance. The stars were identified as metal-poor candidates from the RAdial Velocity Experiment (RAVE) and were followed-up at high spectral resolution (R~31,500) with the 3.5~m telescope at Apache Point Observatory. The atmospheric… ▽ More This paper presents the detailed abundances and r-process classifications of 126 newly identified metal-poor stars as part of an ongoing collaboration, the R-Process Alliance. The stars were identified as metal-poor candidates from the RAdial Velocity Experiment (RAVE) and were followed-up at high spectral resolution (R~31,500) with the 3.5~m telescope at Apache Point Observatory. The atmospheric parameters were determined spectroscopically from Fe I lines, taking into account <3D> non-LTE corrections and using differential abundances with respect to a set of standards. Of the 126 new stars, 124 have [Fe/H]<-1.5, 105 have [Fe/H]<-2.0, and 4 have [Fe/H]<-3.0. Nine new carbon-enhanced metal-poor stars have been discovered, 3 of which are enhanced in r-process elements. Abundances of neutron-capture elements reveal 60 new r-I stars (with +0.3<=[Eu/Fe]<=+1.0 and [Ba/Eu]<0) and 4 new r-II stars (with [Eu/Fe]>+1.0). Nineteen stars are found to exhibit a `limited-r' signature ([Sr/Ba]>+0.5, [Ba/Eu]<0). For the r-II stars, the second- and third-peak main r-process patterns are consistent with the r-process signature in other metal-poor stars and the Sun. The abundances of the light, alpha, and Fe-peak elements match those of typical Milky Way halo stars, except for one r-I star which has high Na and low Mg, characteristic of globular cluster stars. Parallaxes and proper motions from the second Gaia data release yield UVW space velocities for these stars which are consistent with membership in the Milky Way halo. Intriguingly, all r-II and the majority of r-I stars have retrograde orbits, which may indicate an accretion origin. △ Less

Submitted 22 October, 2018; v1 submitted 24 September, 2018; originally announced September 2018.

Comments: Accepted for publication in the Astrophysical Journal

Regression Discontinuity Designs Using Covariates

Authors: Sebastian Calonico, Matias D. Cattaneo, Max H. Farrell, Rocio Titiunik

Abstract: We study regression discontinuity designs when covariates are included in the estimation. We examine local polynomial estimators that include discrete or continuous covariates in an additive separable way, but without imposing any parametric restrictions on the underlying population regression functions. We recommend a covariate-adjustment approach that retains consistency under intuitive conditio… ▽ More We study regression discontinuity designs when covariates are included in the estimation. We examine local polynomial estimators that include discrete or continuous covariates in an additive separable way, but without imposing any parametric restrictions on the underlying population regression functions. We recommend a covariate-adjustment approach that retains consistency under intuitive conditions, and characterize the potential for estimation and inference improvements. We also present new covariate-adjusted mean squared error expansions and robust bias-corrected inference procedures, with heteroskedasticity-consistent and cluster-robust standard errors. An empirical illustration and an extensive simulation study is presented. All methods are implemented in \texttt{R} and \texttt{Stata} software packages. △ Less

Submitted 11 September, 2018; originally announced September 2018.

Journal ref: Review of Economics and Statistics, 101(3), 442--451, 2019

Characteristic-Sorted Portfolios: Estimation and Inference

Authors: Matias D. Cattaneo, Richard K. Crump, Max H. Farrell, Ernst Schaumburg

Abstract: Portfolio sorting is ubiquitous in the empirical finance literature, where it has been widely used to identify pricing anomalies. Despite its popularity, little attention has been paid to the statistical properties of the procedure. We develop a general framework for portfolio sorting by casting it as a nonparametric estimator. We present valid asymptotic inference methods and a valid mean square… ▽ More Portfolio sorting is ubiquitous in the empirical finance literature, where it has been widely used to identify pricing anomalies. Despite its popularity, little attention has been paid to the statistical properties of the procedure. We develop a general framework for portfolio sorting by casting it as a nonparametric estimator. We present valid asymptotic inference methods and a valid mean square error expansion of the estimator leading to an optimal choice for the number of portfolios. In practical settings, the optimal choice may be much larger than the standard choices of 5 or 10. To illustrate the relevance of our results, we revisit the size and momentum anomalies. △ Less

Submitted 5 October, 2019; v1 submitted 10 September, 2018; originally announced September 2018.

Journal ref: Review of Economics and Statistics, 102(3), 531--551, 2020

Optimal Bandwidth Choice for Robust Bias Corrected Inference in Regression Discontinuity Designs

Authors: Sebastian Calonico, Matias D. Cattaneo, Max H. Farrell

Abstract: Modern empirical work in Regression Discontinuity (RD) designs often employs local polynomial estimation and inference with a mean square error (MSE) optimal bandwidth choice. This bandwidth yields an MSE-optimal RD treatment effect estimator, but is by construction invalid for inference. Robust bias corrected (RBC) inference methods are valid when using the MSE-optimal bandwidth, but we show they… ▽ More Modern empirical work in Regression Discontinuity (RD) designs often employs local polynomial estimation and inference with a mean square error (MSE) optimal bandwidth choice. This bandwidth yields an MSE-optimal RD treatment effect estimator, but is by construction invalid for inference. Robust bias corrected (RBC) inference methods are valid when using the MSE-optimal bandwidth, but we show they yield suboptimal confidence intervals in terms of coverage error. We establish valid coverage error expansions for RBC confidence interval estimators and use these results to propose new inference-optimal bandwidth choices for forming these intervals. We find that the standard MSE-optimal bandwidth for the RD point estimator is too large when the goal is to construct RBC confidence intervals with the smallest coverage error. We further optimize the constant terms behind the coverage error to derive new optimal choices for the auxiliary bandwidth required for RBC inference. Our expansions also establish that RBC inference yields higher-order refinements (relative to traditional undersmoothing) in the context of RD designs. Our main results cover sharp and sharp kink RD designs under conditional heteroskedasticity, and we discuss extensions to fuzzy and other RD designs, clustered sampling, and pre-intervention covariates adjustments. The theoretical findings are illustrated with a Monte Carlo experiment and an empirical application, and the main methodological results are available in \texttt{R} and \texttt{Stata} packages. △ Less

Submitted 2 January, 2020; v1 submitted 1 September, 2018; originally announced September 2018.

Journal ref: Econometrics Journal, 23(2), 192--210, 2020

Coverage Error Optimal Confidence Intervals for Local Polynomial Regression

Authors: Sebastian Calonico, Matias D. Cattaneo, Max H. Farrell

Abstract: This paper studies higher-order inference properties of nonparametric local polynomial regression methods under random sampling. We prove Edgeworth expansions for $t$ statistics and coverage error expansions for interval estimators that (i) hold uniformly in the data generating process, (ii) allow for the uniform kernel, and (iii) cover estimation of derivatives of the regression function. The ter… ▽ More This paper studies higher-order inference properties of nonparametric local polynomial regression methods under random sampling. We prove Edgeworth expansions for $t$ statistics and coverage error expansions for interval estimators that (i) hold uniformly in the data generating process, (ii) allow for the uniform kernel, and (iii) cover estimation of derivatives of the regression function. The terms of the higher-order expansions, and their associated rates as a function of the sample size and bandwidth sequence, depend on the smoothness of the population regression function, the smoothness exploited by the inference procedure, and on whether the evaluation point is in the interior or on the boundary of the support. We prove that robust bias corrected confidence intervals have the fastest coverage error decay rates in all cases, and we use our results to deliver novel, inference-optimal bandwidth selectors. The main methodological results are implemented in companion \textsf{R} and \textsf{Stata} software packages. △ Less

Submitted 23 July, 2021; v1 submitted 3 August, 2018; originally announced August 2018.

Formal Specification and Verification of Autonomous Robotic Systems: A Survey

Authors: Matt Luckcuck, Marie Farrell, Louise Dennis, Clare Dixon, Michael Fisher

Abstract: Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics has received some attention in th… ▽ More Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics has received some attention in the literature, but no resource provides a current overview. This paper systematically surveys the state-of-the-art in formal specification and verification for autonomous robotics. Specially, it identifies and categorises the challenges posed by, the formalisms aimed at, and the formal approaches for the specification and verification of autonomous robotics. △ Less

Submitted 1 May, 2019; v1 submitted 29 June, 2018; originally announced July 2018.

Comments: 32 pages (in this format) resubmitted to ACM CSUR

Journal ref: ACM Computing Surveys, Volume 52, Issue 5, (2019) Article No.: 100, pp 1-41

Robotics and Integrated Formal Methods: Necessity meets Opportunity

Authors: Marie Farrell, Matt Luckcuck, Michael Fisher

Abstract: Robotic systems are multi-dimensional entities, combining both hardware and software, that are heavily dependent on, and influenced by, interactions with the real world. They can be variously categorised as embedded, cyberphysical, real-time, hybrid, adaptive and even autonomous systems, with a typical robotic system being likely to contain all of these aspects. The techniques for developing and v… ▽ More Robotic systems are multi-dimensional entities, combining both hardware and software, that are heavily dependent on, and influenced by, interactions with the real world. They can be variously categorised as embedded, cyberphysical, real-time, hybrid, adaptive and even autonomous systems, with a typical robotic system being likely to contain all of these aspects. The techniques for developing and verifying each of these system varieties are often quite distinct. This, together with the sheer complexity of robotic systems, leads us to argue that diverse formal techniques must be integrated in order to develop, verify, and provide certification evidence for, robotic systems. Furthermore, we propose the fast evolving field of robotics as an ideal catalyst for the advancement of integrated formal methods research, helping to drive the field in new and exciting directions and shedding light on the development of large-scale, dynamic, complex systems. △ Less

Submitted 3 September, 2018; v1 submitted 2 May, 2018; originally announced May 2018.

Comments: 10 Pages, accepted at iFM2018: https://link.springer.com/chapter/10.1007/978-3-319-98938-9_10