Showing 1–25 of 25 results for author: Johnson, T

Enviro-IoT: Calibrating Low-Cost Environmental Sensors in Urban Settings

Authors: Thomas Johnson, Kieran Woodward

Abstract: Low-cost miniaturised sensors offer significant advantage to monitor the environment in real-time and accurately. The area of air quality monitoring has attracted much attention in recent years because of the increasing impacts on the environment and more personally to human health and mental wellbeing. Rapid growth in sensors and Internet of Things (IoT) technologies is paving the way for low-cos… ▽ More Low-cost miniaturised sensors offer significant advantage to monitor the environment in real-time and accurately. The area of air quality monitoring has attracted much attention in recent years because of the increasing impacts on the environment and more personally to human health and mental wellbeing. Rapid growth in sensors and Internet of Things (IoT) technologies is paving the way for low-cost systems to transform global monitoring of air quality. Drawing on 4 years of development work, in this paper we outline the design, implementation and analysis of \textit{Enviro-IoT} as a step forward to monitoring air quality levels within urban environments by means of a low-cost sensing system. An in-the-wild study for 9-months was performed to evaluate the Enviro-IoT system against industry standard equipment is performed with accuracy for measuring Particulate Matter 2.5, 10 and Nitrogen Dioxide achieving 98\%, 97\% and 97\% respectively. The results in this case study are made up Of 57, 120 which highlight that it is possible to take advantage of low-cost sensors coupled with IoT technologies to validate the Enviro-IoT device against research-grade industrial instruments. △ Less

Submitted 11 February, 2025; originally announced February 2025.

A New Hybrid Automaton Framework with Partial Differential Equation Dynamics

Authors: Tianshu Bao, Hengrong Du, Weiming Xiang, Taylor T. Johnson

Abstract: This paper presents the syntax and semantics of a novel type of hybrid automaton (HA) with partial differential equation (PDE) dynamic, partial differential hybrid automata (PDHA). In PDHA, we add a spatial domain $X$ and harness a mathematic conception, partition, to help us formally define the spatial relations. While classically the dynamics of HA are described by ordinary differential equation… ▽ More This paper presents the syntax and semantics of a novel type of hybrid automaton (HA) with partial differential equation (PDE) dynamic, partial differential hybrid automata (PDHA). In PDHA, we add a spatial domain $X$ and harness a mathematic conception, partition, to help us formally define the spatial relations. While classically the dynamics of HA are described by ordinary differential equations (ODEs) and differential inclusions, PDHA is capable of describing the behavior of cyber-physical systems (CPS) with continuous dynamics that cannot be modelled using the canonical hybrid systems' framework. For the purposes of analyzing PDHA, we propose another model called the discrete space partial differential hybrid automata (DSPDHA) which handles discrete spatial domains using finite difference methods (FDM) and this simple and intuitive approach reduces the PDHA into HA with ODE systems. We conclude with two illustrative examples in order to exhibit the nature of PDHA and DSPDHA. △ Less

Submitted 18 April, 2024; originally announced April 2024.

Comments: 17 pages

Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach

Authors: Neelanjana Pal, Taylor T Johnson

Abstract: Formally verifying audio classification systems is essential to ensure accurate signal classification across real-world applications like surveillance, automotive voice commands, and multimedia content management, preventing potential errors with serious consequences. Drawing from recent research, this study advances the utilization of star-set-based formal verification, extended through reachabil… ▽ More Formally verifying audio classification systems is essential to ensure accurate signal classification across real-world applications like surveillance, automotive voice commands, and multimedia content management, preventing potential errors with serious consequences. Drawing from recent research, this study advances the utilization of star-set-based formal verification, extended through reachability analysis, tailored explicitly for Long Short-Term Memory architectures and their Convolutional variations within the audio classification domain. By conceptualizing the classification process as a sequence of set operations, the star set-based reachability approach streamlines the exploration of potential operational states attainable by the system. The paper serves as an encompassing case study, validating and verifying sequence audio classification analytics within real-world contexts. It accentuates the necessity for robustness verification to ensure precise and dependable predictions, particularly in light of the impact of noise on the accuracy of output classifications. △ Less

Submitted 16 November, 2023; originally announced November 2023.

Comments: In Proceedings FMAS 2023, arXiv:2311.08987

Journal ref: EPTCS 395, 2023, pp. 162-179

Accurate synthesis of Dysarthric Speech for ASR data augmentation

Authors: Mohammad Soleymanpour, Michael T. Johnson, Rahim Soleymanpour, Jeffrey Berry

Abstract: Dysarthria is a motor speech disorder often characterized by reduced speech intelligibility through slow, uncoordinated control of speech production muscles. Automatic Speech recognition (ASR) systems can help dysarthric talkers communicate more effectively. However, robust dysarthria-specific ASR requires a significant amount of training speech, which is not readily available for dysarthric talke… ▽ More Dysarthria is a motor speech disorder often characterized by reduced speech intelligibility through slow, uncoordinated control of speech production muscles. Automatic Speech recognition (ASR) systems can help dysarthric talkers communicate more effectively. However, robust dysarthria-specific ASR requires a significant amount of training speech, which is not readily available for dysarthric talkers. This paper presents a new dysarthric speech synthesis method for the purpose of ASR training data augmentation. Differences in prosodic and acoustic characteristics of dysarthric spontaneous speech at varying severity levels are important components for dysarthric speech modeling, synthesis, and augmentation. For dysarthric speech synthesis, a modified neural multi-talker TTS is implemented by adding a dysarthria severity level coefficient and a pause insertion model to synthesize dysarthric speech for varying severity levels. To evaluate the effectiveness for synthesis of training data for ASR, dysarthria-specific speech recognition was used. Results show that a DNN-HMM model trained on additional synthetic dysarthric speech achieves WER improvement of 12.2% compared to the baseline, and that the addition of the severity level and pause insertion controls decrease WER by 6.5%, showing the effectiveness of adding these parameters. Overall results on the TORGO database demonstrate that using dysarthric synthetic speech to increase the amount of dysarthric-patterned speech for training has significant impact on the dysarthric ASR systems. In addition, we have conducted a subjective evaluation to evaluate the dysarthric-ness and similarity of synthesized speech. Our subjective evaluation shows that the perceived dysartrhic-ness of synthesized speech is similar to that of true dysarthric speech, especially for higher levels of dysarthria △ Less

Submitted 16 August, 2023; originally announced August 2023.

Comments: arXiv admin note: text overlap with arXiv:2201.11571

Ablation Study of How Run Time Assurance Impacts the Training and Performance of Reinforcement Learning Agents

Authors: Nathaniel Hamilton, Kyle Dunlap, Taylor T Johnson, Kerianne L Hobbs

Abstract: Reinforcement Learning (RL) has become an increasingly important research area as the success of machine learning algorithms and methods grows. To combat the safety concerns surrounding the freedom given to RL agents while training, there has been an increase in work concerning Safe Reinforcement Learning (SRL). However, these new and safe methods have been held to less scrutiny than their unsafe… ▽ More Reinforcement Learning (RL) has become an increasingly important research area as the success of machine learning algorithms and methods grows. To combat the safety concerns surrounding the freedom given to RL agents while training, there has been an increase in work concerning Safe Reinforcement Learning (SRL). However, these new and safe methods have been held to less scrutiny than their unsafe counterparts. For instance, comparisons among safe methods often lack fair evaluation across similar initial condition bounds and hyperparameter settings, use poor evaluation metrics, and cherry-pick the best training runs rather than averaging over multiple random seeds. In this work, we conduct an ablation study using evaluation best practices to investigate the impact of run time assurance (RTA), which monitors the system state and intervenes to assure safety, on effective learning. By studying multiple RTA approaches in both on-policy and off-policy RL algorithms, we seek to understand which RTA methods are most effective, whether the agents become dependent on the RTA, and the importance of reward shaping versus safe exploration in RL agent training. Our conclusions shed light on the most promising directions of SRL, and our evaluation methodology lays the groundwork for creating better comparisons in future SRL work. △ Less

Submitted 8 July, 2022; originally announced July 2022.

Journal ref: 2023 IEEE 9th International Conference on Space Mission Challenges for Information Technology (SMC-IT), 2023, pp. 45-55

Topological Simplification of Signals for Inference and Approximate Reconstruction

Authors: Gary Koplik, Nathan Borggren, Sam Voisin, Gabrielle Angeloro, Jay Hineman, Tessa Johnson, Paul Bendich

Abstract: As Internet of Things (IoT) devices become both cheaper and more powerful, researchers are increasingly finding solutions to their scientific curiosities both financially and computationally feasible. When operating with restricted power or communications budgets, however, devices can only send highly-compressed data. Such circumstances are common for devices placed away from electric grids that c… ▽ More As Internet of Things (IoT) devices become both cheaper and more powerful, researchers are increasingly finding solutions to their scientific curiosities both financially and computationally feasible. When operating with restricted power or communications budgets, however, devices can only send highly-compressed data. Such circumstances are common for devices placed away from electric grids that can only communicate via satellite, a situation particularly plausible for environmental sensor networks. These restrictions can be further complicated by potential variability in the communications budget, for example a solar-powered device needing to expend less energy when transmitting data on a cloudy day. We propose a novel, topology-based, lossy compression method well-equipped for these restrictive yet variable circumstances. This technique, Topological Signal Compression, allows sending compressed signals that utilize the entirety of a variable communications budget. To demonstrate our algorithm's capabilities, we perform entropy calculations as well as a classification exercise on increasingly topologically simplified signals from the Free-Spoken Digit Dataset and explore the stability of the resulting performance against common baselines. △ Less

Submitted 25 May, 2022; originally announced June 2022.

Comments: 10 pages, 12 figures

An Empirical Analysis of the Use of Real-Time Reachability for the Safety Assurance of Autonomous Vehicles

Authors: Patrick Musau, Nathaniel Hamilton, Diego Manzanas Lopez, Preston Robinette, Taylor T. Johnson

Abstract: Recent advances in machine learning technologies and sensing have paved the way for the belief that safe, accessible, and convenient autonomous vehicles may be realized in the near future. Despite tremendous advances within this context, fundamental challenges around safety and reliability are limiting their arrival and comprehensive adoption. Autonomous vehicles are often tasked with operating in… ▽ More Recent advances in machine learning technologies and sensing have paved the way for the belief that safe, accessible, and convenient autonomous vehicles may be realized in the near future. Despite tremendous advances within this context, fundamental challenges around safety and reliability are limiting their arrival and comprehensive adoption. Autonomous vehicles are often tasked with operating in dynamic and uncertain environments. As a result, they often make use of highly complex components, such as machine learning approaches, to handle the nuances of sensing, actuation, and control. While these methods are highly effective, they are notoriously difficult to assure. Moreover, within uncertain and dynamic environments, design time assurance analyses may not be sufficient to guarantee safety. Thus, it is critical to monitor the correctness of these systems at runtime. One approach for providing runtime assurance of systems with components that may not be amenable to formal analysis is the simplex architecture, where an unverified component is wrapped with a safety controller and a switching logic designed to prevent dangerous behavior. In this paper, we propose using a real-time reachability algorithm for the implementation of the simplex architecture to assure the safety of a 1/10 scale open source autonomous vehicle platform known as F1/10. The reachability algorithm that we leverage (a) provides provable guarantees of safety, and (b) is used to detect potentially unsafe scenarios. In our approach, the need to analyze an underlying controller is abstracted away, instead focusing on the effects of the controller's decisions on the system's future states. We demonstrate the efficacy of our architecture through a vast set of experiments conducted both in simulation and on an embedded hardware platform. △ Less

Submitted 3 May, 2022; originally announced May 2022.

Comments: 30 pages, 12 Figures, Submitted to Artificial Intelligence's Special Issue on "Risk-Aware Autonomous Systems: Theory and Practice."

Synthesizing Dysarthric Speech Using Multi-talker TTS for Dysarthric Speech Recognition

Authors: Mohammad Soleymanpour, Michael T. Johnson, Rahim Soleymanpour, Jeffrey Berry

Abstract: Dysarthria is a motor speech disorder often characterized by reduced speech intelligibility through slow, uncoordinated control of speech production muscles. Automatic Speech recognition (ASR) systems may help dysarthric talkers communicate more effectively. To have robust dysarthria-specific ASR, sufficient training speech is required, which is not readily available. Recent advances in Text-To-Sp… ▽ More Dysarthria is a motor speech disorder often characterized by reduced speech intelligibility through slow, uncoordinated control of speech production muscles. Automatic Speech recognition (ASR) systems may help dysarthric talkers communicate more effectively. To have robust dysarthria-specific ASR, sufficient training speech is required, which is not readily available. Recent advances in Text-To-Speech (TTS) synthesis multi-speaker end-to-end TTS systems suggest the possibility of using synthesis for data augmentation. In this paper, we aim to improve multi-speaker end-to-end TTS systems to synthesize dysarthric speech for improved training of a dysarthria-specific DNN-HMM ASR. In the synthesized speech, we add dysarthria severity level and pause insertion mechanisms to other control parameters such as pitch, energy, and duration. Results show that a DNN-HMM model trained on additional synthetic dysarthric speech achieves WER improvement of 12.2% compared to the baseline, the addition of the severity level and pause insertion controls decrease WER by 6.5%, showing the effectiveness of adding these parameters. Audio samples are available at △ Less

Submitted 27 January, 2022; originally announced January 2022.

Comments: Accepted ICASSP 2022

Full Attention Bidirectional Deep Learning Structure for Single Channel Speech Enhancement

Authors: Yuzi Yan, Wei-Qiang Zhang, Michael T. Johnson

Abstract: As the cornerstone of other important technologies, such as speech recognition and speech synthesis, speech enhancement is a critical area in audio signal processing. In this paper, a new deep learning structure for speech enhancement is demonstrated. The model introduces a "full" attention mechanism to a bidirectional sequence-to-sequence method to make use of latent information after each focal… ▽ More As the cornerstone of other important technologies, such as speech recognition and speech synthesis, speech enhancement is a critical area in audio signal processing. In this paper, a new deep learning structure for speech enhancement is demonstrated. The model introduces a "full" attention mechanism to a bidirectional sequence-to-sequence method to make use of latent information after each focal frame. This is an extension of the previous attention-based RNN method. The proposed bidirectional attention-based architecture achieves better performance in terms of speech quality (PESQ), compared with OM-LSA, CNN-LSTM, T-GSA and the unidirectional attention-based LSTM baseline. △ Less

Submitted 26 August, 2021; originally announced August 2021.

Comments: 4 pages

Resonant Processing of Instrumental Sound Controlled by Spatial Position

Authors: Camille Goudeseune, Guy Garnett, Timothy Johnson

Abstract: We present an acoustic musical instrument played through a resonance model of another sound. The resonance model is controlled in real time as part of the composite instrument. Our implementation uses an electric violin, whose spatial position modifies filter parameters of the resonance model. Simplicial interpolation defines the mapping from spatial position to filter parameters. With some effort… ▽ More We present an acoustic musical instrument played through a resonance model of another sound. The resonance model is controlled in real time as part of the composite instrument. Our implementation uses an electric violin, whose spatial position modifies filter parameters of the resonance model. Simplicial interpolation defines the mapping from spatial position to filter parameters. With some effort, pitch tracking can also control the filter parameters. The individual technologies -- motion tracking, pitch tracking, resonance models -- are easily adapted to other instruments. △ Less

Submitted 4 October, 2020; originally announced October 2020.

Comments: Proceedings of the International Conference on New Interfaces for Musical Expression, 2001

ACM Class: H.5.5

Articulatory-WaveNet: Autoregressive Model For Acoustic-to-Articulatory Inversion

Authors: Narjes Bozorg, Michael T. Johnson

Abstract: This paper presents Articulatory-WaveNet, a new approach for acoustic-to-articulator inversion. The proposed system uses the WaveNet speech synthesis architecture, with dilated causal convolutional layers using previous values of the predicted articulatory trajectories conditioned on acoustic features. The system was trained and evaluated on the ElectroMagnetic Articulography corpus of Mandarin Ac… ▽ More This paper presents Articulatory-WaveNet, a new approach for acoustic-to-articulator inversion. The proposed system uses the WaveNet speech synthesis architecture, with dilated causal convolutional layers using previous values of the predicted articulatory trajectories conditioned on acoustic features. The system was trained and evaluated on the ElectroMagnetic Articulography corpus of Mandarin Accented English (EMA-MAE),consisting of 39 speakers including both native English speakers and native Mandarin speakers speaking English. Results show significant improvement in both correlation and RMSE between the generated and true articulatory trajectories for the new method, with an average correlation of 0.83, representing a 36% relative improvement over the 0.61 correlation obtained with a baseline Hidden Markov Model (HMM)-Gaussian Mixture Model (GMM) inversion framework. To the best of our knowledge, this paper presents the first application of a point-by-point waveform synthesis approach to the problem of acoustic-to-articulatory inversion and the results show improved performance compared to previous methods for speaker dependent acoustic to articulatory inversion. △ Less

Submitted 22 June, 2020; originally announced June 2020.

Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach

Authors: Weiming Xiang, Hoang-Dung Tran, Xiaodong Yang, Taylor T. Johnson

Abstract: The vulnerability of artificial intelligence (AI) and machine learning (ML) against adversarial disturbances and attacks significantly restricts their applicability in safety-critical systems including cyber-physical systems (CPS) equipped with neural network components at various stages of sensing and control. This paper addresses the reachable set estimation and safety verification problems for… ▽ More The vulnerability of artificial intelligence (AI) and machine learning (ML) against adversarial disturbances and attacks significantly restricts their applicability in safety-critical systems including cyber-physical systems (CPS) equipped with neural network components at various stages of sensing and control. This paper addresses the reachable set estimation and safety verification problems for dynamical systems embedded with neural network components serving as feedback controllers. The closed-loop system can be abstracted in the form of a continuous-time sampled-data system under the control of a neural network controller. First, a novel reachable set computation method in adaptation to simulations generated out of neural networks is developed. The reachability analysis of a class of feedforward neural networks called multilayer perceptrons (MLP) with general activation functions is performed in the framework of interval arithmetic. Then, in combination with reachability methods developed for various dynamical system classes modeled by ordinary differential equations, a recursive algorithm is developed for over-approximating the reachable set of the closed-loop system. The safety verification for neural network control systems can be performed by examining the emptiness of the intersection between the over-approximation of reachable sets and unsafe sets. The effectiveness of the proposed approach has been validated with evaluations on a robotic arm model and an adaptive cruise control system. △ Less

Submitted 25 April, 2020; originally announced April 2020.

Comments: 10 pages, 8 figures. IEEE Transactions on Neural Networks and Learning Systems

NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems

Authors: Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson

Abstract: This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exa… ▽ More This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exact (sound and complete) and over-approximate (sound) reachability algorithms for verifying safety and robustness properties of feed-forward neural networks (FFNNs) with various activation functions. For learning-enabled CPS, such as closed-loop control systems incorporating neural networks, NNV provides exact and over-approximate reachability analysis schemes for linear plant models and FFNN controllers with piecewise-linear activation functions, such as ReLUs. For similar neural network control systems (NNCS) that instead have nonlinear plant models, NNV supports over-approximate analysis by combining the star set analysis used for FFNN controllers with zonotope-based analysis for nonlinear plant dynamics building on CORA. We evaluate NNV using two real-world case studies: the first is safety verification of ACAS Xu networks and the second deals with the safety verification of a deep learning-based adaptive cruise control system. △ Less

Submitted 11 April, 2020; originally announced April 2020.

Latent Class Model with Application to Speaker Diarization

Authors: Liang He, Xianhong Chen, Can Xu, Yi Liu, Jia Liu, Michael T Johnson

Abstract: In this paper, we apply a latent class model (LCM) to the task of speaker diarization. LCM is similar to Patrick Kenny's variational Bayes (VB) method in that it uses soft information and avoids premature hard decisions in its iterations. In contrast to the VB method, which is based on a generative model, LCM provides a framework allowing both generative and discriminative models. The discriminati… ▽ More In this paper, we apply a latent class model (LCM) to the task of speaker diarization. LCM is similar to Patrick Kenny's variational Bayes (VB) method in that it uses soft information and avoids premature hard decisions in its iterations. In contrast to the VB method, which is based on a generative model, LCM provides a framework allowing both generative and discriminative models. The discriminative property is realized through the use of i-vector (Ivec), probabilistic linear discriminative analysis (PLDA), and a support vector machine (SVM) in this work. Systems denoted as LCM-Ivec-PLDA, LCM-Ivec-SVM, and LCM-Ivec-Hybrid are introduced. In addition, three further improvements are applied to enhance its performance. 1) Adding neighbor windows to extract more speaker information for each short segment. 2) Using a hidden Markov model to avoid frequent speaker change points. 3) Using an agglomerative hierarchical cluster to do initialization and present hard and soft priors, in order to overcome the problem of initial sensitivity. Experiments on the National Institute of Standards and Technology Rich Transcription 2009 speaker diarization database, under the condition of a single distant microphone, show that the diarization error rate (DER) of the proposed methods has substantial relative improvements compared with mainstream systems. Compared to the VB method, the relative improvements of LCM-Ivec-PLDA, LCM-Ivec-SVM, and LCM-Ivec-Hybrid systems are 23.5%, 27.1%, and 43.0%, respectively. Experiments on our collected database, CALLHOME97, CALLHOME00 and SRE08 short2-summed trial conditions also show that the proposed LCM-Ivec-Hybrid system has the best overall performance. △ Less

Submitted 24 April, 2019; originally announced April 2019.

Cyber-Physical Specification Mismatches

Authors: Luan V. Nguyen, Khaza Anuarul Hoque, Stanley Bak, Steven Drager, Taylor T. Johnson

Abstract: Embedded systems use increasingly complex software and are evolving into cyber-physical systems (CPS) with sophisticated interaction and coupling between physical and computational processes. Many CPS operate in safety-critical environments and have stringent certification, reliability, and correctness requirements. These systems undergo changes throughout their lifetimes, where either the softwar… ▽ More Embedded systems use increasingly complex software and are evolving into cyber-physical systems (CPS) with sophisticated interaction and coupling between physical and computational processes. Many CPS operate in safety-critical environments and have stringent certification, reliability, and correctness requirements. These systems undergo changes throughout their lifetimes, where either the software or physical hardware is updated in subsequent design iterations. One source of failure in safety-critical CPS is when there are unstated assumptions in either the physical or cyber parts of the system, and new components do not match those assumptions. In this work, we present an automated method towards identifying unstated assumptions in CPS. Dynamic specifications in the form of candidate invariants of both the software and physical components are identified using dynamic analysis (executing and/or simulating the system implementation or model thereof). A prototype tool called Hynger (for HYbrid iNvariant GEneratoR) was developed that instruments Simulink/Stateflow (SLSF) model diagrams to generate traces in the input format compatible with the Daikon invariant inference tool, which has been extensively applied to software systems. Hynger, in conjunction with Daikon, is able to detect candidate invariants of several CPS case studies. We use the running example of a DC-to-DC power converter, and demonstrate that Hynger can detect a specification mismatch where a tolerance assumed by the software is violated due to a plant change. Another case study of an automotive control system is also introduced to illustrate the power of Hynger and Daikon in automatically identifying cyber-physical specification mismatches. △ Less

Submitted 24 June, 2018; originally announced June 2018.

Reachability Analysis and Safety Verification for Neural Network Control Systems

Authors: Weiming Xiang, Taylor T. Johnson

Abstract: Autonomous cyber-physical systems (CPS) rely on the correct operation of numerous components, with state-of-the-art methods relying on machine learning (ML) and artificial intelligence (AI) components in various stages of sensing and control. This paper develops methods for estimating the reachable set and verifying safety properties of dynamical systems under control of neural network-based contr… ▽ More Autonomous cyber-physical systems (CPS) rely on the correct operation of numerous components, with state-of-the-art methods relying on machine learning (ML) and artificial intelligence (AI) components in various stages of sensing and control. This paper develops methods for estimating the reachable set and verifying safety properties of dynamical systems under control of neural network-based controllers that may be implemented in embedded software. The neural network controllers we consider are feedforward neural networks called multilayer perceptrons (MLP) with general activation functions. As such feedforward networks are memoryless, they may be abstractly represented as mathematical functions, and the reachability analysis of the network amounts to range (image) estimation of this function provided a set of inputs. By discretizing the input set of the MLP into a finite number of hyper-rectangular cells, our approach develops a linear programming (LP) based algorithm for over-approximating the output set of the MLP with its input set as a union of hyper-rectangular cells. Combining the over-approximation for the output set of an MLP based controller and reachable set computation routines for ordinary difference/differential equation (ODE) models, an algorithm is developed to estimate the reachable set of the closed-loop system. Finally, safety verification for neural network control systems can be performed by checking the existence of intersections between the estimated reachable set and unsafe regions. The approach is implemented in a computational software prototype and evaluated on numerical examples. △ Less

Submitted 24 May, 2018; originally announced May 2018.

Comments: 21 pages, 6 figures

Speaker Embedding Extraction with Phonetic Information

Authors: Yi Liu, Liang He, Jia Liu, Michael T. Johnson

Abstract: Speaker embeddings achieve promising results on many speaker verification tasks. Phonetic information, as an important component of speech, is rarely considered in the extraction of speaker embeddings. In this paper, we introduce phonetic information to the speaker embedding extraction based on the x-vector architecture. Two methods using phonetic vectors and multi-task learning are proposed. On t… ▽ More Speaker embeddings achieve promising results on many speaker verification tasks. Phonetic information, as an important component of speech, is rarely considered in the extraction of speaker embeddings. In this paper, we introduce phonetic information to the speaker embedding extraction based on the x-vector architecture. Two methods using phonetic vectors and multi-task learning are proposed. On the Fisher dataset, our best system outperforms the original x-vector approach by 20% in EER, and by 15%, 15% in minDCF08 and minDCF10, respectively. Experiments conducted on NIST SRE10 further demonstrate the effectiveness of the proposed methods. △ Less

Submitted 14 June, 2018; v1 submitted 13 April, 2018; originally announced April 2018.

Comments: submitted to Interspeech 2018 (accepted) and open-sourced. Please refer to Interspeech for the final version

Simulation-Based Reachability Analysis for High-Index Large Linear Differential Algebraic Equations

Authors: Hoang-Dung Tran, Weiming Xiang, Nathaniel Hamilton, Taylor T. Johnson

Abstract: Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as differential equations. In the last two decades, numerous reachability analysis methods and tools have been proposed for a common class of dynamics in CPS known as ordinary differential equations (ODE). However, there is… ▽ More Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as differential equations. In the last two decades, numerous reachability analysis methods and tools have been proposed for a common class of dynamics in CPS known as ordinary differential equations (ODE). However, there is lack of methods dealing with differential algebraic equations (DAE) which is a more general class of dynamics that is widely used to describe a variety of problems from engineering and science such as multibody mechanics, electrical cicuit design, incompressible fluids, molecular dynamics and chemcial process control. Reachability analysis for DAE systems is more complex than ODE systems, especially for high-index DAEs because they contain both a differential part (i.e., ODE) and algebraic constraints (AC). In this paper, we extend the recent scalable simulation-based reachability analysis in combination with decoupling techniques for a class of high-index large linear DAEs. In particular, a high-index linear DAE is first decoupled into one ODE and one or several AC subsystems based on the well-known Marz decoupling method ultilizing admissible projectors. Then, the discrete reachable set of the DAE, represented as a list of star-sets, is computed using simulation. Unlike ODE reachability analysis where the initial condition is freely defined by a user, in DAE cases, the consistency of the inititial condition is an essential requirement to guarantee a feasible solution. Therefore, a thorough check for the consistency is invoked before computing the discrete reachable set. Our approach sucessfully verifies (or falsifies) a wide range of practical, high-index linear DAE systems in which the number of state variables varies from several to thousands. △ Less

Submitted 9 April, 2018; originally announced April 2018.

Numerical Verification of Affine Systems with up to a Billion Dimensions

Authors: Stanley Bak, Hoang-Dung Tran, Taylor T. Johnson

Abstract: Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models with inputs, nonlinear differential equations, and hybrid dynamics. As such, the scalability of affine systems verification is a prerequisite to scalable analysis for more complex systems. In this paper, we improve the scalability of affine systems verificati… ▽ More Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models with inputs, nonlinear differential equations, and hybrid dynamics. As such, the scalability of affine systems verification is a prerequisite to scalable analysis for more complex systems. In this paper, we improve the scalability of affine systems verification, in terms of the number of dimensions (variables) in the system. The reachable states of affine systems can be written in terms of the matrix exponential, and safety checking can be performed at specific time steps with linear programming. Unfortunately, for large systems with many state variables, this direct approach requires an intractable amount of memory while using an intractable amount of computation time. We overcome these challenges by combining several methods that leverage common problem structure. Memory is reduced by exploiting initial states that are not full-dimensional and safety properties (outputs) over a few linear projections of the state variables. Computation time is saved by using numerical simulations to compute only projections of the matrix exponential relevant for the verification problem. Since large systems often have sparse dynamics, we use Krylov-subspace simulation approaches based on the Arnoldi or Lanczos iterations. Our method produces accurate counter-examples when properties are violated and, in the extreme case with sufficient problem structure, can analyze a system with one billion real-valued state variables. △ Less

Submitted 5 March, 2019; v1 submitted 4 April, 2018; originally announced April 2018.

Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers

Authors: Weiming Xiang, Hoang-Dung Tran, Joel A. Rosenfeld, Taylor T. Johnson

Abstract: In this work, the reachable set estimation and safety verification problems for a class of piecewise linear systems equipped with neural network controllers are addressed. The neural network is considered to consist of Rectified Linear Unit (ReLU) activation functions. A layer-by-layer approach is developed for the output reachable set computation of ReLU neural networks. The computation is formul… ▽ More In this work, the reachable set estimation and safety verification problems for a class of piecewise linear systems equipped with neural network controllers are addressed. The neural network is considered to consist of Rectified Linear Unit (ReLU) activation functions. A layer-by-layer approach is developed for the output reachable set computation of ReLU neural networks. The computation is formulated in the form of a set of manipulations for a union of polytopes. Based on the output reachable set for neural network controllers, the output reachable set for a piecewise linear feedback control system can be estimated iteratively for a given finite-time interval. With the estimated output reachable set, the safety verification for piecewise linear systems with neural network controllers can be performed by checking the existence of intersections of unsafe regions and output reach set. A numerical example is presented to illustrate the effectiveness of our approach. △ Less

Submitted 20 February, 2018; originally announced February 2018.

Comments: 6 pages, 2 figures, ACC 2018

Reachable Set Estimation and Verification for Neural Network Models of Nonlinear Dynamic Systems

Authors: Weiming Xiang, Diego Manzanas Lopez, Patrick Musau, Taylor T. Johnson

Abstract: Neural networks have been widely used to solve complex real-world problems. Due to the complicate, nonlinear, non-convex nature of neural networks, formal safety guarantees for the behaviors of neural network systems will be crucial for their applications in safety-critical systems. In this paper, the reachable set estimation and verification problems for Nonlinear Autoregressive-Moving Average (N… ▽ More Neural networks have been widely used to solve complex real-world problems. Due to the complicate, nonlinear, non-convex nature of neural networks, formal safety guarantees for the behaviors of neural network systems will be crucial for their applications in safety-critical systems. In this paper, the reachable set estimation and verification problems for Nonlinear Autoregressive-Moving Average (NARMA) models in the forms of neural networks are addressed. The neural network involved in the model is a class of feed-forward neural networks called Multi-Layer Perceptron (MLP). By partitioning the input set of an MLP into a finite number of cells, a layer-by-layer computation algorithm is developed for reachable set estimation for each individual cell. The union of estimated reachable sets of all cells forms an over-approximation of reachable set of the MLP. Furthermore, an iterative reachable set estimation algorithm based on reachable set estimation for MLPs is developed for NARMA models. The safety verification can be performed by checking the existence of intersections of unsafe regions and estimated reachable set. Several numerical examples are provided to illustrate our approach. △ Less

Submitted 10 February, 2018; originally announced February 2018.

Comments: 23 pages, 4 figures

Investigation of Frame Alignments for GMM-based Digit-prompted Speaker Verification

Authors: Yi Liu, Liang He, Weiqiang Zhang, Jia Liu, Michael T. Johnson

Abstract: Frame alignments can be computed by different methods in GMM-based speaker verification. By incorporating a phonetic Gaussian mixture model (PGMM), we are able to compare the performance using alignments extracted from the deep neural networks (DNN) and the conventional hidden Markov model (HMM) in digit-prompted speaker verification. Based on the different characteristics of these two alignments,… ▽ More Frame alignments can be computed by different methods in GMM-based speaker verification. By incorporating a phonetic Gaussian mixture model (PGMM), we are able to compare the performance using alignments extracted from the deep neural networks (DNN) and the conventional hidden Markov model (HMM) in digit-prompted speaker verification. Based on the different characteristics of these two alignments, we present a novel content verification method to improve the system security without much computational overhead. Our experiments on the RSR2015 Part-3 digit-prompted task show that, the DNN based alignment performs on par with the HMM alignment. The results also demonstrate the effectiveness of the proposed Kullback-Leibler (KL) divergence based scoring to reject speech with incorrect pass-phrases. △ Less

Submitted 2 September, 2018; v1 submitted 28 October, 2017; originally announced October 2017.

Comments: accepted by APSIPA ASC 2018

Order-Reduction Abstractions for Safety Verification of High-Dimensional Linear Systems

Authors: Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang, Taylor T. Johnson

Abstract: Order-reduction is a standard automated approximation technique for computer-aided design, analysis, and simulation of many classes of systems, from circuits to buildings. For a given system, these methods produce a reduced-order system where the dimension of the state-space is smaller, while attempting to preserve behaviors similar to those of the full-order original system. To be used as a sound… ▽ More Order-reduction is a standard automated approximation technique for computer-aided design, analysis, and simulation of many classes of systems, from circuits to buildings. For a given system, these methods produce a reduced-order system where the dimension of the state-space is smaller, while attempting to preserve behaviors similar to those of the full-order original system. To be used as a sound abstraction for formal verification, a measure of the similarity of behavior must be formalized and computed, which we develop in a computational way for a class of linear systems and periodically-switched systems as the main contributions of this paper. We have implemented the order-reduction as a sound abstraction process through a source-to-source model transformation in the HyST tool and use SpaceEx to compute sets of reachable states to verify properties of the full-order system through analysis of the reduced-order system. Our experimental results suggest systems with on the order of a thousand state variables can be reduced to systems with tens of state variables such that the order-reduction overapproximation error is small enough to prove or disprove safety properties of interest using current reachability analysis tools. Our results illustrate this approach is effective to alleviate the state-space explosion problem for verification of high-dimensional linear systems. △ Less

Submitted 20 February, 2016; originally announced February 2016.

Comments: Preliminary version under review for Discrete Event Dynamic Systems

Virtual Prototyping and Distributed Control for Solar Array with Distributed Multilevel Inverter

Authors: Luan Viet Nguyen, Taylor T. Johnson

Abstract: In this paper, we present the virtual prototyping of a solar array with a grid-tie implemented as a distributed inverter and controlled using distributed algorithms. Due to the distributed control and inherent redundancy in the array composed of many panels and inverter modules, the virtual prototype exhibits fault-tolerance capabilities. The distributed identifier algorithm allows the system to k… ▽ More In this paper, we present the virtual prototyping of a solar array with a grid-tie implemented as a distributed inverter and controlled using distributed algorithms. Due to the distributed control and inherent redundancy in the array composed of many panels and inverter modules, the virtual prototype exhibits fault-tolerance capabilities. The distributed identifier algorithm allows the system to keep track of the number of operating panels to appropriately regulate the DC voltage output of the panels using buck-boost converters, and determine appropriate switching times for H-bridges in the grid-tie. We evaluate the distributed inverter, its control strategy, and fault-tolerance through simulation in Simulink/Stateflow. Our virtual prototyping framework allows for generating arrays and grid-ties consisting of many panels, and we evaluate arrays of five to dozens of panels. Our analysis suggests the achievable total harmonic distortion (THD) of the system may allow for operating the array in spite of failures of the power electronics, control software, and other subcomponents. △ Less

Submitted 8 April, 2014; originally announced April 2014.

Comments: Preprint draft under review, submitted on March 18, 2014 to IEEE Transactions on Energy Conversion, Special Issue: Advanced Distributed Control of Energy Conversion Devices and Systems

Safe and Stabilizing Distributed Multi-Path Cellular Flows

Authors: Taylor T. Johnson, Sayan Mitra

Abstract: We study the problem of distributed traffic control in the partitioned plane, where the movement of all entities (robots, vehicles, etc.) within each partition (cell) is coupled. Establishing liveness in such systems is challenging, but such analysis will be necessary to apply such distributed traffic control algorithms in applications like coordinating robot swarms and the intelligent highway sys… ▽ More We study the problem of distributed traffic control in the partitioned plane, where the movement of all entities (robots, vehicles, etc.) within each partition (cell) is coupled. Establishing liveness in such systems is challenging, but such analysis will be necessary to apply such distributed traffic control algorithms in applications like coordinating robot swarms and the intelligent highway system. We present a formal model of a distributed traffic control protocol that guarantees minimum separation between entities, even as some cells fail. Once new failures cease occurring, in the case of a single target, the protocol is guaranteed to self-stabilize and the entities with feasible paths to the target cell make progress towards it. For multiple targets, failures may cause deadlocks in the system, so we identify a class of non-deadlocking failures where all entities are able to make progress to their respective targets. The algorithm relies on two general principles: temporary blocking for maintenance of safety and local geographical routing for guaranteeing progress. Our assertional proofs may serve as a template for the analysis of other distributed traffic control protocols. We present simulation results that provide estimates of throughput as a function of entity velocity, safety separation, single-target path complexity, failure-recovery rates, and multi-target path complexity. △ Less

Submitted 11 October, 2012; v1 submitted 10 September, 2012; originally announced September 2012.

Comments: An earlier version of this paper appeared in the 30th IEEE International Conference on Distributed Computing Systems (ICDCS 2010)