Showing 1–15 of 15 results for author: Dixon, C

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.

Multi-Scale Verification of Distributed Synchronisation

Authors: Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher

Abstract: Algorithms for the synchronisation of clocks across networks are both common and important within distributed systems. We here address not only the formal modelling of these algorithms, but also the formal verification of their behaviour. Of particular importance is the strong link between the very different levels of abstraction at which the algorithms may be verified. Our contribution is primari… ▽ More Algorithms for the synchronisation of clocks across networks are both common and important within distributed systems. We here address not only the formal modelling of these algorithms, but also the formal verification of their behaviour. Of particular importance is the strong link between the very different levels of abstraction at which the algorithms may be verified. Our contribution is primarily the formalisation of this connection between individual models and population-based models, and the subsequent verification that is then possible. While the technique is applicable across a range of synchronisation algorithms, we particularly focus on the synchronisation of (biologically-inspired) pulse-coupled oscillators, a widely used approach in practical distributed systems. For this application domain, different levels of abstraction are crucial: models based on the behaviour of an individual process are able to capture the details of distinguished nodes in possibly heterogenous networks, where each node may exhibit different behaviour. On the other hand, collective models assume homogeneous sets of processes, and allow the behaviour of the network to be analysed at the global level. System-wide parameters may be easily adjusted, for example environmental factors inhibiting the reliability of the shared communication medium. This work provides a formal bridge across the abstraction gap separating the individual models and the population-based models for this important class of synchronisation algorithms. △ Less

Submitted 27 September, 2018; originally announced September 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

Complex Octahedral Tilt Phases in the Ferroelectric Perovskite System Li$_x$Na$_{1-x}$NbO$_3$

Authors: Charlotte Dixon, Philip Lightfoot

Abstract: High-temperature phase behavior in the system LixNa1-xNbO3 has been studied by using high-resolution powder neutron diffraction. Each of the three compositions studied in the Na-rich part of the phase diagram (x = 0.03, 0.08 and 0.12) shows evidence for distinct and complex structural modulations based on different tilting schemes of NbO6 octahedral units. Whilst octahedral tilting is prevalent in… ▽ More High-temperature phase behavior in the system LixNa1-xNbO3 has been studied by using high-resolution powder neutron diffraction. Each of the three compositions studied in the Na-rich part of the phase diagram (x = 0.03, 0.08 and 0.12) shows evidence for distinct and complex structural modulations based on different tilting schemes of NbO6 octahedral units. Whilst octahedral tilting is prevalent in the structural chemistry of perovskites the nature of complexity of the phases observed here is unprecedented. Neither of the long-range tilt phases observed in NaNbO3 itself occurs here; instead a novel phase with a well-defined 4-fold superlattice is observed for the composition Li0.12Na0.88NbO3, and yet more complex phases with modulations based on 20-fold and 30-fold repeats are observed for Li0.03Na0.97NbO3 and Li0.08Na0.92NbO3, respectively. This peculiar structural behavior makes the system LixNa1-xNbO3 the most structurally complex 'simple' perovskite known. △ Less

Submitted 23 February, 2018; originally announced February 2018.

Journal ref: Phys. Rev. B 97, 224105 (2018)

On the formation mechanisms of compact elliptical galaxies

Authors: Anna Ferre-Mateu, Duncan A. Forbes, Aaron J. Romanowsky, Joachim Janz, Christoper Dixon

Abstract: In order to investigate the formation mechanisms of the rare compact elliptical galaxies (cE) we have compiled a sample of 25 cEs with good SDSS spectra, covering a range of stellar masses, sizes and environments. They have been visually classified according to the interaction with their host, representing different evolutionary stages. We have included clearly disrupted galaxies, galaxies that de… ▽ More In order to investigate the formation mechanisms of the rare compact elliptical galaxies (cE) we have compiled a sample of 25 cEs with good SDSS spectra, covering a range of stellar masses, sizes and environments. They have been visually classified according to the interaction with their host, representing different evolutionary stages. We have included clearly disrupted galaxies, galaxies that despite not showing signs of interaction are located close to a massive neighbor (thus are good candidates for a strip** process), and cEs with no host nearby. For the latter, tidal strip** is less likely to have happened and instead they could simply represent the very low-mass, faint end of the ellipticals. We study a set of properties (structural parameters, stellar populations, star formation histories and mass ratios) that can be used to discriminate between an intrinsic or stripped origin. We find that one diagnostic tool alone is inconclusive for the majority of objects. However, if we combine all the tools a clear picture emerges. The most plausible origin, as well as the evolutionary stage and progenitor type, can be then determined. Our results favor the strip** mechanism for those galaxies in groups and clusters that have a plausible host nearby, but favors an intrinsic origin for those rare cEs without a plausible host and that are located in looser environments. △ Less

Submitted 20 September, 2017; originally announced September 2017.

Comments: Accepeted for publication in MNRAS. 24 pages, 21 figures, 5 tables

The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators

Authors: Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher

Abstract: We assess the power consumption of network synchronisation protocols, particularly the energy required to synchronise all nodes across a network. We use the widely adopted approach of bio-inspired, pulse-coupled oscillators to achieve network-wide synchronisation and provide an extended formal model of just such a protocol, enhanced with structures for recording energy usage. Exhaustive analysis i… ▽ More We assess the power consumption of network synchronisation protocols, particularly the energy required to synchronise all nodes across a network. We use the widely adopted approach of bio-inspired, pulse-coupled oscillators to achieve network-wide synchronisation and provide an extended formal model of just such a protocol, enhanced with structures for recording energy usage. Exhaustive analysis is then carried out through formal verification, utilising the PRISM model checker to calculate the resources consumed on each possible system execution. This allows us to assess a range of parameter instantiations and to explore trade-offs between power consumption and time to synchronise. This provides a principled basis for the formal analysis of a much broader range of large-scale network protocols. △ Less

Submitted 24 October, 2017; v1 submitted 13 September, 2017; originally announced September 2017.

A Corroborative Approach to Verification and Validation of Human--Robot Teams

Authors: Matt Webster, David Western, Dejanira Araiza-Illan, Clare Dixon, Kerstin Eder, Michael Fisher, Anthony G. Pipe

Abstract: We present an approach for the verification and validation (V&V) of robot assistants in the context of human-robot interactions (HRI), to demonstrate their trustworthiness through corroborative evidence of their safety and functional correctness. Key challenges include the complex and unpredictable nature of the real world in which assistant and service robots operate, the limitations on available… ▽ More We present an approach for the verification and validation (V&V) of robot assistants in the context of human-robot interactions (HRI), to demonstrate their trustworthiness through corroborative evidence of their safety and functional correctness. Key challenges include the complex and unpredictable nature of the real world in which assistant and service robots operate, the limitations on available V&V techniques when used individually, and the consequent lack of confidence in the V&V results. Our approach, called corroborative V&V, addresses these challenges by combining several different V&V techniques; in this paper we use formal verification (model checking), simulation-based testing, and user validation in experiments with a real robot. We demonstrate our corroborative V&V approach through a handover task, the most critical part of a complex cooperative manufacturing scenario, for which we propose some safety and liveness requirements to verify and validate. We construct formal models, simulations and an experimental test rig for the HRI. To capture requirements we use temporal logic properties, assertion checkers and textual descriptions. This combination of approaches allows V&V of the HRI task at different levels of modelling detail and thoroughness of exploration, thus overcoming the individual limitations of each technique. Should the resulting V&V evidence present discrepancies, an iterative process between the different V&V techniques takes place until corroboration between the V&V techniques is gained from refining and improving the assets (i.e., system and requirement models) to represent the HRI task in a more truthful manner. Therefore, corroborative V&V affords a systematic approach to 'meta-V&V,' in which different V&V techniques can be used to corroborate and check one another, increasing the level of certainty in the results of V&V. △ Less

Submitted 5 September, 2019; v1 submitted 26 August, 2016; originally announced August 2016.

Comments: 49 pages

Clausal Resolution for Modal Logics of Confluence

Authors: Cláudia Nalon, João Marcos, Clare Dixon

Abstract: We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms th… ▽ More We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms that characterise such systems. We discuss soundness, completeness, and termination of the method. In particular, completeness can be modularly proved by showing that the conclusions of each newly added inference rule ensures that the corresponding conditions on frames hold. Some examples are given in order to illustrate the use of the method. △ Less

Submitted 1 May, 2014; originally announced May 2014.

Comments: 15 pages, 1 figure. Preprint of the paper accepted to IJCAR 2014

A Resolution Prover for Coalition Logic

Authors: Cláudia Nalon, Lan Zhang, Clare Dixon, Ullrich Hustadt

Abstract: We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolution-bas… ▽ More We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolution-based calculus for Coalition Logic. We then give details of the implementation of CLProver and present the results for a comparison with an existing tableau-based solver. △ Less

Submitted 3 April, 2014; originally announced April 2014.

Comments: In Proceedings SR 2014, arXiv:1404.0414

ACM Class: I.2.3; F.4.1

Journal ref: EPTCS 146, 2014, pp. 65-73

Discovery and Early Multi-Wavelength Measurements of the Energetic Type Ic Supernova PTF12gzk: A Massive-Star Explosion in a Dwarf Host Galaxy

Authors: Sagi Ben-Ami, Avishay Gal-Yam, Alexei V. Filippenko, Paolo A. Mazzali, Maryam Modjaz, Ofer Yaron, Iair Arcavi, S. Bradley Cenko, Assaf Horesh, D. Andrew Howell, Melissa L. Graham, J. Chuck Horst, Myunshin Im, Yiseul Jeon, Shrinivas R. Kulkarni, Douglas C. Leonard, Elena Pian, David J. Sand, Mark Sullivan, Juliette C. Becker, David Bersier, Joshua S. Bloom, Michael Bottom, Peter J. Brown, Kelsey I. Clubb , et al. (23 additional authors not shown)

Abstract: We present the discovery and extensive early-time observations of the Type Ic supernova (SN) PTF12gzk. Our finely sampled light curves show a rise of 0.8mag within 2.5hr. Power-law fits [f(t)\sim(t-t_0)^n] to these data constrain the explosion date to within one day. We cannot rule out the expected quadratic fireball model, but higher values of n are possible as well for larger areas in the fit pa… ▽ More We present the discovery and extensive early-time observations of the Type Ic supernova (SN) PTF12gzk. Our finely sampled light curves show a rise of 0.8mag within 2.5hr. Power-law fits [f(t)\sim(t-t_0)^n] to these data constrain the explosion date to within one day. We cannot rule out the expected quadratic fireball model, but higher values of n are possible as well for larger areas in the fit parameter space. Our bolometric light curve and a dense spectral sequence are used to estimate the physical parameters of the exploding star and of the explosion. We show that the photometric evolution of PTF12gzk is slower than that of most SNe Ic, and its high ejecta velocities (~30,000km/s four days after explosion) are closer to the observed velocities of broad-lined SNe Ic associated with gamma-ray bursts (GRBs) than to the observed velocities in normal Type Ic SNe. The high velocities are sustained through the SN early evolution, and are similar to those of GRB-SNe when the SN reach peak magnitude. By comparison with the spectroscopically similar SN 2004aw, we suggest that the observed properties of PTF12gzk indicate an initial progenitor mass of 25-35 solar mass and a large (5-10E51 erg) kinetic energy, close to the regime of GRB-SN properties. The host-galaxy characteristics are consistent with GRB-SN hosts, and not with normal SN Ic hosts as well, yet this SN does not show the broad lines over extended periods of time that are typical of broad-line Type Ic SNe. △ Less

Submitted 23 September, 2013; v1 submitted 29 August, 2012; originally announced August 2012.

Efficient First-Order Temporal Logic for Infinite-State Systems

Authors: Clare Dixon, Michael Fisher, Boris Konev, Alexei Lisitsa

Abstract: In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for this form of specification and tractable enough for practical deductive verification. Importantly, the power of the temporal language allows us to describe (… ▽ More In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for this form of specification and tractable enough for practical deductive verification. Importantly, the power of the temporal language allows us to describe (and verify) asynchronous systems, communication delays and more complex properties such as liveness and fairness properties. These aspects appear difficult for many other approaches to infinite-state verification. △ Less

Submitted 6 February, 2007; originally announced February 2007.

Comments: 16 pages, 2 figures

ACM Class: F.4.1; F.3.1; D.2.2; D.2.4

Enhancement of Josephson quasiparticle current in coupled superconducting single-electron transistors

Authors: D. C. Dixon, C. P. Heij, P. Hadley, J. E. Mooij

Abstract: The Josephson quasiparticle (JQP) cycle in a voltage-biased superconducting single-electron transistor (SSET) combines coherent Cooper pair tunneling with incoherent quasiparticle decay. We have measured the influence of current flow through an independently-biased SSET on the JQP cycle when the two SSET's have a strong mutual capacitive coupling. We find, among other effects, that the JQP curre… ▽ More The Josephson quasiparticle (JQP) cycle in a voltage-biased superconducting single-electron transistor (SSET) combines coherent Cooper pair tunneling with incoherent quasiparticle decay. We have measured the influence of current flow through an independently-biased SSET on the JQP cycle when the two SSET's have a strong mutual capacitive coupling. We find, among other effects, that the JQP current in one SSET is enhanced by the presence of a quasiparticle current in the other SSET. A simplified model of the coupled-SSET system is presented which reproduces the enhancement effect. △ Less

Submitted 30 September, 1999; originally announced September 1999.

Clausal Temporal Resolution

Authors: Michael Fisher, Clare Dixon, Martin Peim

Abstract: In this article, we examine how clausal resolution can be applied to a specific, but widely used, non-classical logic, namely discrete linear temporal logic. Thus, we first define a normal form for temporal formulae and show how arbitrary temporal formulae can be translated into the normal form, while preserving satisfiability. We then introduce novel resolution rules that can be applied to form… ▽ More In this article, we examine how clausal resolution can be applied to a specific, but widely used, non-classical logic, namely discrete linear temporal logic. Thus, we first define a normal form for temporal formulae and show how arbitrary temporal formulae can be translated into the normal form, while preserving satisfiability. We then introduce novel resolution rules that can be applied to formulae in this normal form, provide a range of examples and examine the correctness and complexity of this approach is examined and. This clausal resolution approach. Finally, we describe related work and future developments concerning this work. △ Less

Submitted 14 April, 2000; v1 submitted 21 July, 1999; originally announced July 1999.

Comments: 35 pages, 0 figures Expanded related work, corrected typos, expanded proofs

ACM Class: I.2.3; F.4.1

Negative differential resistance due to single-electron switching

Authors: C. P. Heij, D. C. Dixon, P. Hadley, J. E. Mooij

Abstract: We present the multilevel fabrication and measurement of a Coulomb-blockade device displaying tunable negative differential resistance (NDR). Applications for devices displaying NDR include amplification, logic, and memory circuits. Our device consists of two Al/Al$_{x}$O$_{y}$ islands that are strongly coupled by an overlap capacitor. Our measurements agree excellently with a model based on the… ▽ More We present the multilevel fabrication and measurement of a Coulomb-blockade device displaying tunable negative differential resistance (NDR). Applications for devices displaying NDR include amplification, logic, and memory circuits. Our device consists of two Al/Al$_{x}$O$_{y}$ islands that are strongly coupled by an overlap capacitor. Our measurements agree excellently with a model based on the orthodox theory of single-electron transport. △ Less

Submitted 21 September, 1998; originally announced September 1998.

Comments: 3 pages, 3 figures; submitted to APL

Dynamic nuclear polarization at the edge of a two-dimensional electron gas

Authors: David C. Dixon, Keith R. Wald, Paul L. McEuen, M. R. Melloch

Abstract: We have used gated GaAs/AlGaAs heterostructures to explore nonlinear transport between spin-resolved Landau level (LL) edge states over a submicron region of two-dimensional electron gas (2DEG). The current I flowing from one edge state to the other as a function of the voltage V between them shows diode-like behavior---a rapid increase in I above a well-defined threshold V_t under forward bias,… ▽ More We have used gated GaAs/AlGaAs heterostructures to explore nonlinear transport between spin-resolved Landau level (LL) edge states over a submicron region of two-dimensional electron gas (2DEG). The current I flowing from one edge state to the other as a function of the voltage V between them shows diode-like behavior---a rapid increase in I above a well-defined threshold V_t under forward bias, and a slower increase in I under reverse bias. In these measurements, a pronounced influence of a current-induced nuclear spin polarization on the spin splitting is observed, and supported by a series of NMR experiments. We conclude that the hyperfine interaction plays an important role in determining the electronic properties at the edge of a 2DEG. △ Less

Submitted 7 January, 1997; originally announced January 1997.

Comments: 8 pages RevTeX, 7 figures (GIF); submitted to Phys. Rev. B

Report number: LBNL-39807