-
Reinforcement Learning and Machine ethics:a systematic review
Authors:
Ajay Vishwanath,
Louise A. Dennis,
Marija Slavkovik
Abstract:
Machine ethics is the field that studies how ethical behaviour can be accomplished by autonomous systems. While there exist some systematic reviews aiming to consolidate the state of the art in machine ethics prior to 2020, these tend to not include work that uses reinforcement learning agents as entities whose ethical behaviour is to be achieved. The reason for this is that only in the last years…
▽ More
Machine ethics is the field that studies how ethical behaviour can be accomplished by autonomous systems. While there exist some systematic reviews aiming to consolidate the state of the art in machine ethics prior to 2020, these tend to not include work that uses reinforcement learning agents as entities whose ethical behaviour is to be achieved. The reason for this is that only in the last years we have witnessed an increase in machine ethics studies within reinforcement learning. We present here a systematic review of reinforcement learning for machine ethics and machine ethics within reinforcement learning. Additionally, we highlight trends in terms of ethics specifications, components and frameworks of reinforcement learning, and environments used to result in ethical behaviour. Our systematic review aims to consolidate the work in machine ethics and reinforcement learning thus completing the gap in the state of the art machine ethics landscape
△ Less
Submitted 2 July, 2024;
originally announced July 2024.
-
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving
Authors:
Xin Quan,
Marco Valentino,
Louise A. Dennis,
André Freitas
Abstract:
Natural language explanations have become a proxy for evaluating explainable and multi-step Natural Language Inference (NLI) models. However, assessing the validity of explanations for NLI is challenging as it typically involves the crowd-sourcing of apposite datasets, a process that is time-consuming and prone to logical errors. To address existing limitations, this paper investigates the verific…
▽ More
Natural language explanations have become a proxy for evaluating explainable and multi-step Natural Language Inference (NLI) models. However, assessing the validity of explanations for NLI is challenging as it typically involves the crowd-sourcing of apposite datasets, a process that is time-consuming and prone to logical errors. To address existing limitations, this paper investigates the verification and refinement of natural language explanations through the integration of Large Language Models (LLMs) and Theorem Provers (TPs). Specifically, we present a neuro-symbolic framework, named Explanation-Refiner, that augments a TP with LLMs to generate and formalise explanatory sentences and suggest potential inference strategies for NLI. In turn, the TP is employed to provide formal guarantees on the logical validity of the explanations and to generate feedback for subsequent improvements. We demonstrate how Explanation-Refiner can be jointly used to evaluate explanatory reasoning, autoformalisation, and error correction mechanisms of state-of-the-art LLMs as well as to automatically enhance the quality of human-annotated explanations of variable complexity in different domains.
△ Less
Submitted 7 May, 2024; v1 submitted 2 May, 2024;
originally announced May 2024.
-
Specifying Agent Ethics (Blue Sky Ideas)
Authors:
Louise A. Dennis,
Michael Fisher
Abstract:
We consider the question of what properties a Machine Ethics system should have. This question is complicated by the existence of ethical dilemmas with no agreed upon solution. We provide an example to motivate why we do not believe falling back on the elicitation of values from stakeholders is sufficient to guarantee correctness of such systems. We go on to define two broad categories of ethical…
▽ More
We consider the question of what properties a Machine Ethics system should have. This question is complicated by the existence of ethical dilemmas with no agreed upon solution. We provide an example to motivate why we do not believe falling back on the elicitation of values from stakeholders is sufficient to guarantee correctness of such systems. We go on to define two broad categories of ethical property that have arisen in our own work and present a challenge to the community to approach this question in a more systematic way.
△ Less
Submitted 24 March, 2024;
originally announced March 2024.
-
Generating Uniform Magnetic Fields Using Pulse Field Magnetisation
Authors:
Dian Weerakonda,
Benjamin Bryant,
Anthony Dennis,
Tobia Nava,
John Durrell
Abstract:
Bulk high-temperature superconductors (HTS) are capable of generating very strong magnetic fields while maintaining a relatively compact form factor. Solenoids constructed using stacks of ring-shaped bulk HTS have been demonstrated to be capable of nuclear magnetic resonance (NMR) spectroscopy and magnetic resonance imaging (MRI). However, these stacks were magnetised via field cooling (FC), which…
▽ More
Bulk high-temperature superconductors (HTS) are capable of generating very strong magnetic fields while maintaining a relatively compact form factor. Solenoids constructed using stacks of ring-shaped bulk HTS have been demonstrated to be capable of nuclear magnetic resonance (NMR) spectroscopy and magnetic resonance imaging (MRI). However, these stacks were magnetised via field cooling (FC), which typically requires a secondary superconducting charging magnet capable of sustaining a high magnetic field for a long period. A more economical alternative to FC is pulsed field magnetisation, which can be carried out with a magnet wound from a normal conductor, such as copper. In this work, we present a technique we have developed for iteratively homogenising the magnetic field within a stack of ring-shaped bulk HTS by manipulating the spatial profile of the applied pulsed field.
△ Less
Submitted 14 February, 2024;
originally announced February 2024.
-
Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement
Authors:
Xin Quan,
Marco Valentino,
Louise A. Dennis,
André Freitas
Abstract:
An increasing amount of research in Natural Language Inference (NLI) focuses on the application and evaluation of Large Language Models (LLMs) and their reasoning capabilities. Despite their success, however, LLMs are still prone to factual errors and inconsistencies in their explanations, offering limited control and interpretability for inference in complex domains. In this paper, we focus on et…
▽ More
An increasing amount of research in Natural Language Inference (NLI) focuses on the application and evaluation of Large Language Models (LLMs) and their reasoning capabilities. Despite their success, however, LLMs are still prone to factual errors and inconsistencies in their explanations, offering limited control and interpretability for inference in complex domains. In this paper, we focus on ethical NLI, investigating how hybrid neuro-symbolic techniques can enhance the logical validity and alignment of ethical explanations produced by LLMs. Specifically, we present an abductive-deductive framework named Logic-Explainer, which integrates LLMs with an external backward-chaining solver to refine step-wise natural language explanations and jointly verify their correctness, reduce incompleteness and minimise redundancy. An extensive empirical analysis demonstrates that Logic-Explainer can improve explanations generated via in-context learning methods and Chain-of-Thought (CoT) on challenging ethical NLI tasks, while, at the same time, producing formal proofs describing and supporting models' reasoning. As ethical NLI requires commonsense reasoning to identify underlying moral violations, our results suggest the effectiveness of neuro-symbolic methods for multi-step NLI more broadly, opening new opportunities to enhance the logical consistency, reliability, and alignment of LLMs.
△ Less
Submitted 1 February, 2024;
originally announced February 2024.
-
Autonomous Systems' Safety Cases for use in UK Nuclear Environments
Authors:
Christopher R. Anderson,
Louise A. Dennis
Abstract:
An overview of the process to develop a safety case for an autonomous robot deployment on a nuclear site in the UK is described and a safety case for a hypothetical robot incorporating AI is presented. This forms a first step towards a deployment, showing what is possible now and what may be possible with development of tools. It forms the basis for further discussion between nuclear site licensee…
▽ More
An overview of the process to develop a safety case for an autonomous robot deployment on a nuclear site in the UK is described and a safety case for a hypothetical robot incorporating AI is presented. This forms a first step towards a deployment, showing what is possible now and what may be possible with development of tools. It forms the basis for further discussion between nuclear site licensees, the Office for Nuclear Regulation (ONR), industry and academia.
△ Less
Submitted 3 October, 2023;
originally announced October 2023.
-
Modelling Cosmic Radiation Events in the Tree-ring Radiocarbon Record
Authors:
Qingyuan Zhang,
Utkarsh Sharma,
Jordan A. Dennis,
Andrea Scifo,
Margot Kuitems,
Ulf Buentgen,
Mathew J. Owens,
Michael W. Dee,
Benjamin J. S. Pope
Abstract:
Annually-resolved measurements of the radiocarbon content in tree-rings have revealed rare sharp rises in carbon-14 production. These 'Miyake events' are likely produced by rare increases in cosmic radiation from the Sun or other energetic astrophysical sources. The radiocarbon produced is not only circulated through the Earth's atmosphere and oceans, but also absorbed by the biosphere and locked…
▽ More
Annually-resolved measurements of the radiocarbon content in tree-rings have revealed rare sharp rises in carbon-14 production. These 'Miyake events' are likely produced by rare increases in cosmic radiation from the Sun or other energetic astrophysical sources. The radiocarbon produced is not only circulated through the Earth's atmosphere and oceans, but also absorbed by the biosphere and locked in the annual growth rings of trees. To interpret high-resolution tree-ring radiocarbon measurements therefore necessitates modelling the entire global carbon cycle. Here, we introduce 'ticktack', the first open-source Python package that connects box models of the carbon cycle with modern Bayesian inference tools. We use this to analyse all public annual 14C tree data, and infer posterior parameters for all six known Miyake events. They do not show a consistent relationship to the solar cycle, and several display extended durations that challenge either astrophysical or geophysical models.
△ Less
Submitted 25 October, 2022;
originally announced October 2022.
-
Advising Autonomous Cars about the Rules of the Road
Authors:
Joe Collenette,
Louise A. Dennis,
Michael Fisher
Abstract:
This paper describes (R)ules (o)f (T)he (R)oad (A)dvisor, an agent that provides recommended and possible actions to be generated from a set of human-level rules. We describe the architecture and design of RoTRA, both formally and with an example. Specifically, we use RoTRA to formalise and implement the UK "Rules of the Road", and describe how this can be incorporated into autonomous cars such…
▽ More
This paper describes (R)ules (o)f (T)he (R)oad (A)dvisor, an agent that provides recommended and possible actions to be generated from a set of human-level rules. We describe the architecture and design of RoTRA, both formally and with an example. Specifically, we use RoTRA to formalise and implement the UK "Rules of the Road", and describe how this can be incorporated into autonomous cars such that they can reason internally about obeying the rules of the road. In addition, the possible actions generated are annotated to indicate whether the rules state that the action must be taken or that they only recommend that the action should be taken, as per the UK Highway Code (Rules of The Road). The benefits of utilising this system include being able to adapt to different regulations in different jurisdictions; allowing clear traceability from rules to behaviour, and providing an external automated accountability mechanism that can check whether the rules were obeyed in some given situation. A simulation of an autonomous car shows, via a concrete example, how trust can be built by putting the autonomous vehicle through a number of scenarios which test the car's ability to obey the rules of the road. Autonomous cars that incorporate this system are able to ensure that they are obeying the rules of the road and external (legal or regulatory) bodies can verify that this is the case, without the vehicle or its manufacturer having to expose their source code or make their working transparent, thus allowing greater trust between car companies, jurisdictions, and the general public.
△ Less
Submitted 28 September, 2022;
originally announced September 2022.
-
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.
-
Proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy
Authors:
Rafael C. Cardoso,
Angelo Ferrando,
Fabio Papacchini,
Mehrnoosh Askarpour,
Louise A. Dennis
Abstract:
This volume contains the proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2022), co-located with the 31st International Joint Conference on Artificial Intelligence and the 25th European Conference on Artificial Intelligence (IJCAI-ECAI 2022). The AREA workshop brings together researchers from autonomous agents, software engineering and robotic communit…
▽ More
This volume contains the proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2022), co-located with the 31st International Joint Conference on Artificial Intelligence and the 25th European Conference on Artificial Intelligence (IJCAI-ECAI 2022). The AREA workshop brings together researchers from autonomous agents, software engineering and robotic communities, as combining knowledge coming from these research areas may lead to innovative approaches that solve complex problems related with the verification and validation of autonomous robotic systems.
△ Less
Submitted 19 July, 2022;
originally announced July 2022.
-
Electric Field Induced Macroscopic Cellular Phase of Nanoparticles
Authors:
Abigail Rendos,
Wenhan Cao,
Margaret Chern,
Marco Lauricella,
Sauro Succi,
Joerg G. Werner,
Allison M. Dennis,
Keith A. Brown
Abstract:
A suspension of nanoparticles with very low volume fraction is found to assemble into a macroscopic cellular phase under the collective influence of AC and DC voltages. Systematic study of this phase transition shows that it was the result of electrophoretic assembly into a two-dimensional configuration followed by spinodal decomposition into particle-rich walls and particle-poor cells mediated pr…
▽ More
A suspension of nanoparticles with very low volume fraction is found to assemble into a macroscopic cellular phase under the collective influence of AC and DC voltages. Systematic study of this phase transition shows that it was the result of electrophoretic assembly into a two-dimensional configuration followed by spinodal decomposition into particle-rich walls and particle-poor cells mediated principally by electrohydrodynamic flow. This mechanistic understanding reveals two characteristics needed for a cellular phase to form, namely 1) a system that is considered two dimensional and 2) short-range attractive, long-range repulsive interparticle interactions. In addition to determining the mechanism underpinning the formation of the cellular phase, this work presents a method to reversibly assemble microscale continuous structures out of nanoscale particles in a manner that may enable the creation of materials that impact diverse fields including energy storage and filtration.
△ Less
Submitted 30 November, 2021;
originally announced December 2021.
-
Electron vacancy-level dependent hybrid photoionization of F-@C60+ molecule
Authors:
Esam Ali,
Taylor O'Brien,
Andrew Dennis,
Mohamed El-Amine Madjet,
Steven T. Manson,
Himadri S. Chakraborty
Abstract:
Our previous studies [J. Phys. B 53, 125101 (2020); Euro. Phys. J. D 74, 191 (2020)] have predicted that the atom-fullerene hybrid photoionization properties for X = Cl, Br and I endohedrally confined in C60 are different before and after an electron transfers from C60 to the halogen. It was further found as a rule that the ionization dynamics is insensitive to the C60 level the electron originate…
▽ More
Our previous studies [J. Phys. B 53, 125101 (2020); Euro. Phys. J. D 74, 191 (2020)] have predicted that the atom-fullerene hybrid photoionization properties for X = Cl, Br and I endohedrally confined in C60 are different before and after an electron transfers from C60 to the halogen. It was further found as a rule that the ionization dynamics is insensitive to the C60 level the electron originates from to produce X-@C60+. In the current study, we report an exception to this rule in F@C60. It is found that when the electron vacancy is situated in the C60 level that participates in the hybridization in F-@C60+, the mixing becomes dramatically large leading to strong modifications in the photoionization of the hybrid levels. But when the vacancy is at any other pure level of C60, the level-invariance is retained showing weak hybridization. Even though this case of F@C60 is an anomaly in the halogen@C60 series, the phenomenon can be more general and can occur with compounds of other atoms caged in a variety of fullerenes. In addition, possible experimental studies are suggested to benchmark the present results.
△ Less
Submitted 4 June, 2021;
originally announced June 2021.
-
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.
-
Adaptable and Verifiable BDI Reasoning
Authors:
Peter Stringer,
Rafael C. Cardoso,
Xiaowei Huang,
Louise A. Dennis
Abstract:
Long-term autonomy requires autonomous systems to adapt as their capabilities no longer perform as expected. To achieve this, a system must first be capable of detecting such changes. In this position paper, we describe a system architecture for BDI autonomous agents capable of adapting to changes in a dynamic environment and outline the required research. Specifically, we describe an agent-mainta…
▽ More
Long-term autonomy requires autonomous systems to adapt as their capabilities no longer perform as expected. To achieve this, a system must first be capable of detecting such changes. In this position paper, we describe a system architecture for BDI autonomous agents capable of adapting to changes in a dynamic environment and outline the required research. Specifically, we describe an agent-maintained self-model with accompanying theories of durative actions and learning new action descriptions in BDI systems.
△ Less
Submitted 22 July, 2020;
originally announced July 2020.
-
A Summary of Formal Specification and Verification of Autonomous Robotic Systems
Authors:
Matt Luckcuck,
Marie Farrel,
Louise A. Dennis,
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 have received some attention in t…
▽ 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 have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions of Luckcuck 2019, which surveys the state-of-the-art in formal specification and verification for autonomous robotics.
△ Less
Submitted 25 November, 2019;
originally announced November 2019.
-
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.
-
Composite stacks for reliable > 17 T trapped fields in bulk superconductor magnets
Authors:
Kai Yuan Huang,
Yunhua Shi,
Jan Srpčič,
Mark D Ainslie,
Devendra K Namburi,
Anthony R Dennis,
Difan Zhou,
Martin Boll,
Mykhaylo Filipenko,
Jan Jaroszynski,
Eric E Hellstrom,
David A Cardwell,
John H Durrell
Abstract:
Trapped fields of over 20 T are, in principle, achievable in bulk, single-grain high temperature cuprate superconductors. The principle barriers to realizing such performance are, firstly, the large tensile stresses that develop during the magnetization of such trapped-field magnets as a result of the Lorentz force, which lead to brittle fracture of these ceramic-like materials at high fields and,…
▽ More
Trapped fields of over 20 T are, in principle, achievable in bulk, single-grain high temperature cuprate superconductors. The principle barriers to realizing such performance are, firstly, the large tensile stresses that develop during the magnetization of such trapped-field magnets as a result of the Lorentz force, which lead to brittle fracture of these ceramic-like materials at high fields and, secondly, catastrophic thermal instabilities as a result of flux movement during magnetization. Moreover, for a batch of samples nominally fabricated identically, the statistical nature of the failure mechanism means the best performance (i.e. trapped fields of over 17 T) cannot be attained reliably. The magnetization process, particularly to higher fields, also often damages the samples such that they cannot repeatedly trap high fields following subsequent magnetization. In this study, we report the sequential trap** of magnetic fields of ~ 17 T, achieving 16.8 T at 26 K initially and 17.6 T at 22.5 K subsequently, in a stack of two Ag-doped GdBa2Cu3O7-δ bulk superconductor composites of diameter 24 mm reinforced with (1) stainless-steel laminations, and (2) shrink-fit stainless steel rings. A trapped field of 17.6 T is, in fact, comparable with the highest trapped fields reported to date for bulk superconducting magnets of any mechanical and chemical composition, and this was achieved using the first composite stack to be fabricated by this technique.
△ Less
Submitted 3 December, 2019; v1 submitted 22 August, 2019;
originally announced August 2019.
-
Directed Non-Targeted Mass Spectrometry and Chemical Networking for Discovery of Eicosanoids
Authors:
Jeramie D. Watrous,
Teemu Niiranen,
Kim A. Lagerborg,
Mir Henglin,
Yong-Jian Xu,
Sonia Sharma,
Ramachandran S. Vasan,
Martin G. Larson,
Aaron Armando,
Oswald Quehenberger,
Edward A. Dennis,
Susan Cheng,
Mohit Jain
Abstract:
Eicosanoids and related species are critical, small bioactive mediators of human physiology and inflammation. While ~1100 distinct eicosanoids have been predicted to exist, to date, less than 150 of these molecules have been measured in humans, limiting our understanding of eicosanoids and their role in human biology. Using a directed non-targeted mass spectrometry approach in conjunction with com…
▽ More
Eicosanoids and related species are critical, small bioactive mediators of human physiology and inflammation. While ~1100 distinct eicosanoids have been predicted to exist, to date, less than 150 of these molecules have been measured in humans, limiting our understanding of eicosanoids and their role in human biology. Using a directed non-targeted mass spectrometry approach in conjunction with computational chemical networking of spectral fragmentation patterns, we find over 500 discrete chemical signals highly consistent with known and putative eicosanoids in human plasma, including 46 putative novel molecules not previously described, thereby greatly expanding the breath of prior analytical strategies. In plasma samples from 1500 individuals, we find members of this expanded eicosanoid library hold close association with markers of inflammation, as well as clinical characteristics linked with inflammation, including advancing age and obesity. These experimental and computational approaches enable discovery of new chemical entities and will shed important insight into the role of bioactive molecules in human disease.
△ Less
Submitted 4 June, 2018;
originally announced June 2018.
-
Demagnetization of cubic Gd-Ba-Cu-O bulk superconductor by cross-fields: measurements and 3D modelling
Authors:
M. Kapolka,
J. Srpcic,
D. Zhou,
M. Ainslie,
E. Pardo,
A. Dennis
Abstract:
Superconducting bulks, acting as high-field permanent magnets, are promising for many applications. An important effect in bulk permanent magnets is crossed-field demagnetization, which can reduce the magnetic field in superconductors due to relatively small transverse fields. Crossed-field demagnetization has not been studied in sample shapes such as rectangular prisms or cubes. This contribution…
▽ More
Superconducting bulks, acting as high-field permanent magnets, are promising for many applications. An important effect in bulk permanent magnets is crossed-field demagnetization, which can reduce the magnetic field in superconductors due to relatively small transverse fields. Crossed-field demagnetization has not been studied in sample shapes such as rectangular prisms or cubes. This contribution presents a study based on both 3D numerical modelling and experiments. We study a cubic Gd-Ba-Cu-O bulk superconductor sample of size 6 mm magnetized by field cooling in an external field of around 1.3 T, which is later submitted to crossed-field magnetic fields of up to 164 mT. Modelling results agree with experiments, except at transverse fields 50\% or above of the initial trapped field. The current paths present a strong 3D nature. For instance, at the mid-plane perpendicular to the initial magnetizing field, the current density in this direction changes smoothly from the critical magnitude, ${J_c}$, at the lateral sides to zero at a certain penetration depth. This indicates a rotation of the current density with magnitude ${J_c}$, and hence force free effects like flux cutting are expected to play a significant role.
△ Less
Submitted 21 March, 2018; v1 submitted 14 September, 2017;
originally announced September 2017.
-
A portable magnetic field of > 3 T generated by the flux jump assisted, pulsed field magnetisation of bulk superconductors
Authors:
Difan Zhou,
Mark D. Ainslie,
Yunhua Shi,
Anthony R. Dennis,
Kaiyuan Huang,
John R. Hull,
David A. Cardwell,
John H. Durrell
Abstract:
A trapped magnetic field of greater than 3 T has been achieved in a single grain GdBa2Cu3O7-δ (GdBaCuO) bulk superconductor of diameter 30 mm by employing pulsed field magnetisation (PFM). The magnet system is portable and operates at temperatures between 50 K and 60 K. Flux jump behaviour was observed consistently during magnetisation when the applied pulsed field, Ba, exceeded a critical value (…
▽ More
A trapped magnetic field of greater than 3 T has been achieved in a single grain GdBa2Cu3O7-δ (GdBaCuO) bulk superconductor of diameter 30 mm by employing pulsed field magnetisation (PFM). The magnet system is portable and operates at temperatures between 50 K and 60 K. Flux jump behaviour was observed consistently during magnetisation when the applied pulsed field, Ba, exceeded a critical value (e.g. 3.78 T at 60 K). A sharp dBa/dt is essential to this phenomenon. This flux jump behaviour enables the magnetic flux to penetrate fully to the centre of the bulk superconductor, resulting in full magnetization of the sample without requiring an applied field as large as that predicted by the Bean model. We show that this flux jump behaviour can occur over a wide range of fields and temperatures, and that it can be exploited in a practical quasi-permanent magnet system.
△ Less
Submitted 1 January, 2017;
originally announced January 2017.
-
Formal Verification of Autonomous Vehicle Platooning
Authors:
Maryam Kamali,
Louise A. Dennis,
Owen McAree,
Michael Fisher,
Sandor M. Veres
Abstract:
The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out b…
▽ More
The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the agent code does not scale to the full system and as the global verification technique does not capture the essential verification of autonomous behavior, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles.
△ Less
Submitted 4 February, 2016;
originally announced February 2016.
-
Towards Verifiably Ethical Robot Behaviour
Authors:
Louise A. Dennis,
Michael Fisher,
Alan F. T. Winfield
Abstract:
Ensuring that autonomous systems work ethically is both complex and difficult. However, the idea of having an additional `governor' that assesses options the system has, and prunes them to select the most ethical choices is well understood. Recent work has produced such a governor consisting of a `consequence engine' that assesses the likely future outcomes of actions then applies a Safety/Ethical…
▽ More
Ensuring that autonomous systems work ethically is both complex and difficult. However, the idea of having an additional `governor' that assesses options the system has, and prunes them to select the most ethical choices is well understood. Recent work has produced such a governor consisting of a `consequence engine' that assesses the likely future outcomes of actions then applies a Safety/Ethical logic to select actions. Although this is appealing, it is impossible to be certain that the most ethical options are actually taken. In this paper we extend and apply a well-known agent verification approach to our consequence engine, allowing us to verify the correctness of its ethical decision-making.
△ Less
Submitted 14 April, 2015;
originally announced April 2015.
-
A new seeding technique for the reliable fabrication of large, SmBCO single grains containing silver using top seeded melt growth
Authors:
Y-H Shi,
A R Dennis,
D A Cardwell
Abstract:
Silver (Ag) is an established additive for improving the mechanical properties of single grain, (RE)BCO bulk superconductors (where RE = Sm, Gd and Y). The presence of Ag in the (RE)BCO bulk composition, however, typically reduces the melting temperature of the single crystal seed in the top seeded melt growth (TSMG) process, which complicates significantly the controlled nucleation and subsequent…
▽ More
Silver (Ag) is an established additive for improving the mechanical properties of single grain, (RE)BCO bulk superconductors (where RE = Sm, Gd and Y). The presence of Ag in the (RE)BCO bulk composition, however, typically reduces the melting temperature of the single crystal seed in the top seeded melt growth (TSMG) process, which complicates significantly the controlled nucleation and subsequent epitaxial growth of a single grain, which is essential for high field engineering applications. The reduced reliability of the seeding process in the presence of Ag is particularly acute for the SmBCO system, since the melting temperature of SmBCO is very close to that of the generic NdBCO(MgO) seed. SmBCO has the highest superconducting transition temperature, Tc, and exhibits the most pronounced "peak" effect at higher magnetic field of all materials in the family of (RE)BCO bulk superconductors and, therefore, has the greatest potential for use in practical applications (compared to GdBCO and YBCO, in particular). Development of an effective seeding process, therefore, is one of the major challenges of the TSMG process for the growth of large, high quantity single grain superconductors. In this paper, we report a novel technique that involves introducing a buffer layer between the seed crystal and the precursor pellet, primarily to inhibit the diffusion of Ag from the green body to the seed during melt processing in order to prevent the melting of the seed. The success rate of the seeding process using this technique is 100% for relatively small batch samples. The superconducting properties, Tc, Jc and trapped fields, of the single grains fabricated using the buffers are reported and the micro-structures in the vicinity of the buffer of single grains fabricated by the modified technique are analysed.
△ Less
Submitted 29 October, 2014;
originally announced October 2014.
-
An Abstract Formal Basis for Digital Crowds
Authors:
Marija Slavkovik,
Louise A. Dennis,
Michael Fisher
Abstract:
Crowdsourcing, together with its related approaches, has become very popular in recent years. All crowdsourcing processes involve the participation of a digital crowd, a large number of people that access a single Internet platform or shared service. In this paper we explore the possibility of applying formal methods, typically used for the verification of software and hardware systems, in analysi…
▽ More
Crowdsourcing, together with its related approaches, has become very popular in recent years. All crowdsourcing processes involve the participation of a digital crowd, a large number of people that access a single Internet platform or shared service. In this paper we explore the possibility of applying formal methods, typically used for the verification of software and hardware systems, in analysing the behaviour of a digital crowd. More precisely, we provide a formal description language for specifying digital crowds. We represent digital crowds in which the agents do not directly communicate with each other. We further show how this specification can provide the basis for sophisticated formal methods, in particular formal verification.
△ Less
Submitted 7 August, 2014;
originally announced August 2014.
-
A Trapped Field of 17.6 T in Melt-Processed, Bulk Gd-Ba-Cu-O Reinforced with Shrink-Fit Steel
Authors:
John H. Durrell,
Anthony R. Dennis,
Jan Jaroszynski,
Mark D. Ainslie,
Kysen G. B. Palmer,
Yunhua Shi,
Archie M. Campbell,
John Hull,
Mike Strasik,
Eric Hellstrom,
David A. Cardwell
Abstract:
The ability of large grain, REBa$_{2}$Cu$_{3}$O$_{7-δ}$ [(RE)BCO; RE = rare earth] bulk superconductors to trap magnetic field is determined by their critical current. With high trapped fields, however, bulk samples are subject to a relatively large Lorentz force, and their performance is limited primarily by their tensile strength. Consequently, sample reinforcement is the key to performance impr…
▽ More
The ability of large grain, REBa$_{2}$Cu$_{3}$O$_{7-δ}$ [(RE)BCO; RE = rare earth] bulk superconductors to trap magnetic field is determined by their critical current. With high trapped fields, however, bulk samples are subject to a relatively large Lorentz force, and their performance is limited primarily by their tensile strength. Consequently, sample reinforcement is the key to performance improvement in these technologically important materials. In this work, we report a trapped field of 17.6 T, the largest reported to date, in a stack of two, silver-doped GdBCO superconducting bulk samples, each of diameter 25 mm, fabricated by top-seeded melt growth (TSMG) and reinforced with shrink-fit stainless steel. This sample preparation technique has the advantage of being relatively straightforward and inexpensive to implement and offers the prospect of easy access to portable, high magnetic fields without any requirement for a sustaining current source.
△ Less
Submitted 7 July, 2014; v1 submitted 3 June, 2014;
originally announced June 2014.
-
Practical Verification of Decision-Making in Agent-Based Autonomous Systems
Authors:
Louise A. Dennis,
Michael Fisher,
Nicholas K. Lincoln,
Alexei Lisitsa,
Sandor M. Veres
Abstract:
We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex…
▽ More
We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.
△ Less
Submitted 9 October, 2013;
originally announced October 2013.
-
Laboratory Search for Spin-dependent Short-range Force from Axion-Like-Particles using Optically Polarized 3He gas
Authors:
**-Han Chu,
Alec Dennis,
ChangBo Fu,
Haiyan Gao,
Rakshya Khatiwada,
Georgios Laskaris,
Ke Li,
Erick Smith,
William Michael Snow,
Haiyang Yan,
Wangzhi Zheng
Abstract:
The possible existence of short-range forces between unpolarized and polarized spin-1/2 particles has attracted the attention of physicists for decades. These forces are predicted in various theories and provide a possible new source for parity (P) and time reversal (T) symmetry violation. We use an ensemble of polarized 3He gas in a cell with a 250 um thickness glass window to search for a force…
▽ More
The possible existence of short-range forces between unpolarized and polarized spin-1/2 particles has attracted the attention of physicists for decades. These forces are predicted in various theories and provide a possible new source for parity (P) and time reversal (T) symmetry violation. We use an ensemble of polarized 3He gas in a cell with a 250 um thickness glass window to search for a force from scalar boson exchange over a sub-millimeter ranges. This interaction would produce a NMR frequency shift as an unpolarized mass is moved near and far from the polarized ensemble. We report a new upper bound on the product g_{s}g_{p}^{n} of the scalar couplings to the fermions in the unpolarized mass, and the pseudoscalar coupling of the polarized neutron in the 3He nucleus for force ranges from 1e-4 to 1e-2 m, which corresponds to a mass range of 2e-3 to 2e-5 eV for the scalar boson.
△ Less
Submitted 4 December, 2012; v1 submitted 12 November, 2012;
originally announced November 2012.
-
YBCO single grains seeded by 45° - 45° bridge-seeds of different lengths
Authors:
Yunhua Shi,
John H. Durrell,
Anthony R. Dennis,
David A. Cardwell
Abstract:
Single grain, (RE)BCO bulk superconductors in large or complicated geometries are required for a variety of potential applications, such as motors and generators and magnetic shielding devices. As a result, top, multi-seeded, melt growth (TMSMG) has been investigated over the past two years in an attempt to enlarge the size of (RE)BCO single grains specifically for such applications. Of these mult…
▽ More
Single grain, (RE)BCO bulk superconductors in large or complicated geometries are required for a variety of potential applications, such as motors and generators and magnetic shielding devices. As a result, top, multi-seeded, melt growth (TMSMG) has been investigated over the past two years in an attempt to enlarge the size of (RE)BCO single grains specifically for such applications. Of these multi-seeding techniques, so-called bridge seeding provides the best alignment of two seeds in a single grain growth process. Here we report, for the first time, the successful growth of YBCO using a special, 45° - 45°, arrangement of bridge-seeds. The superconducting properties, including trapped field, of the multi-seeded YBCO grains have been measured for different bridge lengths of the 45°- 45° bridge-seeds. The boundaries at the im**ing growth front and the growth features of the top, multi-seeded surface and cross-section of the multi-seeded, samples have been analysed using optical microscopy. The results suggest that an impurity-free boundary between the two seeds of each leg of the bridge-seed can form when 45°- 45° bridge-seeds are used to enlarge the size of YBCO grains.
△ Less
Submitted 19 October, 2012;
originally announced October 2012.
-
A Trapped Field of >3T in Bulk MgB2 Fabricated by Uniaxial Hot Pressing
Authors:
J. H. Durrell,
C. E. J. Dancer,
A. Dennis,
Y. Shi,
Z. Xu,
A. M. Campbell,
N. H. Babu,
R. I. Todd,
C. R. M. Grovenor,
D. A. Cardwell
Abstract:
A trapped field of over 3 T has been measured at 17.5 K in a magnetised stack of two disc-shaped bulk MgB2 superconductors of diameter 25 mm and thickness 5.4 mm. The bulk MgB2 samples were fabricated by uniaxial hot pressing, which is a readily scalable, industrial technique, to 91% of their maximum theoretical density. The macroscopic critical current density derived from the trapped field data…
▽ More
A trapped field of over 3 T has been measured at 17.5 K in a magnetised stack of two disc-shaped bulk MgB2 superconductors of diameter 25 mm and thickness 5.4 mm. The bulk MgB2 samples were fabricated by uniaxial hot pressing, which is a readily scalable, industrial technique, to 91% of their maximum theoretical density. The macroscopic critical current density derived from the trapped field data using the Biot-Savart law is consistent with the measured local critical current density. From this we conclude that critical current density, and therefore trapped field performance, is limited by the flux pinning available in MgB2, rather than by lack of connectivity. This suggests strongly that both increasing sample size and enhancing pinning through do** will allow further increases in trapped field performance of bulk MgB2.
△ Less
Submitted 28 September, 2012; v1 submitted 30 July, 2012;
originally announced July 2012.
-
Agent Based Approaches to Engineering Autonomous Space Software
Authors:
Louise A. Dennis,
Michael Fisher,
Nicholas Lincoln,
Alexei Lisitsa,
Sandor M. Veres
Abstract:
Current approaches to the engineering of space software such as satellite control systems are based around the development of feedback controllers using packages such as MatLab's Simulink toolbox. These provide powerful tools for engineering real time systems that adapt to changes in the environment but are limited when the controller itself needs to be adapted.
We are investigating ways in wh…
▽ More
Current approaches to the engineering of space software such as satellite control systems are based around the development of feedback controllers using packages such as MatLab's Simulink toolbox. These provide powerful tools for engineering real time systems that adapt to changes in the environment but are limited when the controller itself needs to be adapted.
We are investigating ways in which ideas from temporal logics and agent programming can be integrated with the use of such control systems to provide a more powerful layer of autonomous decision making. This paper will discuss our initial approaches to the engineering of such systems.
△ Less
Submitted 2 March, 2010;
originally announced March 2010.
