arXiv subjects

Taylor Johnson

Publications and source records attributed to Taylor Johnson.

6 recordsLinked to original sources

arXiv2026

Engineering Reliable Autonomous Systems: Challenges and Solutions

Engineering reliable autonomous systems is an important and growing topic in computer science. As autonomous systems become more prevalent, easy-to-use techniques for building them reliably are increasingly important. This workshop report captures and expands on the discussions at the Lorentz Center Workshop "Engineering Reliable Autonomous Systems" (ERAS), held from 10 to 14 June 2024. The workshop was co-organised by the organisers of the Workshop on Formal Methods for Autonomous Systems (FMAS) and the Workshop on Agents and Robots for reliable Engineered Autonomy (AREA). It brought together members of the FMAS and AREA communities, industry practitioners, and representatives from sectors where autonomous systems pose distinctive engineering challenges. The workshop focused on three main research topics: techniques for verification and validation of autonomous systems; engineering real-world autonomous systems; and software architectures for safe autonomous systems. Its main outcome is a catalogue of challenges in these areas and, most importantly, a pathway to solutions. Some challenges can already be tackled by techniques that are well known in academia but have not yet become regularly used in practice. Other challenges remain unresolved and require further research. This roadmap is intended to support future research and industrial collaboration.

cs.RO↗

arXiv2024

QRIS: A Quantitative Reflectance Imaging System for the Pristine Sample of Asteroid Bennu

The Quantitative Reflectance Imaging System (QRIS) is a laboratory-based spectral imaging system constructed to image the sample of asteroid Bennu delivered to Earth by the Origins, Spectral Interpretation, Resource Identification, and Security-Regolith Explorer (OSIRIS-REx) spacecraft. The system was installed in the OSIRIS-REx cleanroom at NASA's Johnson Space Center to collect data during preliminary examination of the Bennu sample. QRIS uses a 12-bit machine vision camera to measure reflectance over wavelength bands spanning the near ultraviolet to the near infrared. Raw data are processed by a calibration pipeline that generates a series of monochromatic, high-dynamic-range reflectance images, as well as band ratio maps, band depth maps, and 3-channel color images. The purpose of these spectral reflectance data is to help characterize lithologies in the sample and compare them to lithologies observed on Bennu by the OSIRIS-REx spacecraft. This initial assessment of lithological diversity was intended to help select the subsamples that will be used to address mission science questions about the early solar system and the origins of life and to provide important context for the selection of representative subsamples for preservation and distribution to international partners. When QRIS imaged the Bennu sample, unexpected calibration issues arose that had not been evident at imaging rehearsals and negatively impacted the quality of QRIS data. These issues were caused by stray light within the lens and reflections off the glovebox window and interior, and were exacerbated by the sample's extremely low reflectance. QRIS data were useful for confirming conclusions drawn from other data, but reflectance and spectral data from QRIS alone unfortunately have limited utility.

astro-ph.EP↗

arXiv2023

EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability

Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) are widely used in automated verification, but there is a lack of interactive tools designed for educational purposes in this field. To address this gap, we present EduSAT, a pedagogical tool specifically developed to support learning and understanding of SAT and SMT solving. EduSAT offers implementations of key algorithms such as the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and the Reduced Order Binary Decision Diagram (ROBDD) for SAT solving. Additionally, EduSAT provides solver abstractions for five NP-complete problems beyond SAT and SMT. Users can benefit from EduSAT by experimenting, analyzing, and validating their understanding of SAT and SMT solving techniques. Our tool is accompanied by comprehensive documentation and tutorials, extensive testing, and practical features such as a natural language interface and SAT and SMT formula generators, which also serve as a valuable opportunity for learners to deepen their understanding. Our evaluation of EduSAT demonstrates its high accuracy, achieving 100% correctness across all the implemented SAT and SMT solvers. We release EduSAT as a python package in .whl file, and the source can be identified at https://github.com/zhaoy37/SAT_Solver.

cs.AI↗

arXiv2021

The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results

This report summarizes the second International Verification of Neural Networks Competition (VNN-COMP 2021), held as a part of the 4th Workshop on Formal Methods for ML-Enabled Autonomous Systems that was collocated with the 33rd International Conference on Computer-Aided Verification (CAV). Twelve teams participated in this competition. The goal of the competition is to provide an objective comparison of the state-of-the-art methods in neural network verification, in terms of scalability and speed. Along this line, we used standard formats (ONNX for neural networks and VNNLIB for specifications), standard hardware (all tools are run by the organizers on AWS), and tool parameters provided by the tool authors. This report summarizes the rules, benchmarks, participating tools, results, and lessons learned from this competition.

cs.LO↗

arXiv2020

Reachability Analysis for Feed-Forward Neural Networks using Face Lattices

Deep neural networks have been widely applied as an effective approach to handle complex and practical problems. However, one of the most fundamental open problems is the lack of formal methods to analyze the safety of their behaviors. To address this challenge, we propose a parallelizable technique to compute exact reachable sets of a neural network to an input set. Our method currently focuses on feed-forward neural networks with ReLU activation functions. One of the primary challenges for polytope-based approaches is identifying the intersection between intermediate polytopes and hyperplanes from neurons. In this regard, we present a new approach to construct the polytopes with the face lattice, a complete combinatorial structure. The correctness and performance of our methodology are evaluated by verifying the safety of ACAS Xu networks and other benchmarks. Compared to state-of-the-art methods such as Reluplex, Marabou, and NNV, our approach exhibits a significantly higher efficiency. Additionally, our approach is capable of constructing the complete input set given an output set, so that any input that leads to safety violation can be tracked.

cs.AI↗

arXiv2014

The NUbots Team Description Paper 2014

The NUbots team, from The University of Newcastle, Australia, has had a strong record of success in the RoboCup Standard Platform League since first entering in 2002. The team has also competed within the RoboCup Humanoid Kid-Size League since 2012. The 2014 team brings a renewed focus on software architecture, modularity, and the ability to easily share code. This paper summarizes the history of the NUbots team, describes the roles and research of the team members, gives an overview of the NUbots' robots and software system, and addresses relevant research projects within the the Newcastle Robotics Laboratory.

cs.RO↗