Showing 1–46 of 46 results for author: Mitra, S

Are Vision xLSTM Embedded UNet More Reliable in Medical 3D Image Segmentation?

Authors: Pallabi Dutta, Soham Bose, Swalpa Kumar Roy, Sushmita Mitra

Abstract: The advancement of develo** efficient medical image segmentation has evolved from initial dependence on Convolutional Neural Networks (CNNs) to the present investigation of hybrid models that combine CNNs with Vision Transformers. Furthermore, there is an increasing focus on creating architectures that are both high-performing in medical image segmentation tasks and computationally efficient to… ▽ More The advancement of develo** efficient medical image segmentation has evolved from initial dependence on Convolutional Neural Networks (CNNs) to the present investigation of hybrid models that combine CNNs with Vision Transformers. Furthermore, there is an increasing focus on creating architectures that are both high-performing in medical image segmentation tasks and computationally efficient to be deployed on systems with limited resources. Although transformers have several advantages like capturing global dependencies in the input data, they face challenges such as high computational and memory complexity. This paper investigates the integration of CNNs and Vision Extended Long Short-Term Memory (Vision-xLSTM) models by introducing a novel approach called UVixLSTM. The Vision-xLSTM blocks captures temporal and global relationships within the patches extracted from the CNN feature maps. The convolutional feature reconstruction path upsamples the output volume from the Vision-xLSTM blocks to produce the segmentation output. Our primary objective is to propose that Vision-xLSTM forms a reliable backbone for medical image segmentation tasks, offering excellent segmentation performance and reduced computational complexity. UVixLSTM exhibits superior performance compared to state-of-the-art networks on the publicly-available Synapse dataset. Code is available at: https://github.com/duttapallabi2907/UVixLSTM △ Less

Submitted 24 June, 2024; originally announced June 2024.

GenzIQA: Generalized Image Quality Assessment using Prompt-Guided Latent Diffusion Models

Authors: Diptanu De, Shankhanil Mitra, Rajiv Soundararajan

Abstract: The design of no-reference (NR) image quality assessment (IQA) algorithms is extremely important to benchmark and calibrate user experiences in modern visual systems. A major drawback of state-of-the-art NR-IQA methods is their limited ability to generalize across diverse IQA settings with reasonable distribution shifts. Recent text-to-image generative models such as latent diffusion models genera… ▽ More The design of no-reference (NR) image quality assessment (IQA) algorithms is extremely important to benchmark and calibrate user experiences in modern visual systems. A major drawback of state-of-the-art NR-IQA methods is their limited ability to generalize across diverse IQA settings with reasonable distribution shifts. Recent text-to-image generative models such as latent diffusion models generate meaningful visual concepts with fine details related to text concepts. In this work, we leverage the denoising process of such diffusion models for generalized IQA by understanding the degree of alignment between learnable quality-aware text prompts and images. In particular, we learn cross-attention maps from intermediate layers of the denoiser of latent diffusion models to capture quality-aware representations of images. In addition, we also introduce learnable quality-aware text prompts that enable the cross-attention features to be better quality-aware. Our extensive cross database experiments across various user-generated, synthetic, and low-light content-based benchmarking databases show that latent diffusion models can achieve superior generalization in IQA when compared to other methods in the literature. △ Less

Submitted 7 June, 2024; originally announced June 2024.

Searching for Optimal Runtime Assurance via Reachability and Reinforcement Learning

Authors: Kristina Miller, Christopher K. Zeitler, William Shen, Kerianne Hobbs, Sayan Mitra, John Schierman, Mahesh Viswanathan

Abstract: A runtime assurance system (RTA) for a given plant enables the exercise of an untrusted or experimental controller while assuring safety with a backup (or safety) controller. The relevant computational design problem is to create a logic that assures safety by switching to the safety controller as needed, while maximizing some performance criteria, such as the utilization of the untrusted controll… ▽ More A runtime assurance system (RTA) for a given plant enables the exercise of an untrusted or experimental controller while assuring safety with a backup (or safety) controller. The relevant computational design problem is to create a logic that assures safety by switching to the safety controller as needed, while maximizing some performance criteria, such as the utilization of the untrusted controller. Existing RTA design strategies are well-known to be overly conservative and, in principle, can lead to safety violations. In this paper, we formulate the optimal RTA design problem and present a new approach for solving it. Our approach relies on reward sha** and reinforcement learning. It can guarantee safety and leverage machine learning technologies for scalability. We have implemented this algorithm and present experimental results comparing our approach with state-of-the-art reachability and simulation-based RTA approaches in a number of scenarios using aircraft models in 3D space with complex safety requirements. Our approach can guarantee safety while increasing utilization of the experimental controller over existing approaches. △ Less

Submitted 6 October, 2023; originally announced October 2023.

Learning-based Inverse Perception Contracts and Applications

Authors: Dawei Sun, Benjamin C. Yang, Sayan Mitra

Abstract: Perception modules are integral in many modern autonomous systems, but their accuracy can be subject to the vagaries of the environment. In this paper, we propose a learning-based approach that can automatically characterize the error of a perception module from data and use this for safe control. The proposed approach constructs an inverse perception contract (IPC) which generates a set that cont… ▽ More Perception modules are integral in many modern autonomous systems, but their accuracy can be subject to the vagaries of the environment. In this paper, we propose a learning-based approach that can automatically characterize the error of a perception module from data and use this for safe control. The proposed approach constructs an inverse perception contract (IPC) which generates a set that contains the ground-truth value that is being estimated by the perception module, with high probability. We apply the proposed approach to study a vision pipeline deployed on a quadcopter. With the proposed approach, we successfully constructed an IPC for the vision pipeline. We then designed a control algorithm that utilizes the learned IPC, with the goal of landing the quadcopter safely on a landing pad. Experiments show that with the learned IPC, the control algorithm safely landed the quadcopter despite the error from the perception module, while the baseline algorithm without using the learned IPC failed to do so. △ Less

Submitted 3 March, 2024; v1 submitted 23 September, 2023; originally announced September 2023.

Test Time Adaptation for Blind Image Quality Assessment

Authors: Subhadeep Roy, Shankhanil Mitra, Soma Biswas, Rajiv Soundararajan

Abstract: While the design of blind image quality assessment (IQA) algorithms has improved significantly, the distribution shift between the training and testing scenarios often leads to a poor performance of these methods at inference time. This motivates the study of test time adaptation (TTA) techniques to improve their performance at inference time. Existing auxiliary tasks and loss functions used for T… ▽ More While the design of blind image quality assessment (IQA) algorithms has improved significantly, the distribution shift between the training and testing scenarios often leads to a poor performance of these methods at inference time. This motivates the study of test time adaptation (TTA) techniques to improve their performance at inference time. Existing auxiliary tasks and loss functions used for TTA may not be relevant for quality-aware adaptation of the pre-trained model. In this work, we introduce two novel quality-relevant auxiliary tasks at the batch and sample levels to enable TTA for blind IQA. In particular, we introduce a group contrastive loss at the batch level and a relative rank loss at the sample level to make the model quality aware and adapt to the target data. Our experiments reveal that even using a small batch of images from the test distribution helps achieve significant improvement in performance by updating the batch normalization statistics of the source model. △ Less

Submitted 26 September, 2023; v1 submitted 27 July, 2023; originally announced July 2023.

Comments: Accepted to ICCV 2023

Verification of $L_1$ Adaptive Control using Verse Library: A Case Study of Quadrotors

Authors: Lin Song, Yangge Li, Sheng Cheng, Pan Zhao, Sayan Mitra, Naira Hovakimyan

Abstract: $L_1$ adaptive control ($L_1$AC) is a control design technique that can handle a broad class of system uncertainties and provide transient performance guarantees. In this work-in-progress abstract, we discuss how existing formal verification tools can be applied to check the performance of $L_1$AC systems. We show that the theoretical transient performance and robustness guarantees of an $L_1… ▽ More $L_1$ adaptive control ($L_1$AC) is a control design technique that can handle a broad class of system uncertainties and provide transient performance guarantees. In this work-in-progress abstract, we discuss how existing formal verification tools can be applied to check the performance of $L_1$AC systems. We show that the theoretical transient performance and robustness guarantees of an $L_1$ adaptive controller for an 18-dimensional quadrotor system can be verified using the recently developed Verse reachability analysis tool. We will further consider the performance verification of $L_1$AC on systems with learning-enabled components. △ Less

Submitted 24 March, 2023; originally announced March 2023.

Comments: accepted to ICCPS-wip 2023

Composite Deep Network with Feature Weighting for Improved Delineation of COVID Infection in Lung CT

Authors: Pallabi Dutta, Sushmita Mitra

Abstract: An early effective screening and grading of COVID-19 has become imperative towards optimizing the limited available resources of the medical facilities. An automated segmentation of the infected volumes in lung CT is expected to significantly aid in the diagnosis and care of patients. However, an accurate demarcation of lesions remains problematic due to their irregular structure and location(s) w… ▽ More An early effective screening and grading of COVID-19 has become imperative towards optimizing the limited available resources of the medical facilities. An automated segmentation of the infected volumes in lung CT is expected to significantly aid in the diagnosis and care of patients. However, an accurate demarcation of lesions remains problematic due to their irregular structure and location(s) within the lung. A novel deep learning architecture, Composite Deep network with Feature Weighting (CDNetFW), is proposed for efficient delineation of infected regions from lung CT images. Initially a coarser-segmentation is performed directly at shallower levels, thereby facilitating discovery of robust and discriminatory characteristics in the hidden layers. The novel feature weighting module helps prioritise relevant feature maps to be probed, along with those regions containing crucial information within these maps. This is followed by estimating the severity of the disease.The deep network CDNetFW has been shown to outperform several state-of-the-art architectures in the COVID-19 lesion segmentation task, as measured by experimental results on CT slices from publicly available datasets, especially when it comes to defining structures involving complex geometries. △ Less

Submitted 17 February, 2023; v1 submitted 17 January, 2023; originally announced January 2023.

Collective Intelligent Strategy for Improved Segmentation of COVID-19 from CT

Authors: Surochita Pal Das, Sushmita Mitra, B. Uma Shankar

Abstract: The devastation caused by the coronavirus pandemic makes it imperative to design automated techniques for a fast and accurate detection. We propose a novel non-invasive tool, using deep learning and imaging, for delineating COVID-19 infection in lungs. The Ensembling Attention-based Multi-scaled Convolution network (EAMC), employing Leave-One-Patient-Out (LOPO) training, exhibits high sensitivity… ▽ More The devastation caused by the coronavirus pandemic makes it imperative to design automated techniques for a fast and accurate detection. We propose a novel non-invasive tool, using deep learning and imaging, for delineating COVID-19 infection in lungs. The Ensembling Attention-based Multi-scaled Convolution network (EAMC), employing Leave-One-Patient-Out (LOPO) training, exhibits high sensitivity and precision in outlining infected regions along with assessment of severity. The Attention module combines contextual with local information, at multiple scales, for accurate segmentation. Ensemble learning integrates heterogeneity of decision through different base classifiers. The superiority of EAMC, even with severe class imbalance, is established through comparison with existing state-of-the-art learning models over four publicly-available COVID-19 datasets. The results are suggestive of the relevance of deep learning in providing assistive intelligence to medical practitioners, when they are overburdened with patients as in pandemics. Its clinical significance lies in its unprecedented scope in providing low-cost decision-making for patients lacking specialized healthcare at remote locations. △ Less

Submitted 23 December, 2022; originally announced December 2022.

Semi-supervised Learning of Perceptual Video Quality by Generating Consistent Pairwise Pseudo-Ranks

Authors: Shankhanil Mitra, Saiyam Jogani, Rajiv Soundararajan

Abstract: Designing learning-based no-reference (NR) video quality assessment (VQA) algorithms for camera-captured videos is cumbersome due to the requirement of a large number of human annotations of quality. In this work, we propose a semi-supervised learning (SSL) framework exploiting many unlabelled and very limited amounts of labelled authentically distorted videos. Our main contributions are two-fold.… ▽ More Designing learning-based no-reference (NR) video quality assessment (VQA) algorithms for camera-captured videos is cumbersome due to the requirement of a large number of human annotations of quality. In this work, we propose a semi-supervised learning (SSL) framework exploiting many unlabelled and very limited amounts of labelled authentically distorted videos. Our main contributions are two-fold. Leveraging the benefits of consistency regularization and pseudo-labelling, our SSL model generates pairwise pseudo-ranks for the unlabelled videos using a student-teacher model on strongweak augmented videos. We design the strong-weak augmentations to be quality invariant to use the unlabelled videos effectively in SSL. The generated pseudo-ranks are used along with the limited labels to train our SSL model. Our primary focus in SSL for NR VQA is to learn the map** from video feature representations to the quality scores. We compare various feature extraction methods and show that our SSL framework can lead to improved performance on these features. In addition to the existing features, we present a spatial and temporal feature extraction method based on predicting spatial and temporal entropic differences. We show that these features help achieve a robust performance when trained with limited data providing a better baseline to apply SSL. Extensive experiments on three popular VQA datasets demonstrate that a combination of our novel SSL approach and features achieves an impressive performance in terms of correlation with human perception, even though the number of human-annotated videos may be limited. △ Less

Submitted 30 November, 2022; originally announced November 2022.

Full-scale Deeply Supervised Attention Network for Segmenting COVID-19 Lesions

Authors: Pallabi Dutta, Sushmita Mitra

Abstract: Automated delineation of COVID-19 lesions from lung CT scans aids the diagnosis and prognosis for patients. The asymmetric shapes and positioning of the infected regions make the task extremely difficult. Capturing information at multiple scales will assist in deciphering features, at global and local levels, to encompass lesions of variable size and texture. We introduce the Full-scale Deeply Sup… ▽ More Automated delineation of COVID-19 lesions from lung CT scans aids the diagnosis and prognosis for patients. The asymmetric shapes and positioning of the infected regions make the task extremely difficult. Capturing information at multiple scales will assist in deciphering features, at global and local levels, to encompass lesions of variable size and texture. We introduce the Full-scale Deeply Supervised Attention Network (FuDSA-Net), for efficient segmentation of corona-infected lung areas in CT images. The model considers activation responses from all levels of the encoding path, encompassing multi-scalar features acquired at different levels of the network. This helps segment target regions (lesions) of varying shape, size and contrast. Incorporation of the entire gamut of multi-scalar characteristics into the novel attention mechanism helps prioritize the selection of activation responses and locations containing useful information. Determining robust and discriminatory features along the decoder path is facilitated with deep supervision. Connections in the decoder arm are remodeled to handle the issue of vanishing gradient. As observed from the experimental results, FuDSA-Net surpasses other state-of-the-art architectures; especially, when it comes to characterizing complicated geometries of the lesions. △ Less

Submitted 27 October, 2022; originally announced October 2022.

Learning Certifiably Robust Controllers Using Fragile Perception

Authors: Dawei Sun, Negin Musavi, Geir Dullerud, Sanjay Shakkottai, Sayan Mitra

Abstract: Advances in computer vision and machine learning enable robots to perceive their surroundings in powerful new ways, but these perception modules have well-known fragilities. We consider the problem of synthesizing a safe controller that is robust despite perception errors. The proposed method constructs a state estimator based on Gaussian processes with input-dependent noises. This estimator compu… ▽ More Advances in computer vision and machine learning enable robots to perceive their surroundings in powerful new ways, but these perception modules have well-known fragilities. We consider the problem of synthesizing a safe controller that is robust despite perception errors. The proposed method constructs a state estimator based on Gaussian processes with input-dependent noises. This estimator computes a high-confidence set for the actual state given a perceived state. Then, a robust neural network controller is synthesized that can provably handle the state uncertainty. Furthermore, an adaptive sampling algorithm is proposed to jointly improve the estimator and controller. Simulation experiments, including a realistic vision-based lane-kee** example in CARLA, illustrate the promise of the proposed approach in synthesizing robust controllers with deep-learning-based perception. △ Less

Submitted 22 September, 2022; originally announced September 2022.

GAS: Generating Fast and Accurate Surrogate Models for Autonomous Vehicle Systems

Authors: Keyur Joshi, Chiao Hsieh, Sayan Mitra, Sasa Misailovic

Abstract: Modern autonomous vehicle systems use complex perception and control components. These components can rapidly change during development of such systems, requiring constant re-testing. Unfortunately, high-fidelity simulations of these complex systems for evaluating vehicle safety are costly. The complexity also hinders the creation of less computationally intensive surrogate models. We present GA… ▽ More Modern autonomous vehicle systems use complex perception and control components. These components can rapidly change during development of such systems, requiring constant re-testing. Unfortunately, high-fidelity simulations of these complex systems for evaluating vehicle safety are costly. The complexity also hinders the creation of less computationally intensive surrogate models. We present GAS, the first approach for creating surrogate models of complete (perception, control, and dynamics) autonomous vehicle systems containing complex perception and/or control components. GAS's two-stage approach first replaces complex perception components with a perception model. Then, GAS constructs a polynomial surrogate model of the complete vehicle system using Generalized Polynomial Chaos (GPC). We demonstrate the use of these surrogate models in two applications. First, we estimate the probability that the vehicle will enter an unsafe state over time. Second, we perform global sensitivity analysis of the vehicle system with respect to its state in a previous time step. GAS's approach also allows for reuse of the perception model when vehicle control and dynamics characteristics are altered during vehicle development, saving significant time. We consider five scenarios concerning crop management vehicles that must not crash into adjacent crops, self driving cars that must stay within their lane, and unmanned aircraft that must avoid collision. Each of the systems in these scenarios contain a complex perception or control component. Using GAS, we generate surrogate models for these systems, and evaluate the generated models in the applications described above. GAS's surrogate models provide an average speedup of $3.7\times$ for safe state probability estimation (minimum $2.1\times$) and $1.4\times$ for sensitivity analysis (minimum $1.3\times$), while still maintaining high accuracy. △ Less

Submitted 13 July, 2023; v1 submitted 3 August, 2022; originally announced August 2022.

Multiview Contrastive Learning for Completely Blind Video Quality Assessment of User Generated Content

Authors: Shankhanil Mitra, Rajiv Soundararajan

Abstract: Completely blind video quality assessment (VQA) refers to a class of quality assessment methods that do not use any reference videos, human opinion scores or training videos from the target database to learn a quality model. The design of this class of methods is particularly important since it can allow for superior generalization in performance across various datasets. We consider the design of… ▽ More Completely blind video quality assessment (VQA) refers to a class of quality assessment methods that do not use any reference videos, human opinion scores or training videos from the target database to learn a quality model. The design of this class of methods is particularly important since it can allow for superior generalization in performance across various datasets. We consider the design of completely blind VQA for user generated content. While several deep feature extraction methods have been considered in supervised and weakly supervised settings, such approaches have not been studied in the context of completely blind VQA. We bridge this gap by presenting a self-supervised multiview contrastive learning framework to learn spatio-temporal quality representations. In particular, we capture the common information between frame differences and frames by treating them as a pair of views and similarly obtain the shared representations between frame differences and optical flow. The resulting features are then compared with a corpus of pristine natural video patches to predict the quality of the distorted video. Detailed experiments on multiple camera captured VQA datasets reveal the superior performance of our method over other features when evaluated without training on human scores. △ Less

Submitted 23 June, 2024; v1 submitted 13 July, 2022; originally announced July 2022.

Unified Modeling of Multi-Domain Multi-Device ASR Systems

Authors: Soumyajit Mitra, Swayambhu Nath Ray, Bharat Padi, Arunasish Sen, Raghavendra Bilgi, Harish Arsikere, Shalini Ghosh, Ajay Srinivasamurthy, Sri Garimella

Abstract: Modern Automatic Speech Recognition (ASR) systems often use a portfolio of domain-specific models in order to get high accuracy for distinct user utterance types across different devices. In this paper, we propose an innovative approach that integrates the different per-domain per-device models into a unified model, using a combination of domain embedding, domain experts, mixture of experts and ad… ▽ More Modern Automatic Speech Recognition (ASR) systems often use a portfolio of domain-specific models in order to get high accuracy for distinct user utterance types across different devices. In this paper, we propose an innovative approach that integrates the different per-domain per-device models into a unified model, using a combination of domain embedding, domain experts, mixture of experts and adversarial training. We run careful ablation studies to show the benefit of each of these innovations in contributing to the accuracy of the overall unified model. Experiments show that our proposed unified modeling approach actually outperforms the carefully tuned per-domain models, giving relative gains of up to 10% over a baseline model with negligible increase in the number of parameters. △ Less

Submitted 13 October, 2022; v1 submitted 13 May, 2022; originally announced May 2022.

Comments: We will update the paper completely with our latest experiments and analysis

Functional Parcellation of fMRI data using multistage k-means clustering

Authors: Harshit Parmar, Brian Nutter, Rodney Long, Sameer Antani, Sunanda Mitra

Abstract: Purpose: Functional Magnetic Resonance Imaging (fMRI) data acquired through resting-state studies have been used to obtain information about the spontaneous activations inside the brain. One of the approaches for analysis and interpretation of resting-state fMRI data require spatially and functionally homogenous parcellation of the whole brain based on underlying temporal fluctuations. Clustering… ▽ More Purpose: Functional Magnetic Resonance Imaging (fMRI) data acquired through resting-state studies have been used to obtain information about the spontaneous activations inside the brain. One of the approaches for analysis and interpretation of resting-state fMRI data require spatially and functionally homogenous parcellation of the whole brain based on underlying temporal fluctuations. Clustering is often used to generate functional parcellation. However, major clustering algorithms, when used for fMRI data, have their limitations. Among commonly used parcellation schemes, a tradeoff exists between intra-cluster functional similarity and alignment with anatomical regions. Approach: In this work, we present a clustering algorithm for resting state and task fMRI data which is developed to obtain brain parcellations that show high structural and functional homogeneity. The clustering is performed by multistage binary k-means clustering algorithm designed specifically for the 4D fMRI data. The results from this multistage k-means algorithm show that by modifying and combining different algorithms, we can take advantage of the strengths of different techniques while overcoming their limitations. Results: The clustering output for resting state fMRI data using the multistage k-means approach is shown to be better than simple k-means or functional atlas in terms of spatial and functional homogeneity. The clusters also correspond to commonly identifiable brain networks. For task fMRI, the clustering output can identify primary and secondary activation regions and provide information about the varying hemodynamic response across different brain regions. Conclusion: The multistage k-means approach can provide functional parcellations of the brain using resting state fMRI data. The method is model-free and is data driven which can be applied to both resting state and task fMRI. △ Less

Submitted 19 February, 2022; originally announced February 2022.

Multi-agent Motion Planning from Signal Temporal Logic Specifications

Authors: Dawei Sun, **gkai Chen, Sayan Mitra, Chuchu Fan

Abstract: We tackle the challenging problem of multi-agent cooperative motion planning for complex tasks described using signal temporal logic (STL), where robots can have nonlinear and nonholonomic dynamics. Existing methods in multi-agent motion planning, especially those based on discrete abstractions and model predictive control (MPC), suffer from limited scalability with respect to the complexity of th… ▽ More We tackle the challenging problem of multi-agent cooperative motion planning for complex tasks described using signal temporal logic (STL), where robots can have nonlinear and nonholonomic dynamics. Existing methods in multi-agent motion planning, especially those based on discrete abstractions and model predictive control (MPC), suffer from limited scalability with respect to the complexity of the task, the size of the workspace, and the planning horizon. We present a method based on {\em timed waypoints\/} to address this issue. We show that timed waypoints can help abstract nonlinear behaviors of the system as safety envelopes around the reference path defined by those waypoints. Then the search for waypoints satisfying the STL specifications can be inductively encoded as a mixed-integer linear program. The agents following the synthesized timed waypoints have their tasks automatically allocated, and are guaranteed to satisfy the STL specifications while avoiding collisions. We evaluate the algorithm on a wide variety of benchmarks. Results show that it supports multi-agent planning from complex specification over long planning horizons, and significantly outperforms state-of-the-art abstraction-based and MPC-based motion planning methods. The implementation is available at https://github.com/sundw2014/STLPlanning. △ Less

Submitted 13 January, 2022; originally announced January 2022.

Comments: Accepted to IEEE Robotics and Automation Letters (RA-L)

Analysis of MRI Biomarkers for Brain Cancer Survival Prediction

Authors: Subhashis Banerjee, Sushmita Mitra, Lawrence O. Hall

Abstract: Prediction of Overall Survival (OS) of brain cancer patients from multi-modal MRI is a challenging field of research. Most of the existing literature on survival prediction is based on Radiomic features, which does not consider either non-biological factors or the functional neurological status of the patient(s). Besides, the selection of an appropriate cut-off for survival and the presence of cen… ▽ More Prediction of Overall Survival (OS) of brain cancer patients from multi-modal MRI is a challenging field of research. Most of the existing literature on survival prediction is based on Radiomic features, which does not consider either non-biological factors or the functional neurological status of the patient(s). Besides, the selection of an appropriate cut-off for survival and the presence of censored data create further problems. Application of deep learning models for OS prediction is also limited due to the lack of large annotated publicly available datasets. In this scenario we analyse the potential of two novel neuroimaging feature families, extracted from brain parcellation atlases and spatial habitats, along with classical radiomic and geometric features; to study their combined predictive power for analysing overall survival. A cross validation strategy with grid search is proposed to simultaneously select and evaluate the most predictive feature subset based on its predictive power. A Cox Proportional Hazard (CoxPH) model is employed for univariate feature selection, followed by the prediction of patient-specific survival functions by three multivariate parsimonious models viz. Coxnet, Random survival forests (RSF) and Survival SVM (SSVM). The brain cancer MRI data used for this research was taken from two open-access collections TCGA-GBM and TCGA-LGG available from The Cancer Imaging Archive (TCIA). Corresponding survival data for each patient was downloaded from The Cancer Genome Atlas (TCGA). A high cross validation $C-index$ score of $0.82\pm.10$ was achieved using RSF with the best $24$ selected features. Age was found to be the most important biological predictor. There were $9$, $6$, $6$ and $2$ features selected from the parcellation, habitat, radiomic and region-based feature groups respectively. △ Less

Submitted 3 September, 2021; originally announced September 2021.

Improving RNN-T ASR Performance with Date-Time and Location Awareness

Authors: Swayambhu Nath Ray, Soumyajit Mitra, Raghavendra Bilgi, Sri Garimella

Abstract: In this paper, we explore the benefits of incorporating context into a Recurrent Neural Network (RNN-T) based Automatic Speech Recognition (ASR) model to improve the speech recognition for virtual assistants. Specifically, we use meta information extracted from the time at which the utterance is spoken and the approximate location information to make ASR context aware. We show that these contextua… ▽ More In this paper, we explore the benefits of incorporating context into a Recurrent Neural Network (RNN-T) based Automatic Speech Recognition (ASR) model to improve the speech recognition for virtual assistants. Specifically, we use meta information extracted from the time at which the utterance is spoken and the approximate location information to make ASR context aware. We show that these contextual information, when used individually, improves overall performance by as much as 3.48% relative to the baseline and when the contexts are combined, the model learns complementary features and the recognition improves by 4.62%. On specific domains, these contextual signals show improvements as high as 11.5%, without any significant degradation on others. We ran experiments with models trained on data of sizes 30K hours and 10K hours. We show that the scale of improvement with the 10K hours dataset is much higher than the one obtained with 30K hours dataset. Our results indicate that with limited data to train the ASR model, contextual signals can improve the performance significantly. △ Less

Submitted 16 June, 2021; v1 submitted 11 June, 2021; originally announced June 2021.

Comments: To appear in TSD 2021

An FPGA Implementation of Convolutional Spiking Neural Networks for Radioisotope Identification

Authors: Xiaoyu Huang, Edward Jones, Siru Zhang, Shouyu Xie, Steve Furber, Yannis Goulermas, Edward Marsden, Ian Baistow, Srinjoy Mitra, Alister Hamilton

Abstract: This paper details the FPGA implementation methodology for Convolutional Spiking Neural Networks (CSNN) and applies this methodology to low-power radioisotope identification using high-resolution data. Power consumption of 75 mW has been achieved on an FPGA implementation of a CSNN, with an inference accuracy of 90.62% on a synthetic dataset. The chip validation method is presented. Prototy** wa… ▽ More This paper details the FPGA implementation methodology for Convolutional Spiking Neural Networks (CSNN) and applies this methodology to low-power radioisotope identification using high-resolution data. Power consumption of 75 mW has been achieved on an FPGA implementation of a CSNN, with an inference accuracy of 90.62% on a synthetic dataset. The chip validation method is presented. Prototy** was accelerated by evaluating SNN parameters using SpiNNaker neuromorphic platform. △ Less

Submitted 24 February, 2021; originally announced February 2021.

Comments: 5 pages, 10 FIGURES, IEEE ISCAS 2021

Combining Hybrid Input-Output Automaton and Game Theory for Security Modeling of Cyber-Physical Systems

Authors: Mustafa Abdallah, Sayan Mitra, Shreyas Sundaram, Saurabh Bagchi

Abstract: We consider a security setting in which the Cyber-Physical System (CPS) is composed of subnetworks where each subnetwork is under ownership of one defender. Such CPS can be represented by an attack graph where the defenders are required to invest (subject to a budget constraint) on the graph's edges in order to protect their critical assets (where each defender's critical asset has a certain value… ▽ More We consider a security setting in which the Cyber-Physical System (CPS) is composed of subnetworks where each subnetwork is under ownership of one defender. Such CPS can be represented by an attack graph where the defenders are required to invest (subject to a budget constraint) on the graph's edges in order to protect their critical assets (where each defender's critical asset has a certain value to the defender if compromised). We model such CPS using Hybrid Input-Output Automaton (HIOA) where each subnetwork is represented by a HIOA module. We first establish the building blocks needed in our setting. We then present our model that characterizes the continuous time evolution of the investments and discrete transitions between different states (where each state represents different condition and/or perturbation) within the system. Finally, we provide a real-world CPS example to validate our modeling. △ Less

Submitted 22 December, 2020; v1 submitted 1 December, 2020; originally announced December 2020.

SceneChecker: Boosting Scenario Verification using Symmetry Abstractions

Authors: Hussein Sibai, Yangge Li, Sayan Mitra

Abstract: We presentSceneChecker, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. SceneChecker converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. SceneChecker uses symmetry abstractions, a novel refinement algor… ▽ More We presentSceneChecker, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. SceneChecker converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. SceneChecker uses symmetry abstractions, a novel refinement algorithm, and importantly, is built to boost the performance of any existing reachability analysis tool as a plug-in subroutine. We evaluated SceneChecker on several scenarios involving ground and aerial vehicles with nonlinear dynamics and neural network controllers, employing different kinds of symmetries, using different reachability subroutines, and following plans with hundreds of way-points in complex workspaces. Compared to two leading tools, DryVR and Flow*, SceneChecker shows 20x speedup in verification time, even while using those very tools as reachability subroutines. △ Less

Submitted 2 March, 2021; v1 submitted 20 November, 2020; originally announced November 2020.

State Estimation of Continuous-time Dynamical Systems with Uncertain Inputs with Bounded Variation: Entropy, Bit Rates, and Relation with Switched Systems

Authors: Hussein Sibai, Sayan Mitra

Abstract: We extend the notion of estimation entropy of autonomous dynamical systems proposed by Liberzon and Mitra [1] to nonlinear dynamical systems with uncertain inputs with bounded variation. We call this new notion the {$ε$}-estimation entropy of the system and show that it lower bounds the bit rate needed for state estimation. {$ε$}-estimation entropy represents the exponential rate of the increase o… ▽ More We extend the notion of estimation entropy of autonomous dynamical systems proposed by Liberzon and Mitra [1] to nonlinear dynamical systems with uncertain inputs with bounded variation. We call this new notion the {$ε$}-estimation entropy of the system and show that it lower bounds the bit rate needed for state estimation. {$ε$}-estimation entropy represents the exponential rate of the increase of the minimal number of functions that are adequate for {$ε$}- approximating any trajectory of the system. We show that alternative entropy definitions using spanning or separating trajectories bound ours from both sides. On the other hand, we show that other commonly used definitions of entropy, for example the ones in [1], diverge to infinity. Thus, they are potentially not suitable for systems with uncertain inputs. We derive an upper bound on {$ε$}-estimation entropy and estimation bit rates, and evaluate it for two examples. We present a state estimation algorithm that constructs a function that approximates a given trajectory up to an {$ε$} error, given time-sampled and quantized measurements of state and input. We investigate the relation between {$ε$}-estimation entropy and a previous notion for switched nonlinear systems and derive a new upper bound for the latter, showing the generality of our results on systems with uncertain inputs. △ Less

Submitted 13 November, 2023; v1 submitted 20 November, 2020; originally announced November 2020.

Computational Challenges in Non-parametric Prediction of Bradycardia in Preterm Infants

Authors: Sin**i Mitra

Abstract: Infants born before 37 weeks of pregnancy are considered to be preterm. Typically, preterm infants have to be strictly monitored since they are highly susceptible to health problems like hypoxemia (low blood oxygen level), apnea, respiratory issues, cardiac problems, neurological problems as well as an increased chance of long-term health issues such as cerebral palsy, asthma and sudden infant dea… ▽ More Infants born before 37 weeks of pregnancy are considered to be preterm. Typically, preterm infants have to be strictly monitored since they are highly susceptible to health problems like hypoxemia (low blood oxygen level), apnea, respiratory issues, cardiac problems, neurological problems as well as an increased chance of long-term health issues such as cerebral palsy, asthma and sudden infant death syndrome. One of the leading health complications in preterm infants is bradycardia - which is defined as the slower than expected heart rate, generally beating lower than 60 beats per minute. Bradycardia is often accompanied by low oxygen levels and can cause additional long term health problems in the premature infant. The implementation of a non-parametric method to predict the onset of bradycardia is presented. This method assumes no prior knowledge of the data and uses kernel density estimation to predict the future onset of bradycardia events. The data is preprocessed, and then analyzed to detect the peaks in the ECG signals, following which different kernels are implemented to estimate the shared underlying distribution of the data. The performance of the algorithm is evaluated using various metrics and the computational challenges and methods to overcome them are also discussed. It is observed that the performance of the algorithm with regards to the kernels used are consistent with the theoretical performance of the kernel as presented in a previous work. The theoretical approach has also been automated in this work and the various implementation challenges have been addressed. △ Less

Submitted 16 November, 2020; originally announced November 2020.

Spiking Neural Network Based Low-Power Radioisotope Identification using FPGA

Authors: Xiaoyu Huang, Edward Jones, Siru Zhang, Shouyu Xie, Steve Furber, Yannis Goulermas, Edward Marsden, Ian Baistow, Srinjoy Mitra, Alister Hamilton

Abstract: this paper presents a detailed methodology of a Spiking Neural Network (SNN) based low-power design for radioisotope identification. A low power cost of 72 mW has been achieved on FPGA with the inference accuracy of 100% at 10 cm test distance and 97% at 25 cm. The design verification and chip validation methods are presented. It also discusses SNN simulation on SpiNNaker for rapid prototy** and… ▽ More this paper presents a detailed methodology of a Spiking Neural Network (SNN) based low-power design for radioisotope identification. A low power cost of 72 mW has been achieved on FPGA with the inference accuracy of 100% at 10 cm test distance and 97% at 25 cm. The design verification and chip validation methods are presented. It also discusses SNN simulation on SpiNNaker for rapid prototy** and various considerations specific to the application such as test distance, integration time, and SNN hyperparameter selections. △ Less

Submitted 25 October, 2020; originally announced October 2020.

Comments: 4 pages, 10 figures, 27th IEEE International Conference on Electronics Circuits and Systems (ICECS) 2020

Event-based Signal Processing for Radioisotope Identification

Authors: Xiaoyu Huang, Edward Jones, Siru Zhang, Steve Furber, Yannis Goulermas, Edward Marsden, Ian Baistow, Srinjoy Mitra, Alister Hamilton

Abstract: This paper identifies the problem of unnecessary high power overhead of the conventional frame-based radioisotope identification process and proposes an event-based signal processing process to address the problem established. It also presents the design flow of the neuromorphic processor. This paper identifies the problem of unnecessary high power overhead of the conventional frame-based radioisotope identification process and proposes an event-based signal processing process to address the problem established. It also presents the design flow of the neuromorphic processor. △ Less

Submitted 2 October, 2020; v1 submitted 11 July, 2020; originally announced July 2020.

Comments: 4 pages, 7 figures, sixth international conference of Event-Based Control, Communication and Signal Processing

Symmetry Abstractions for Hybrid Systems and their Applications

Authors: Hussein Sibai, Sayan Mitra

Abstract: A symmetry of a dynamical system is a map that transforms one trajectory to another trajectory. We introduce a new type of abstraction for hybrid automata based on symmetries. The abstraction combines different modes in a concrete automaton A, whose trajectories are related by symmetries, into a single mode in the abstract automaton B. The abstraction sets the guard and reset of an abstract edge t… ▽ More A symmetry of a dynamical system is a map that transforms one trajectory to another trajectory. We introduce a new type of abstraction for hybrid automata based on symmetries. The abstraction combines different modes in a concrete automaton A, whose trajectories are related by symmetries, into a single mode in the abstract automaton B. The abstraction sets the guard and reset of an abstract edge to be the union of the symmetry-transformed guards and resets of the concrete edges. We establish the soundness of the abstraction using a forward simulation relation (FSR) and present several examples. Our abstraction results in simpler automata, that are more amenable for formal analysis and design. We illustrate an application of this abstraction in making reachability analysis faster and enabling unbounded time safety verification. We show how a fixed point of the reachable set computation of B can be used to answer reachability queries for A, even if the latter visits an infinite and unbounded sequences of modes. We present our implementation of the abstraction construction, the fixed point check, and the map that transforms abstract reachable sets to concrete ones in a software tool. Finally, we show the advantage of our method over existing ones, and the different aspects of our abstraction, in a sequence of experiments including scenarios with linear and nonlinear agents following waypoints. △ Less

Submitted 16 June, 2020; originally announced June 2020.

Deep Learning for Screening COVID-19 using Chest X-Ray Images

Authors: Sanhita Basu, Sushmita Mitra, Nilanjan Saha

Abstract: With the ever increasing demand for screening millions of prospective "novel coronavirus" or COVID-19 cases, and due to the emergence of high false negatives in the commonly used PCR tests, the necessity for probing an alternative simple screening mechanism of COVID-19 using radiological images (like chest X-Rays) assumes importance. In this scenario, machine learning (ML) and deep learning (DL) o… ▽ More With the ever increasing demand for screening millions of prospective "novel coronavirus" or COVID-19 cases, and due to the emergence of high false negatives in the commonly used PCR tests, the necessity for probing an alternative simple screening mechanism of COVID-19 using radiological images (like chest X-Rays) assumes importance. In this scenario, machine learning (ML) and deep learning (DL) offer fast, automated, effective strategies to detect abnormalities and extract key features of the altered lung parenchyma, which may be related to specific signatures of the COVID-19 virus. However, the available COVID-19 datasets are inadequate to train deep neural networks. Therefore, we propose a new concept called domain extension transfer learning (DETL). We employ DETL, with pre-trained deep convolutional neural network, on a related large chest X-Ray dataset that is tuned for classifying between four classes \textit{viz.} $normal$, $pneumonia$, $other\_disease$, and $Covid-19$. A 5-fold cross validation is performed to estimate the feasibility of using chest X-Rays to diagnose COVID-19. The initial results show promise, with the possibility of replication on bigger and more diverse data sets. The overall accuracy was measured as $90.13\% \pm 0.14$. In order to get an idea about the COVID-19 detection transparency, we employed the concept of Gradient Class Activation Map (Grad-CAM) for detecting the regions where the model paid more attention during the classification. This was found to strongly correlate with clinical findings, as validated by experts. △ Less

Submitted 21 August, 2020; v1 submitted 22 April, 2020; originally announced April 2020.

Cytology Image Analysis Techniques Towards Automation: Systematically Revisited

Authors: Shyamali Mitra, Nibaran Das, Soumyajyoti Dey, Sukanta Chakrabarty, Mita Nasipuri, Mrinal Kanti Naskar

Abstract: Cytology is the branch of pathology which deals with the microscopic examination of cells for diagnosis of carcinoma or inflammatory conditions. Automation in cytology started in the early 1950s with the aim to reduce manual efforts in diagnosis of cancer. The inflush of intelligent technological units with high computational power and improved specimen collection techniques helped to achieve its… ▽ More Cytology is the branch of pathology which deals with the microscopic examination of cells for diagnosis of carcinoma or inflammatory conditions. Automation in cytology started in the early 1950s with the aim to reduce manual efforts in diagnosis of cancer. The inflush of intelligent technological units with high computational power and improved specimen collection techniques helped to achieve its technological heights. In the present survey, we focus on such image processing techniques which put steps forward towards the automation of cytology. We take a short tour to 17 types of cytology and explore various segmentation and/or classification techniques which evolved during last three decades boosting the concept of automation in cytology. It is observed, that most of the works are aligned towards three types of cytology: Cervical, Breast and Lung, which are discussed elaborately in this paper. The user-end systems developed during that period are summarized to comprehend the overall growth in the respective domains. To be precise, we discuss the diversity of the state-of-the-art methodologies, their challenges to provide prolific and competent future research directions inbringing the cytology-based commercial systems into the mainstream. △ Less

Submitted 17 March, 2020; originally announced March 2020.

Multi-Agent Safety Verification using Symmetry Transformations

Authors: Hussein Sibai, Navid Mokhlesi, Chuchu Fan, Sayan Mitra

Abstract: We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map solutions and to other solutions. We show that this property can be used to transform cached reachsets to compute new reachsets, for hybrid and multi-agent models. We develop a notion of virtual system which define symmetry transformations… ▽ More We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map solutions and to other solutions. We show that this property can be used to transform cached reachsets to compute new reachsets, for hybrid and multi-agent models. We develop a notion of virtual system which define symmetry transformations for a broad class of agent models that visit waypoint sequences. Using this notion of virtual system, we present a prototype tool CacheReach that builds a cache of reachtubes for this system, in a way that is agnostic of the representation of the reachsets and the reachability analysis subroutine used. Our experimental evaluation of CacheReach shows up to 66% savings in safety verification computation time on multi-agent systems with 3-dimensional linear and 4-dimensional nonlinear fixed-wing aircraft models following sequences of waypoints. These savings and our theoretical results illustrate the potential benefits of using symmetry-based caching in the safety verification of multi-agent systems. △ Less

Submitted 1 November, 2019; originally announced November 2019.

Online monitoring for safe pedestrian-vehicle interactions

Authors: Peter Du, Zhe Huang, Tianqi Liu, Ke Xu, Qichao Gao, Hussein Sibai, Katherine Driggs-Campbell, Sayan Mitra

Abstract: As autonomous systems begin to operate amongst humans, methods for safe interaction must be investigated. We consider an example of a small autonomous vehicle in a pedestrian zone that must safely maneuver around people in a free-form fashion. We investigate two key questions: How can we effectively integrate pedestrian intent estimation into our autonomous stack. Can we develop an online monitori… ▽ More As autonomous systems begin to operate amongst humans, methods for safe interaction must be investigated. We consider an example of a small autonomous vehicle in a pedestrian zone that must safely maneuver around people in a free-form fashion. We investigate two key questions: How can we effectively integrate pedestrian intent estimation into our autonomous stack. Can we develop an online monitoring framework to give formal guarantees on the safety of such human-robot interactions. We present a pedestrian intent estimation framework that can accurately predict future pedestrian trajectories given multiple possible goal locations. We integrate this into a reachability-based online monitoring scheme that formally assesses the safety of these interactions with nearly real-time performance (approximately 0.3 seconds). These techniques are integrated on a test vehicle with a complete in-house autonomous stack, demonstrating effective and safe interaction in real-world experiments. △ Less

Submitted 17 July, 2020; v1 submitted 12 October, 2019; originally announced October 2019.

Comments: 15 pages, 5 figures,

ApproxNet: Content and Contention-Aware Video Analytics System for Embedded Clients

Authors: Ran Xu, Rakesh Kumar, Pengcheng Wang, Peter Bai, Ganga Meghanath, Somali Chaterji, Subrata Mitra, Saurabh Bagchi

Abstract: Videos take a lot of time to transport over the network, hence running analytics on the live video on embedded or mobile devices has become an important system driver. Considering that such devices, e.g., surveillance cameras or AR/VR gadgets, are resource constrained, creating lightweight deep neural networks (DNNs) for embedded devices is crucial. None of the current approximation techniques for… ▽ More Videos take a lot of time to transport over the network, hence running analytics on the live video on embedded or mobile devices has become an important system driver. Considering that such devices, e.g., surveillance cameras or AR/VR gadgets, are resource constrained, creating lightweight deep neural networks (DNNs) for embedded devices is crucial. None of the current approximation techniques for object classification DNNs can adapt to changing runtime conditions, e.g., changes in resource availability on the device, the content characteristics, or requirements from the user. In this paper, we introduce ApproxNet, a video object classification system for embedded or mobile clients. It enables novel dynamic approximation techniques to achieve desired inference latency and accuracy trade-off under changing runtime conditions. It achieves this by enabling two approximation knobs within a single DNN model, rather than creating and maintaining an ensemble of models (e.g., MCDNN [MobiSys-16]. We show that ApproxNet can adapt seamlessly at runtime to these changes, provides low and stable latency for the image and video frame classification problems, and show the improvement in accuracy and latency over ResNet [CVPR-16], MCDNN [MobiSys-16], MobileNets [Google-17], NestDNN [MobiCom-18], and MSDNet [ICLR-18]. △ Less

Submitted 14 July, 2021; v1 submitted 28 August, 2019; originally announced September 2019.

Comments: This paper has been accepted to appear in ACM Transactions on Sensor Networks in 2021

Deep Radiomics for Brain Tumor Detection and Classification from Multi-Sequence MRI

Authors: Subhashis Banerjee, Sushmita Mitra, Francesco Masulli, Stefano Rovetta

Abstract: Glioma constitutes 80% of malignant primary brain tumors and is usually classified as HGG and LGG. The LGG tumors are less aggressive, with slower growth rate as compared to HGG, and are responsive to therapy. Tumor biopsy being challenging for brain tumor patients, noninvasive imaging techniques like Magnetic Resonance Imaging (MRI) have been extensively employed in diagnosing brain tumors. There… ▽ More Glioma constitutes 80% of malignant primary brain tumors and is usually classified as HGG and LGG. The LGG tumors are less aggressive, with slower growth rate as compared to HGG, and are responsive to therapy. Tumor biopsy being challenging for brain tumor patients, noninvasive imaging techniques like Magnetic Resonance Imaging (MRI) have been extensively employed in diagnosing brain tumors. Therefore automated systems for the detection and prediction of the grade of tumors based on MRI data becomes necessary for assisting doctors in the framework of augmented intelligence. In this paper, we thoroughly investigate the power of Deep ConvNets for classification of brain tumors using multi-sequence MR images. We propose novel ConvNet models, which are trained from scratch, on MRI patches, slices, and multi-planar volumetric slices. The suitability of transfer learning for the task is next studied by applying two existing ConvNets models (VGGNet and ResNet) trained on ImageNet dataset, through fine-tuning of the last few layers. LOPO testing, and testing on the holdout dataset are used to evaluate the performance of the ConvNets. Results demonstrate that the proposed ConvNets achieve better accuracy in all cases where the model is trained on the multi-planar volumetric dataset. Unlike conventional models, it obtains a testing accuracy of 95% for the low/high grade glioma classification problem. A score of 97% is generated for classification of LGG with/without 1p/19q codeletion, without any additional effort towards extraction and selection of features. We study the properties of self-learned kernels/ filters in different layers, through visualization of the intermediate layer outputs. We also compare the results with that of state-of-the-art methods, demonstrating a maximum improvement of 7% on the grading performance of ConvNets and 9% on the prediction of 1p/19q codeletion status. △ Less

Submitted 21 March, 2019; originally announced March 2019.

CODEV: Automated Model Predictive Control Design and Formal Verification (Tool Paper)

Authors: Nicole Chan, Sayan Mitra

Abstract: We present CODEV, a Matlab-based tool for verifying systems employing Model Predictive Control (MPC). The MPC solution is computed offline and modeled together with the physical system as a hybrid automaton, whose continuous dynamics may be nonlinear with a control solution that remains affine. While MPC is a widely used synthesis technique for constrained and optimal control in industry, our tool… ▽ More We present CODEV, a Matlab-based tool for verifying systems employing Model Predictive Control (MPC). The MPC solution is computed offline and modeled together with the physical system as a hybrid automaton, whose continuous dynamics may be nonlinear with a control solution that remains affine. While MPC is a widely used synthesis technique for constrained and optimal control in industry, our tool provides the first automated approach of analyzing these systems for rigorous guarantees of safety. This is achieved by implementing a simulation-based verification algorithm for nonlinear hybrid models, with extensions tailored to the structure of the MPC solution. Given a physical model and parameters for desired system behavior (i.e. performance and constraints), CODEV generates a control law and verifies the resulting system will robustly maintain constraints. We have applied CODEV successfully to a set of benchmark examples, which illuminates its potential to tackle more complex problems for which MPC is used. △ Less

Submitted 7 April, 2018; originally announced April 2018.

Verifying nonlinear analog and mixed-signal circuits with inputs

Authors: Chuchu Fan, Yu Meng, Jürgen Maier, Ezio Bartocci, Sayan Mitra, Ulrich Schmid

Abstract: We present a new technique for verifying nonlinear and hybrid models with inputs. We observe that once an input signal is fixed, the sensitivity analysis of the model can be computed much more precisely. Based on this result, we propose a new simulation-driven verification algorithm and apply it to a suite of nonlinear and hybrid models of CMOS digital circuits under different input signals. The m… ▽ More We present a new technique for verifying nonlinear and hybrid models with inputs. We observe that once an input signal is fixed, the sensitivity analysis of the model can be computed much more precisely. Based on this result, we propose a new simulation-driven verification algorithm and apply it to a suite of nonlinear and hybrid models of CMOS digital circuits under different input signals. The models are low-dimensional but with highly nonlinear ODEs, with nearly hundreds of logarithmic and exponential terms. Some of our experiments analyze the metastability of bistable circuits with very sensitive ODEs and rigorously establish the connection between metastability recovery time and sensitivity. △ Less

Submitted 8 March, 2018; originally announced March 2018.

Comments: 8 pages, 8 figures, a shorter version will appear on the IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2018)

Road to safe autonomy with data and formal reasoning

Authors: Chuchu Fan, Bolun Qi, Sayan Mitra

Abstract: We present an overview of recently developed data-driven tools for safety analysis of autonomous vehicles and advanced driver assist systems. The core algorithms combine model-based, hybrid system reachability analysis with sensitivity analysis of components with unknown or inaccessible models. We illustrate the applicability of this approach with a new case study of emergency braking systems in s… ▽ More We present an overview of recently developed data-driven tools for safety analysis of autonomous vehicles and advanced driver assist systems. The core algorithms combine model-based, hybrid system reachability analysis with sensitivity analysis of components with unknown or inaccessible models. We illustrate the applicability of this approach with a new case study of emergency braking systems in scenarios with two or three vehicles. This problem is representative of the most common type of rear-end crashes, which is relevant for safety analysis of automatic emergency braking (AEB) and forward collision avoidance systems. We show that our verification tool can effectively prove the safety of certain scenarios (specified by several parameters like braking profiles, initial velocities, uncertainties in position and reaction times), and also compute the severity of accidents for unsafe scenarios. Through hundreds of verification experiments, we quantified the safety envelope of the system across relevant parameters. These results show that the approach is promising for design, debugging and certification. We also show how the reachability analysis can be combined with statistical information about the parameters, to assess the risk level of the control system, which in turn is essential, for example, for determining Automotive Safety Integrity Levels (ASIL) for the ISO26262 standard. △ Less

Submitted 21 April, 2017; originally announced April 2017.

Comments: 7 pages, 5 figures, under submission to IEEE Design & Test

Verifying safety of an autonomous spacecraft rendezvous mission

Authors: Nicole Chan, Sayan Mitra

Abstract: A fundamental maneuver in autonomous space operations is known as rendezvous, where a spacecraft navigates to and approaches another spacecraft. In this case study, we present linear and nonlinear benchmark models of an active chaser spacecraft performing rendezvous toward a passive, orbiting target. The system is modeled as a hybrid automaton, where the chaser must adhere to different sets of con… ▽ More A fundamental maneuver in autonomous space operations is known as rendezvous, where a spacecraft navigates to and approaches another spacecraft. In this case study, we present linear and nonlinear benchmark models of an active chaser spacecraft performing rendezvous toward a passive, orbiting target. The system is modeled as a hybrid automaton, where the chaser must adhere to different sets of constraints in each discrete mode. A switched LQR controller is designed accordingly to meet this collection of physical and geometric safety constraints, while maintaining liveness in navigating toward the target spacecraft. We extend this benchmark problem to check for passive safety, which is collision avoidance along a passive, propulsion-free trajectory that may be followed in the event of system failures. We show that existing hybrid verification tools like SpaceEx, C2E2, and our own implementation of a simulation-driven verification tool can robustly verify this system with respect to the requirements, and a variety of relevant initial conditions. △ Less

Submitted 20 March, 2017; originally announced March 2017.

DRYVR:Data-driven verification and compositional reasoning for automotive systems

Authors: Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan

Abstract: We present the DRYVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the lear… ▽ More We present the DRYVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the learned sensitivity, and (c) reasoning techniques based on simulation relations and sequential composition, that enable verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under shorter sequences. We demonstrate the utility of the framework by verifying a suite of automotive benchmarks that include powertrain control, automatic transmission, and several autonomous and ADAS features like automatic emergency braking, lane-merge, and auto-passing controllers. △ Less

Submitted 22 February, 2017; originally announced February 2017.

Comments: 25 pages, 3 figures

Controller Synthesis with Inductive Proofs for Piecewise Linear Systems: an SMT-based Algorithm

Authors: Zhenqi Huang, Yu Wang, Sayan Mitra, Geir E. Dullerud, Swarat Chaudhuri

Abstract: We present a controller synthesis algorithm for reach-avoid problems for piecewise linear discrete-time systems. Our algorithm relies on SMT solvers and in this paper we focus on piecewise constant control strategies. Our algorithm generates feedback control laws together with inductive proofs of unbounded time safety and progress properties with respect to the reach-avoid sets. Under a reasonable… ▽ More We present a controller synthesis algorithm for reach-avoid problems for piecewise linear discrete-time systems. Our algorithm relies on SMT solvers and in this paper we focus on piecewise constant control strategies. Our algorithm generates feedback control laws together with inductive proofs of unbounded time safety and progress properties with respect to the reach-avoid sets. Under a reasonable robustness assump- tion, the algorithm is shown to be complete. That is, it either generates a controller of the above type along with a proof of correctness, or it establishes the impossibility of the existence of such controllers. To achieve this, the algorithm iteratively attempts to solve a weakened and strengthened versions of the SMT encoding of the reach-avoid problem. We present preliminary experimental results on applying this algorithm based on a prototype implementation. △ Less

Submitted 15 September, 2015; originally announced September 2015.

Model Checking Tap Withdrawal in C. Elegans

Authors: Md. Ariful Islam, Richard DeFrancisco, Chuchu Fan, Radu Grosu, Sayan Mitra, Scott A. Smolka

Abstract: We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in \emph{C. Elegans}, the common roundworm. TW is a reflexive behavior exhibited by \emph{C. Elegans} in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subje… ▽ More We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in \emph{C. Elegans}, the common roundworm. TW is a reflexive behavior exhibited by \emph{C. Elegans} in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subject of this investigation. Specifically, we perform reachability analysis on the TW circuit model of Wicks et al. (1996), which enables us to estimate key circuit parameters. Underlying our approach is the use of Fan and Mitra's recently developed technique for automatically computing local discrepancy (convergence and divergence rates) of general nonlinear systems. We show that the results we obtain are in agreement with the experimental results of Wicks et al. (1995). As opposed to the fixed parameters found in most biological models, which can only produce the predominant behavior, our techniques characterize ranges of parameters that produce (and do not produce) all three observed behaviors: reversal of movement, acceleration, and lack of response. △ Less

Submitted 22 March, 2015; originally announced March 2015.

Bounded Verification with On-the-Fly Discrepancy Computation

Authors: Chuchu Fan, Sayan Mitra

Abstract: Simulation-based verification algorithms can provide formal safety guarantees for nonlinear and hybrid systems. The previous algorithms rely on user provided model annotations called discrepancy function, which are crucial for computing reachtubes from simulations. In this paper, we eliminate this requirement by presenting an algorithm for computing piece-wise exponential discrepancy functions. Th… ▽ More Simulation-based verification algorithms can provide formal safety guarantees for nonlinear and hybrid systems. The previous algorithms rely on user provided model annotations called discrepancy function, which are crucial for computing reachtubes from simulations. In this paper, we eliminate this requirement by presenting an algorithm for computing piece-wise exponential discrepancy functions. The algorithm relies on computing local convergence or divergence rates of trajectories along a simulation using a coarse over-approximation of the reach set and bounding the maximal eigenvalue of the Jacobian over this over-approximation. The resulting discrepancy function preserves the soundness and the relative completeness of the verification algorithm. We also provide a coordinate transformation method to improve the local estimates for the convergence or divergence rates in practical examples. We extend the method to get the input-to-state discrepancy of nonlinear dynamical systems which can be used for compositional analysis. Our experiments show that the approach is effective in terms of running time for several benchmark problems, scales reasonably to larger dimensional systems, and compares favorably with respect to available tools for nonlinear models. △ Less

Submitted 6 February, 2015; originally announced February 2015.

Comments: 24 pages

Report number: University of Illinois Urbana Champaign, Tech Report UILU-ENG-15-2201

Controller Synthesis for Linear Time-varying Systems with Adversaries

Authors: Zhenqi Huang, Yu Wang, Sayan Mitra, Geir Dullerud

Abstract: We present a controller synthesis algorithm for a discrete time reach-avoid problem in the presence of adversaries. Our model of the adversary captures typical malicious attacks envisioned on cyber-physical systems such as sensor spoofing, controller corruption, and actuator intrusion. After formulating the problem in a general setting, we present a sound and complete algorithm for the case with l… ▽ More We present a controller synthesis algorithm for a discrete time reach-avoid problem in the presence of adversaries. Our model of the adversary captures typical malicious attacks envisioned on cyber-physical systems such as sensor spoofing, controller corruption, and actuator intrusion. After formulating the problem in a general setting, we present a sound and complete algorithm for the case with linear dynamics and an adversary with a budget on the total L2-norm of its actions. The algorithm relies on a result from linear control theory that enables us to decompose and precisely compute the reachable states of the system in terms of a symbolic simulation of the adversary-free dynamics and the total uncertainty induced by the adversary. With this decomposition, the synthesis problem eliminates the universal quantifier on the adversary's choices and the symbolic controller actions can be effectively solved using an SMT solver. The constraints induced by the adversary are computed by solving second-order cone programmings. The algorithm is later extended to synthesize state-dependent controller and to generate attacks for the adversary. We present preliminary experimental results that show the effectiveness of this approach on several example problems. △ Less

Submitted 18 January, 2015; originally announced January 2015.

Comments: 10 pages 4 figures; under submission for review

Proving Abstractions of Dynamical Systems through Numerical Simulations

Authors: Sayan Mitra

Abstract: A key question that arises in rigorous analysis of cyberphysical systems under attack involves establishing whether or not the attacked system deviates significantly from the ideal allowed behavior. This is the problem of deciding whether or not the ideal system is an abstraction of the attacked system. A quantitative variation of this question can capture how much the attacked system deviates fro… ▽ More A key question that arises in rigorous analysis of cyberphysical systems under attack involves establishing whether or not the attacked system deviates significantly from the ideal allowed behavior. This is the problem of deciding whether or not the ideal system is an abstraction of the attacked system. A quantitative variation of this question can capture how much the attacked system deviates from the ideal. Thus, algorithms for deciding abstraction relations can help measure the effect of attacks on cyberphysical systems and to develop attack detection strategies. In this paper, we present a decision procedure for proving that one nonlinear dynamical system is a quantitative abstraction of another. Directly computing the reach sets of these nonlinear systems are undecidable in general and reach set over-approximations do not give a direct way for proving abstraction. Our procedure uses (possibly inaccurate) numerical simulations and a model annotation to compute tight approximations of the observable behaviors of the system and then uses these approximations to decide on abstraction. We show that the procedure is sound and that it is guaranteed to terminate under reasonable robustness assumptions. △ Less

Submitted 7 January, 2014; originally announced January 2014.

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)

Differentially Private Iterative Synchronous Consensus

Authors: Zhenqi Huang, Sayan Mitra, Geir Dullerud

Abstract: The iterative consensus problem requires a set of processes or agents with different initial values, to interact and update their states to eventually converge to a common value. Protocols solving iterative consensus serve as building blocks in a variety of systems where distributed coordination is required for load balancing, data aggregation, sensor fusion, filtering, clock synchronization and p… ▽ More The iterative consensus problem requires a set of processes or agents with different initial values, to interact and update their states to eventually converge to a common value. Protocols solving iterative consensus serve as building blocks in a variety of systems where distributed coordination is required for load balancing, data aggregation, sensor fusion, filtering, clock synchronization and platooning of autonomous vehicles. In this paper, we introduce the private iterative consensus problem where agents are required to converge while protecting the privacy of their initial values from honest but curious adversaries. Protecting the initial states, in many applications, suffice to protect all subsequent states of the individual participants. First, we adapt the notion of differential privacy in this setting of iterative computation. Next, we present a server-based and a completely distributed randomized mechanism for solving private iterative consensus with adversaries who can observe the messages as well as the internal states of the server and a subset of the clients. Finally, we establish the tradeoff between privacy and the accuracy of the proposed randomized mechanism. △ Less

Submitted 8 August, 2012; v1 submitted 18 July, 2012; originally announced July 2012.

Comments: The original manuscript from 18th July was updated with new proofs for Lemmas 3, 6, and 8

Bounded epsilon-Reach Set Computation of a Class of Deterministic and Transversal Linear Hybrid Automata

Authors: Kyoung-Dae Kim, Sayan Mitra, P. R. Kumar

Abstract: We define a special class of hybrid automata, called Deterministic and Transversal Linear Hybrid Automata (DTLHA), whose continuous dynamics in each location are linear time-invariant (LTI) with a constant input, and for which every discrete transition up to a given bounded time is deterministic and, importantly, transversal. For such a DTLHA starting from an initial state, we show that it is poss… ▽ More We define a special class of hybrid automata, called Deterministic and Transversal Linear Hybrid Automata (DTLHA), whose continuous dynamics in each location are linear time-invariant (LTI) with a constant input, and for which every discrete transition up to a given bounded time is deterministic and, importantly, transversal. For such a DTLHA starting from an initial state, we show that it is possible to compute an approximation of the reach set of a DTLHA over a finite time interval that is arbitrarily close to the exact reach set, called a bounded epsilon-reach set, through sampling and polyhedral over-approximation of sampled states. We propose an algorithm and an attendant architecture for the overall bounded epsilon-reach set computation process. △ Less

Submitted 15 May, 2012; originally announced May 2012.

A Simple Flood Forecasting Scheme Using Wireless Sensor Networks

Authors: Victor Seal, Arnab Raha, Shovan Maity, Souvik Kr Mitra, Amitava Mukherjee, Mrinal Kanti Naskar

Abstract: This paper presents a forecasting model designed using WSNs (Wireless Sensor Networks) to predict flood in rivers using simple and fast calculations to provide real-time results and save the lives of people who may be affected by the flood. Our prediction model uses multiple variable robust linear regression which is easy to understand and simple and cost effective in implementation, is speed effi… ▽ More This paper presents a forecasting model designed using WSNs (Wireless Sensor Networks) to predict flood in rivers using simple and fast calculations to provide real-time results and save the lives of people who may be affected by the flood. Our prediction model uses multiple variable robust linear regression which is easy to understand and simple and cost effective in implementation, is speed efficient, but has low resource utilization and yet provides real time predictions with reliable accuracy, thus having features which are desirable in any real world algorithm. Our prediction model is independent of the number of parameters, i.e. any number of parameters may be added or removed based on the on-site requirements. When the water level rises, we represent it using a polynomial whose nature is used to determine if the water level may exceed the flood line in the near future. We compare our work with a contemporary algorithm to demonstrate our improvements over it. Then we present our simulation results for the predicted water level compared to the actual water level. △ Less

Submitted 9 March, 2012; originally announced March 2012.

Comments: 16 pages, 4 figures, published in International Journal Of Ad-Hoc, Sensor And Ubiquitous Computing, February 2012; V. seal et al, 'A Simple Flood Forecasting Scheme Using Wireless Sensor Networks', IJASUC, Feb.2012