-
Monitoring ROS2: from Requirements to Autonomous Robots
Authors:
Ivan Perez,
Anastasia Mavridou,
Tom Pressburger,
Alexander Will,
Patrick J. Martin
Abstract:
Runtime verification (RV) has the potential to enable the safe operation of safety-critical systems that are too complex to formally verify, such as Robot Operating System 2 (ROS2) applications. Writing correct monitors can itself be complex, and errors in the monitoring subsystem threaten the mission as a whole. This paper provides an overview of a formal approach to generating runtime monitors f…
▽ More
Runtime verification (RV) has the potential to enable the safe operation of safety-critical systems that are too complex to formally verify, such as Robot Operating System 2 (ROS2) applications. Writing correct monitors can itself be complex, and errors in the monitoring subsystem threaten the mission as a whole. This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool. FRET is used to specify requirements with unambiguous semantics, which are then automatically translated into temporal logic formulae. Ogma generates monitor specifications from the FRET output, which are compiled into hard-real time C99. To facilitate integration of the monitors in ROS2, we have extended Ogma to generate ROS2 packages defining monitoring nodes, which run the monitors when new data becomes available, and publish the results of any violations. The goal of our approach is to treat the generated ROS2 packages as black boxes and integrate them into larger ROS2 systems with minimal effort.
△ Less
Submitted 28 September, 2022;
originally announced September 2022.
-
STPA-driven Multilevel Runtime Monitoring for In-time Hazard Detection
Authors:
Smitha Gautham,
Georgios Bakirtzis,
Alexander Will,
Athira V. Jayakumar,
Carl R. Elks
Abstract:
Runtime verification or runtime monitoring equips safety-critical cyber-physical systems to augment design assurance measures and ensure operational safety and security. Cyber-physical systems have interaction failures, attack surfaces, and attack vectors resulting in unanticipated hazards and loss scenarios. These interaction failures pose challenges to runtime verification regarding monitoring s…
▽ More
Runtime verification or runtime monitoring equips safety-critical cyber-physical systems to augment design assurance measures and ensure operational safety and security. Cyber-physical systems have interaction failures, attack surfaces, and attack vectors resulting in unanticipated hazards and loss scenarios. These interaction failures pose challenges to runtime verification regarding monitoring specifications and monitoring placements for in-time detection of hazards. We develop a well-formed workflow model that connects system theoretic process analysis, commonly referred to as STPA, hazard causation information to lower-level runtime monitoring to detect hazards at the operational phase. Specifically, our model follows the DepDevOps paradigm to provide evidence and insights to runtime monitoring on what to monitor, where to monitor, and the monitoring context. We demonstrate and evaluate the value of multilevel monitors by injecting hazards on an autonomous emergency braking system model.
△ Less
Submitted 22 June, 2022; v1 submitted 19 April, 2022;
originally announced April 2022.
-
Homological Polynomial Coefficients and the Twist Number of Alternating Surface Links
Authors:
David A. Will
Abstract:
For $D$ a reduced alternating surface link diagram, we bound the twist number of $D$ in terms of the coefficients of a polynomial invariant. To this end, we introduce a generalization of the homological Kauffman bracket defined by Krushkal. Combined with work of Futer, Kalfagianni, and Purcell, this yields a bound for the hyperbolic volume of a class of alternating surface links in terms of these…
▽ More
For $D$ a reduced alternating surface link diagram, we bound the twist number of $D$ in terms of the coefficients of a polynomial invariant. To this end, we introduce a generalization of the homological Kauffman bracket defined by Krushkal. Combined with work of Futer, Kalfagianni, and Purcell, this yields a bound for the hyperbolic volume of a class of alternating surface links in terms of these coefficients.
△ Less
Submitted 24 November, 2020;
originally announced November 2020.
-
A comparison of different types of Niching Genetic Algorithms for variable selection in solar radiation estimation
Authors:
Jorge Bustos,
Victor A. Jimenez,
Adrian Will
Abstract:
Variable selection problems generally present more than a single solution and, sometimes, it is worth to find as many solutions as possible. The use of Evolutionary Algorithms applied to this kind of problem proves to be one of the best methods to find optimal solutions. Moreover, there are variants designed to find all or almost all local optima, known as Niching Genetic Algorithms (NGA). There a…
▽ More
Variable selection problems generally present more than a single solution and, sometimes, it is worth to find as many solutions as possible. The use of Evolutionary Algorithms applied to this kind of problem proves to be one of the best methods to find optimal solutions. Moreover, there are variants designed to find all or almost all local optima, known as Niching Genetic Algorithms (NGA). There are several different NGA methods developed in order to achieve this task. The present work compares the behavior of eight different niching techniques, applied to a climatic database of four weather stations distributed in Tucuman, Argentina. The goal is to find different sets of input variables that have been used as the input variable by the estimation method. Final results were evaluated based on low estimation error and low dispersion error, as well as a high number of different results and low computational time. A second experiment was carried out to study the capability of the method to identify critical variables. The best results were obtained with Deterministic Crowding. In contrast, Steady State Worst Among Most Similar and Probabilistic Crowding showed good results but longer processing times and less ability to determine the critical factors.
△ Less
Submitted 14 February, 2020;
originally announced February 2020.
-
Progress on Experiments towards LWFA-driven Transverse Gradient Undulator-Based FELs
Authors:
Axel Bernhard,
Veronica Afonso Rodriguez,
Stephan Kuschel,
Maria Leier,
Peter Peiffer,
Alexander Saevert,
Matthew Schwab,
Walter Werner,
Christina Widmann,
Andreas Will,
Anke-Susanne Mueller,
Malte Kaluza
Abstract:
Free Electron Lasers (FEL) are commonly regarded as the potential key application of laser wakefield accelerators (LWFA). It has been found that electron bunches exiting from state-of-the-art LWFAs exhibit a normalized 6-dimensional beam brightness comparable to those in conventional linear accelerators. Effectively exploiting this beneficial beam property for LWFA-based FELs is challenging due to…
▽ More
Free Electron Lasers (FEL) are commonly regarded as the potential key application of laser wakefield accelerators (LWFA). It has been found that electron bunches exiting from state-of-the-art LWFAs exhibit a normalized 6-dimensional beam brightness comparable to those in conventional linear accelerators. Effectively exploiting this beneficial beam property for LWFA-based FELs is challenging due to the extreme initial conditions particularly in terms of beam divergence and energy spread. Several different approaches for capturing, resha** and matching LWFA beams to suited undulators, such as bunch decompression or transverse-gradient undulator schemes, are currently being explored. In this article the transverse gradient undulator concept will be discussed with a focus on recent experimental achievements.
△ Less
Submitted 13 December, 2017;
originally announced December 2017.
-
Second-Scale Nuclear Spin Coherence Time of Trapped Ultracold $^{23}$Na$^{40}$K Molecules
Authors:
Jee Woo Park,
Zoe Z. Yan,
Huanqian Loh,
Sebastian A. Will,
Martin W. Zwierlein
Abstract:
Coherence, the stability of the relative phase between quantum states, lies at the heart of quantum mechanics. Applications such as precision measurement, interferometry, and quantum computation are enabled by physical systems that have quantum states with robust coherence. With the creation of molecular ensembles at sub-$μ$K temperatures, diatomic molecules have become a novel system under full q…
▽ More
Coherence, the stability of the relative phase between quantum states, lies at the heart of quantum mechanics. Applications such as precision measurement, interferometry, and quantum computation are enabled by physical systems that have quantum states with robust coherence. With the creation of molecular ensembles at sub-$μ$K temperatures, diatomic molecules have become a novel system under full quantum control. Here, we report on the observation of stable coherence between a pair of nuclear spin states of ultracold fermionic NaK molecules in the singlet rovibrational ground state. Employing microwave fields, we perform Ramsey spectroscopy and observe coherence times on the scale of one second. This work opens the door for the exploration of single molecules as a versatile quantum memory. Switchable long-range interactions between dipolar molecules can further enable two-qubit gates, allowing quantum storage and processing in the same physical system. Within the observed coherence time, $10^4$ one- and two-qubit gate operations will be feasible.
△ Less
Submitted 13 June, 2016;
originally announced June 2016.
-
Coherent Microwave Control of Ultracold $^{23}$Na$^{40}$K Molecules
Authors:
Sebastian A. Will,
Jee Woo Park,
Zoe Z. Yan,
Huanqian Loh,
Martin W. Zwierlein
Abstract:
We demonstrate coherent microwave control of rotational and hyperfine states of trapped, ultracold, and chemically stable $^{23}$Na$^{40}$K molecules. Starting with all molecules in the absolute rovibrational and hyperfine ground state, we study rotational transitions in combined magnetic and electric fields and explain the rich hyperfine structure. Following the transfer of the entire molecular e…
▽ More
We demonstrate coherent microwave control of rotational and hyperfine states of trapped, ultracold, and chemically stable $^{23}$Na$^{40}$K molecules. Starting with all molecules in the absolute rovibrational and hyperfine ground state, we study rotational transitions in combined magnetic and electric fields and explain the rich hyperfine structure. Following the transfer of the entire molecular ensemble into a single hyperfine level of the first rotationally excited state, $J{=}1$, we observe collisional lifetimes of more than $3\, \rm s$, comparable to those in the rovibrational ground state, $J{=}0$. Long-lived ensembles and full quantum state control are prerequisites for the use of ultracold molecules in quantum simulation, precision measurements and quantum information processing.
△ Less
Submitted 31 March, 2016;
originally announced April 2016.
-
Two-Photon Pathway to Ultracold Ground State Molecules of $^{23}$Na$^{40}$K
Authors:
Jee Woo Park,
Sebastian A. Will,
Martin W. Zwierlein
Abstract:
We report on high-resolution spectroscopy of ultracold fermionic \nak~Feshbach molecules, and identify a two-photon pathway to the rovibrational singlet ground state via a resonantly mixed \Bcres intermediate state. Photoassociation in a $^{23}$Na-$^{40}$K atomic mixture and one-photon spectroscopy on \nak~Feshbach molecules reveal about 20 vibrational levels of the electronically excited \ctrip s…
▽ More
We report on high-resolution spectroscopy of ultracold fermionic \nak~Feshbach molecules, and identify a two-photon pathway to the rovibrational singlet ground state via a resonantly mixed \Bcres intermediate state. Photoassociation in a $^{23}$Na-$^{40}$K atomic mixture and one-photon spectroscopy on \nak~Feshbach molecules reveal about 20 vibrational levels of the electronically excited \ctrip state. Two of these levels are found to be strongly perturbed by nearby \Bsing states via spin-orbit coupling, resulting in additional lines of dominant singlet character in the perturbed complex {${\rm B}^1Π|v{=}4\rangle {\sim} {\rm c}^3Σ^+ | v{=}25\rangle$}, or of resonantly mixed character in {${\rm B}^1Π| v{=}12 \rangle {\sim}{\rm c}^3Σ^+ | v{=}35 \rangle$}. The dominantly singlet level is used to locate the absolute rovibrational singlet ground state ${\rm X}^1Σ^+ | v{=}0, J{=}0 \rangle$ via Autler-Townes spectroscopy. We demonstrate coherent two-photon coupling via dark state spectroscopy between the predominantly triplet Feshbach molecular state and the singlet ground state. Its binding energy is measured to be 5212.0447(1) \cm, a thousand-fold improvement in accuracy compared to previous determinations. In their absolute singlet ground state, \nak~molecules are chemically stable under binary collisions and possess a large electric dipole moment of $2.72$ Debye. Our work thus paves the way towards the creation of strongly dipolar Fermi gases of NaK molecules.
△ Less
Submitted 7 May, 2015;
originally announced May 2015.
-
Ultracold Dipolar Gas of Fermionic $^{23}$Na$^{40}$K Molecules in their Absolute Ground State
Authors:
Jee Woo Park,
Sebastian A. Will,
Martin W. Zwierlein
Abstract:
We report on the creation of an ultracold dipolar gas of fermionic $^{23}$Na$^{40}$K molecules in their absolute rovibrational and hyperfine ground state. Starting from weakly bound Feshbach molecules, we demonstrate hyperfine resolved two-photon transfer into the singlet ${\rm X}^1Σ^+ |v{=}0,J{=}0\rangle$ ground state, coherently bridging a binding energy difference of 0.65 eV via stimulated rapi…
▽ More
We report on the creation of an ultracold dipolar gas of fermionic $^{23}$Na$^{40}$K molecules in their absolute rovibrational and hyperfine ground state. Starting from weakly bound Feshbach molecules, we demonstrate hyperfine resolved two-photon transfer into the singlet ${\rm X}^1Σ^+ |v{=}0,J{=}0\rangle$ ground state, coherently bridging a binding energy difference of 0.65 eV via stimulated rapid adiabatic passage. The spin-polarized, nearly quantum degenerate molecular gas displays a lifetime longer than 2.5 s, highlighting NaK's stability against two-body chemical reactions. A homogeneous electric field is applied to induce a dipole moment of up to 0.8 Debye. With these advances, the exploration of many-body physics with strongly dipolar Fermi gases of $^{23}$Na$^{40}$K molecules is in experimental reach.
△ Less
Submitted 3 May, 2015;
originally announced May 2015.
