Showing 1–50 of 117 results for author: Zamani, M

$k$-Inductive and Interpolation-Inspired Barrier Certificates for Stochastic Dynamical Systems

Authors: Mohammed Adib Oumer, Vishnu Murali, Majid Zamani

Abstract: We introduce two notions of barrier certificates that use multiple functions to provide a lower bound on the probabilistic satisfaction of safety for stochastic dynamical systems. A barrier certificate for a stochastic dynamical system acts as a nonnegative supermartingale, and provides a lower bound on the probability that the system is safe. The promise of such certificates is that their search… ▽ More We introduce two notions of barrier certificates that use multiple functions to provide a lower bound on the probabilistic satisfaction of safety for stochastic dynamical systems. A barrier certificate for a stochastic dynamical system acts as a nonnegative supermartingale, and provides a lower bound on the probability that the system is safe. The promise of such certificates is that their search can be effectively automated. Typically, one may use optimization or SMT solvers to find such barrier certificates of a given fixed template. When such approaches fail, a typical approach is to instead change the template. We propose an alternative approach that we dub interpolation-inspired barrier certificates. An interpolation-inspired barrier certificate consists of a set of functions that jointly provide a lower bound on the probability of satisfying safety. We show how one may find such certificates of a fixed template, even when we fail to find standard barrier certificates of the same template. However, we note that such certificates still need to ensure a supermartingale guarantee for one function in the set. To address this challenge, we consider the use of $k$-induction with these interpolation-inspired certificates. The recent use of $k$-induction in barrier certificates allows one to relax the supermartingale requirement at every time step to a combination of a supermartingale requirement every $k$ steps and a $c$-martingale requirement for the intermediate steps. We provide a generic formulation of a barrier certificate that we dub $k$-inductive interpolation-inspired barrier certificate. The formulation allows for several combinations of interpolation and $k$-induction for barrier certificate. We present two examples among the possible combinations. We finally present sum-of-squares programming to synthesize this set of functions and demonstrate their utility in case studies. △ Less

Submitted 21 April, 2025; originally announced April 2025.

Comments: This manuscript of 20 pages and 4 figures is a preprint under review with a journal

A Real-time and Hardware Efficient Artfecat-free Spike Sorting Using Deep Spike Detection

Authors: Xiaoyu Jiang, Tao Fang, Majid Zamani

Abstract: Spike sorting is a valuable tool in understanding brain regions. It assigns detected spike waveforms to their origins, helping to research the mechanism of the human brain and the development of implantable brain-machine interfaces (iBMIs). The presence of noise and artefacts will adversely affect the efficacy of spike sorting. This paper proposes a framework for low-cost and real-time implementat… ▽ More Spike sorting is a valuable tool in understanding brain regions. It assigns detected spike waveforms to their origins, helping to research the mechanism of the human brain and the development of implantable brain-machine interfaces (iBMIs). The presence of noise and artefacts will adversely affect the efficacy of spike sorting. This paper proposes a framework for low-cost and real-time implementation of deep spike detection, which consists of two one-dimensional (1-D) convolutional neural network (CNN) model for channel selection and artefact removal. The framework utilizes simulation and hardware layers, and it applies several low-power techniques to optimise the implementation cost of a 1-D CNN model. A compact CNN model with 210 bytes memory size is achieved using structured pruning, network projection and quantization in the simulation layer. The hardware layer also accommodates various techniques including a customized multiply-accumulate (MAC) engine, novel fused layers in the convolution pipeline and proposing flexible resource allocation for a power-efficient and low-delay design. The optimized 1-D CNN significantly decreases both computational complexity and model size, with only a minimal reduction in accuracy. Classification of 1-D CNN on the Cyclone V 5CSEMA5F31C6 FPGA evaluation platform is accomplished in just 16.8 microseconds at a frequency of 2.5 MHz. The FPGA prototype achieves an accuracy rate of 97.14% on a standard dataset and operates with a power consumption of 2.67mW from a supply voltage of 1.1 volts. An accuracy of 95.05% is achieved with a power of 5.6mW when deep spike detection is implemented using two optimized 1-D CNNs on an FPGA board. △ Less

Submitted 19 April, 2025; originally announced April 2025.

Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes

Authors: Mohammed Adib Oumer, Amr Alanwar, Majid Zamani

Abstract: Ensuring safety in cyber-physical systems (CPSs) is a critical challenge, especially when system models are difficult to obtain or cannot be fully trusted due to uncertainty, modeling errors, or environmental disturbances. Traditional model-based approaches rely on precise system dynamics, which may not be available in real-world scenarios. To address this, we propose a data-driven safety verifica… ▽ More Ensuring safety in cyber-physical systems (CPSs) is a critical challenge, especially when system models are difficult to obtain or cannot be fully trusted due to uncertainty, modeling errors, or environmental disturbances. Traditional model-based approaches rely on precise system dynamics, which may not be available in real-world scenarios. To address this, we propose a data-driven safety verification framework that leverages matrix zonotopes and barrier certificates to verify system safety directly from noisy data. Instead of trusting a single unreliable model, we construct a set of models that capture all possible system dynamics that align with the observed data, ensuring that the true system model is always contained within this set. This model set is compactly represented using matrix zonotopes, enabling efficient computation and propagation of uncertainty. By integrating this representation into a barrier certificate framework, we establish rigorous safety guarantees without requiring an explicit system model. Numerical experiments demonstrate the effectiveness of our approach in verifying safety for dynamical systems with unknown models, showcasing its potential for real-world CPS applications. △ Less

Submitted 14 April, 2025; v1 submitted 1 April, 2025; originally announced April 2025.

Comments: This manuscript of 11 pages, 2 tables and 3 figures is a preprint under review with a conference

On the Completeness and Ordering of Path-Complete Barrier Functions

Authors: Mahathi Anand, Raphaël Jungers, Majid Zamani, Frank Allgöwer

Abstract: This paper is concerned with path-complete barrier functions which offer a graph-based methodology for verifying safety properties in switched systems. The path-complete framework leverages algebraic (barrier functions) as well as combinatorial (graph) components to characterize a set of safety conditions for switched systems, thus offering high flexibility (two degrees of freedom) in searching fo… ▽ More This paper is concerned with path-complete barrier functions which offer a graph-based methodology for verifying safety properties in switched systems. The path-complete framework leverages algebraic (barrier functions) as well as combinatorial (graph) components to characterize a set of safety conditions for switched systems, thus offering high flexibility (two degrees of freedom) in searching for suitable safety certificates. In this paper, we do not propose any new safety criteria. Instead, we further investigate the role that the combinatorial component plays in the safety verification problem. First, we prove that path-completeness, which is a property on a graph that describes the switching sequences, is necessary to obtain a set of valid safety conditions. As a result, the path-complete framework is able to provide a complete characterization of safety conditions for switched systems. Furthermore, we provide a systematic methodology for comparing two path-complete graphs and the conservatism associated with the resulting safety conditions. Specifically, we prove that under some conditions, such as when there exists a simulation relation between two path-complete graphs, it is possible to conclude that one graph is always able to provide less conservative safety conditions than another, independent of the algebraic properties of the switched system and the template of the barrier function under consideration. Such a result paves the way for a systematic use of the path-complete framework with barrier functions, as one can then consistently choose the appropriate graph that provides less conservative safety conditions. △ Less

Submitted 25 March, 2025; originally announced March 2025.

Comments: 17 pages, 8 figures

FS-SS: Few-Shot Learning for Fast and Accurate Spike Sorting of High-channel Count Probes

Authors: Tao Fang, Majid Zamani

Abstract: There is a need for fast adaptation in spike sorting algorithms to implement brain-machine interface (BMIs) in different applications. Learning and adapting the functionality of the sorting process in real-time can significantly improve the performance. However, deep neural networks (DNNs) depend on large amounts of data for training models and their performance sustainability decreases when data… ▽ More There is a need for fast adaptation in spike sorting algorithms to implement brain-machine interface (BMIs) in different applications. Learning and adapting the functionality of the sorting process in real-time can significantly improve the performance. However, deep neural networks (DNNs) depend on large amounts of data for training models and their performance sustainability decreases when data is limited. Inspired by meta-learning, this paper proposes a few-shot spike sorting framework (FS-SS) with variable network model size that requires minimal learning training and supervision. The framework is not only compatible with few-shot adaptations, but also it uses attention mechanism and dilated convolutional neural networks. This allows scaling the network parameters to learn the important features of spike signals and to quickly generalize the learning ability to new spike waveforms in recording channels after few observations. The FS-SS was evaluated by using freely accessible datasets, also compared with the other state-of-the-art algorithms. The average classification accuracy of the proposed method is 99.28%, which shows extreme robustness to background noise and similarity of the spike waveforms. When the number of training samples is reduced by 90%, the parameter scale is reduced by 68.2%, while the accuracy only decreased by 0.55%. The paper also visualizes the model's attention distribution under spike sorting tasks of different difficulty levels. The attention distribution results show that the proposed model has clear interpretability and high robustness. △ Less

Submitted 23 March, 2025; originally announced March 2025.

Comments: 10 pages

Symbolic Control for Autonomous Docking of Marine Surface Vessels

Authors: Elizabeth Dietrich, Emir Cem Gezer, Bingzhuo Zhong, Murat Arcak, Majid Zamani, Roger Skjetne, Asgeir Johan Sørensen

Abstract: Docking marine surface vessels remains a largely manual task due to its safety-critical nature. In this paper, we develop a hierarchical symbolic control architecture for autonomous docking maneuvers of a dynamic positioning vessel, to provide formal safety guarantees. At the upper-level, we treat the vessel's desired surge, sway, and yaw velocities as control inputs and synthesize a symbolic cont… ▽ More Docking marine surface vessels remains a largely manual task due to its safety-critical nature. In this paper, we develop a hierarchical symbolic control architecture for autonomous docking maneuvers of a dynamic positioning vessel, to provide formal safety guarantees. At the upper-level, we treat the vessel's desired surge, sway, and yaw velocities as control inputs and synthesize a symbolic controller in real-time. The desired velocities are then transmitted to and executed by the vessel's low-level velocity feedback control loop. Given a synthesized symbolic controller, we investigate methods to optimize the performance of the proposed control scheme for the docking task. The efficacy of this methodology is evaluated on a low-fidelity simulation model of a marine surface vessel in the presence of static and dynamic obstacles and, for the first time, through physical experiments on a scaled model vessel. △ Less

Submitted 22 January, 2025; originally announced January 2025.

Tessellated Linear Model for Age Prediction from Voice

Authors: Dareen Alharthi, Mahsa Zamani, Bhiksha Raj, Rita Singh

Abstract: Voice biometric tasks, such as age estimation require modeling the often complex relationship between voice features and the biometric variable. While deep learning models can handle such complexity, they typically require large amounts of accurately labeled data to perform well. Such data are often scarce for biometric tasks such as voice-based age prediction. On the other hand, simpler models li… ▽ More Voice biometric tasks, such as age estimation require modeling the often complex relationship between voice features and the biometric variable. While deep learning models can handle such complexity, they typically require large amounts of accurately labeled data to perform well. Such data are often scarce for biometric tasks such as voice-based age prediction. On the other hand, simpler models like linear regression can work with smaller datasets but often fail to generalize to the underlying non-linear patterns present in the data. In this paper we propose the Tessellated Linear Model (TLM), a piecewise linear approach that combines the simplicity of linear models with the capacity of non-linear functions. TLM tessellates the feature space into convex regions and fits a linear model within each region. We optimize the tessellation and the linear models using a hierarchical greedy partitioning. We evaluated TLM on the TIMIT dataset on the task of age prediction from voice, where it outperformed state-of-the-art deep learning models. △ Less

Submitted 27 January, 2025; v1 submitted 15 January, 2025; originally announced January 2025.

Comments: Accepted at ICASSP 2025

Transfer Learning for Control Systems via Neural Simulation Relations

Authors: Alireza Nadali, Bingzhuo Zhong, Ashutosh Trivedi, Majid Zamani

Abstract: Transfer learning is an umbrella term for machine learning approaches that leverage knowledge gained from solving one problem (the source domain) to improve speed, efficiency, and data requirements in solving a different but related problem (the target domain). The performance of the transferred model in the target domain is typically measured via some notion of loss function in the target domain.… ▽ More Transfer learning is an umbrella term for machine learning approaches that leverage knowledge gained from solving one problem (the source domain) to improve speed, efficiency, and data requirements in solving a different but related problem (the target domain). The performance of the transferred model in the target domain is typically measured via some notion of loss function in the target domain. This paper focuses on effectively transferring control logic from a source control system to a target control system while providing approximately similar behavioral guarantees in both domains. However, in the absence of a complete characterization of behavioral specifications, this problem cannot be captured in terms of loss functions. To overcome this challenge, we use (approximate) simulation relations to characterize observational equivalence between the behaviors of two systems. Simulation relations ensure that the outputs of both systems, equipped with their corresponding controllers, remain close to each other over time, and their closeness can be quantified {\it a priori}. By parameterizing simulation relations with neural networks, we introduce the notion of \emph{neural simulation relations}, which provides a data-driven approach to transfer any synthesized controller, regardless of the specification of interest, along with its proof of correctness. Compared with prior approaches, our method eliminates the need for a closed-loop mathematical model and specific requirements for both the source and target systems. We also introduce validity conditions that, when satisfied, guarantee the closeness of the outputs of two systems equipped with their corresponding controllers, thus eliminating the need for post-facto verification. We demonstrate the effectiveness of our approach through case studies involving a vehicle and a double inverted pendulum. △ Less

Submitted 2 December, 2024; originally announced December 2024.

Data-driven Construction of Finite Abstractions for Interconnected Systems: A Compositional Approach

Authors: Daniel Ajeleye, Majid Zamani

Abstract: Finite-state abstractions (a.k.a. symbolic models) present a promising avenue for the formal verification and synthesis of controllers in continuous-space control systems. These abstractions provide simplified models that capture the fundamental behaviors of the original systems. However, the creation of such abstractions typically relies on the availability of precise knowledge concerning system… ▽ More Finite-state abstractions (a.k.a. symbolic models) present a promising avenue for the formal verification and synthesis of controllers in continuous-space control systems. These abstractions provide simplified models that capture the fundamental behaviors of the original systems. However, the creation of such abstractions typically relies on the availability of precise knowledge concerning system dynamics, which might not be available in many real-world applications. In this work, we introduce a novel data-driven and compositional approach for constructing finite abstractions for interconnected systems comprised of discrete-time control subsystems with partially unknown dynamics. These subsystems interact through a partially unknown static interconnection map. Our methodology for abstracting the interconnected system involves constructing abstractions for individual subsystems and incorporating an abstraction of the interconnection map. △ Less

Submitted 21 February, 2025; v1 submitted 15 August, 2024; originally announced August 2024.

Comments: This manuscript of 25 pages and 10 figures is a preprint under review with a journal

Verification of Diagnosability for Cyber-Physical Systems: A Hybrid Barrier Certificate Approach

Authors: Bingzhuo Zhong, Weijie Dong, Xiang Yin, Majid Zamani

Abstract: Diagnosability is a system theoretical property characterizing whether fault occurrences in a system can always be detected within a finite time. In this paper, we investigate the verification of diagnosability for cyber-physical systems with continuous state sets. We develop an abstraction-free and automata-based framework to verify (the lack of) diagnosability, leveraging a notion of hybrid barr… ▽ More Diagnosability is a system theoretical property characterizing whether fault occurrences in a system can always be detected within a finite time. In this paper, we investigate the verification of diagnosability for cyber-physical systems with continuous state sets. We develop an abstraction-free and automata-based framework to verify (the lack of) diagnosability, leveraging a notion of hybrid barrier certificates. To this end, we first construct a (delta,K)-deterministic finite automaton that captures the occurrence of faults targeted for diagnosis. Then, the verification of diagnosability property is converted into a safety verification problem over a product system between the automaton and the augmented version of the dynamical system. We demonstrate that this verification problem can be addressed by computing hybrid barrier certificates for the product system. To this end, we introduce two systematic methods, leveraging sum-of-squares programming and counter-example guided inductive synthesis to search for such certificates. Additionally, if the system is found to be diagnosable, we propose methodologies to construct a diagnoser to identify fault occurrences online. Finally, we showcase the effectiveness of our methods through a case study. △ Less

Submitted 13 August, 2024; originally announced August 2024.

Data-Driven Controlled Invariant Sets for Gaussian Process State Space Models

Authors: Paul Griffioen, Bingzhuo Zhong, Murat Arcak, Majid Zamani, Marco Caccamo

Abstract: We compute probabilistic controlled invariant sets for nonlinear systems using Gaussian process state space models, which are data-driven models that account for unmodeled and unknown nonlinear dynamics. We investigate the relationship between robust and probabilistic invariance, leveraging this relationship to design state-feedback controllers that maximize the probability of the system staying w… ▽ More We compute probabilistic controlled invariant sets for nonlinear systems using Gaussian process state space models, which are data-driven models that account for unmodeled and unknown nonlinear dynamics. We investigate the relationship between robust and probabilistic invariance, leveraging this relationship to design state-feedback controllers that maximize the probability of the system staying within the probabilistic controlled invariant set. We propose a semi-definite-programming-based optimization scheme for designing the state-feedback controllers subject to input constraints. The effectiveness of our results are demonstrated and validated on a quadrotor, both in simulation and on a physical platform. △ Less

Submitted 15 July, 2024; originally announced July 2024.

Transfer of Safety Controllers Through Learning Deep Inverse Dynamics Model

Authors: Alireza Nadali, Ashutosh Trivedi, Majid Zamani

Abstract: Control barrier certificates have proven effective in formally guaranteeing the safety of the control systems. However, designing a control barrier certificate is a time-consuming and computationally expensive endeavor that requires expert input in the form of domain knowledge and mathematical maturity. Additionally, when a system undergoes slight changes, the new controller and its correctness ce… ▽ More Control barrier certificates have proven effective in formally guaranteeing the safety of the control systems. However, designing a control barrier certificate is a time-consuming and computationally expensive endeavor that requires expert input in the form of domain knowledge and mathematical maturity. Additionally, when a system undergoes slight changes, the new controller and its correctness certificate need to be recomputed, incurring similar computational challenges as those faced during the design of the original controller. Prior approaches have utilized transfer learning to transfer safety guarantees in the form of a barrier certificate while maintaining the control invariant. Unfortunately, in practical settings, the source and the target environments often deviate substantially in their control inputs, rendering the aforementioned approach impractical. To address this challenge, we propose integrating \emph{inverse dynamics} -- a neural network that suggests required action given a desired successor state -- of the target system with the barrier certificate of the source system to provide formal proof of safety. In addition, we propose a validity condition that, when met, guarantees correctness of the controller. We demonstrate the effectiveness of our approach through three case studies. △ Less

Submitted 24 May, 2024; v1 submitted 22 May, 2024; originally announced May 2024.

Comments: Extended Version, submitted to ADHS 2024

On Approximate Opacity of Stochastic Control Systems

Authors: Siyuan Liu, Xiang Yin, Dimos V. Dimarogonas, Majid Zamani

Abstract: This paper investigates an important class of information-flow security property called opacity for stochastic control systems. Opacity captures whether a system's secret behavior (a subset of the system's behavior that is considered to be critical) can be kept from outside observers. Existing works on opacity for control systems only provide a binary characterization of the system's security leve… ▽ More This paper investigates an important class of information-flow security property called opacity for stochastic control systems. Opacity captures whether a system's secret behavior (a subset of the system's behavior that is considered to be critical) can be kept from outside observers. Existing works on opacity for control systems only provide a binary characterization of the system's security level by determining whether the system is opaque or not. In this work, we introduce a quantifiable measure of opacity that considers the likelihood of satisfying opacity for stochastic control systems modeled as general Markov decision processes (gMDPs). We also propose verification methods tailored to the new notions of opacity for finite gMDPs by using value iteration techniques. Then, a new notion called approximate opacity-preserving stochastic simulation relation is proposed, which captures the distance between two systems' behaviors in terms of preserving opacity. Based on this new system relation, we show that one can verify opacity for stochastic control systems using their abstractions (modeled as finite gMDPs). We also discuss how to construct such abstractions for a class of gMDPs under certain stability conditions. △ Less

Submitted 14 December, 2024; v1 submitted 3 January, 2024; originally announced January 2024.

Comments: 16 pages, 6 figures; This paper has been accepted at IEEE Transactions on Automatic Control

Co-Buchi Barrier Certificates for Discrete-time Dynamical Systems

Authors: Vishnu Murali, Ashutosh Trivedi, Majid Zamani

Abstract: Barrier certificates provide functional overapproximations for the reachable set of dynamical systems and provide inductive guarantees on the safe evolution of the system. Formally a barrier certificate is a real-valued function over the state set that is required to be non-positive for the initial states, positive over the set of unsafe states and nonincreasing along the state transitions. These… ▽ More Barrier certificates provide functional overapproximations for the reachable set of dynamical systems and provide inductive guarantees on the safe evolution of the system. Formally a barrier certificate is a real-valued function over the state set that is required to be non-positive for the initial states, positive over the set of unsafe states and nonincreasing along the state transitions. These conditions together provide an inductive argument that the system will not reach an unsafe state even once as the barrier certificate remains non-positive for all reachable states. In the automata-theoretic approach to verification, a key query is to determine whether the system visits a given predicate over the states finitely often, typically resulting from the complement of the traditional Buchi acceptance condition. This paper proposes a barrier certificate approach to answer such queries by developing a notion of co-Buchi barrier certificates (CBBCs) that generalize classic barrier certificates to ensure that the traces of a system visit a given predicate a fixed number of times. Our notion of CBBC is inspired from bounded synthesis paradigm to LTL realizability, where the LTL specifications are converted to safety automata via universal co-Buchi automata with a bound on final state visitations provided as a hyperparameter. Our application of CBBCs in verification is analogous in nature: we fix a bound and search for a suitable barrier certificate, increasing the bound if no suitable function can be found. We then use these CBBCs to verify our system against properties specified by co-Buchi automata and demonstrate their effectiveness via some case studies. We also show that the present approach strictly generalizes performant barrier certificate based approaches that rely on cutting the paths of the automata that start from an initial state and reach some accepting states. △ Less

Submitted 13 November, 2023; originally announced November 2023.

Secure-by-Construction Synthesis for Control Systems

Authors: Bingzhuo Zhong, Siyuan Liu, Marco Caccamo, Majid Zamani

Abstract: In this paper, we present the synthesis of secure-by-construction controllers that address safety and security properties simultaneously in cyber-physical systems. Our focus is on studying a specific security property called opacity, which characterizes the system's ability to maintain plausible deniability of its secret behavior in the presence of an intruder. These controllers are synthesized ba… ▽ More In this paper, we present the synthesis of secure-by-construction controllers that address safety and security properties simultaneously in cyber-physical systems. Our focus is on studying a specific security property called opacity, which characterizes the system's ability to maintain plausible deniability of its secret behavior in the presence of an intruder. These controllers are synthesized based on a concept of so-called (augmented) control barrier functions, which we introduce and discuss in detail. We propose conditions that facilitate the construction of the desired (augmented) control barrier functions and their corresponding secure-by-construction controllers. To compute these functions, we propose an iterative scheme that leverages iterative sum-of-square programming techniques. This approach enables efficient computation of these functions, particularly for polynomial systems. Moreover, we demonstrate the flexibility of our approach by incorporating user-defined cost functions into the construction of secure-by-construction controllers. Finally, we validate the effectiveness of our results through two case studies, illustrating the practical applicability and benefits of our proposed approach. △ Less

Submitted 16 February, 2024; v1 submitted 5 July, 2023; originally announced July 2023.

Closure Certificates

Authors: Vishnu Murali, Ashutosh Trivedi, Majid Zamani

Abstract: A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT) barrier certificates enable an automated deduc… ▽ More A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT) barrier certificates enable an automated deductive verification approach to safety. The barrier certificate approach has been extended to refute omega-regular specifications by separating consecutive transitions of omega-automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We provide SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness via a paradigmatic case study. △ Less

Submitted 5 March, 2024; v1 submitted 27 May, 2023; originally announced May 2023.

Comments: 14 pages, 5 figures. To appear in 27th ACM International Conference on Hybrid Systems: Computation and Control Hong-Kong, 13-16 May 2024

Collaborative Bearing Estimation Using Set Membership Methods

Authors: Mohammad Zamani, Jochen Trumpf, Chris Manzie

Abstract: We consider the problem of collaborative bearing estimation using a method with historic roots in set theoretic estimation techniques. We refer to this method as the Convex Combination Ellipsoid (CCE) method and show that it provides a less conservative covariance estimate than the well known Covariance Intersection (CI) method. The CCE method does not introduce additional uncertainty that was not… ▽ More We consider the problem of collaborative bearing estimation using a method with historic roots in set theoretic estimation techniques. We refer to this method as the Convex Combination Ellipsoid (CCE) method and show that it provides a less conservative covariance estimate than the well known Covariance Intersection (CI) method. The CCE method does not introduce additional uncertainty that was not already present in the prior estimates. Using our proposed approach for collaborative bearing estimation, the nonlinearity of the bearing measurement is captured as an uncertainty ellipsoid thereby avoiding the need for linearization or approximation via sampling procedures. Simulations are undertaken to evaluate the relative performance of the collaborative bearing estimation solution using the proposed (CCE) and typical (CI) methods. △ Less

Submitted 17 April, 2023; originally announced April 2023.

Comments: 7 pages, 6 figures, Fusion 2023 Conference

Abstraction-Based Verification of Approximate Pre-Opacity for Control Systems

Authors: Junyao Hou, Siyuan Liu, Xiang Yin, Majid Zamani

Abstract: In this paper, we consider the problem of verifying pre-opacity for discrete-time control systems. Pre-opacity is an important information-flow security property that secures the intention of a system to execute some secret behaviors in the future. Existing works on pre-opacity only consider non-metric discrete systems, where it is assumed that intruders can distinguish different output behaviors… ▽ More In this paper, we consider the problem of verifying pre-opacity for discrete-time control systems. Pre-opacity is an important information-flow security property that secures the intention of a system to execute some secret behaviors in the future. Existing works on pre-opacity only consider non-metric discrete systems, where it is assumed that intruders can distinguish different output behaviors precisely. However, for continuous-space control systems whose output sets are equipped with metrics (which is the case for most real-world applications), it is too restrictive to assume precise measurements from outside observers. In this paper, we first introduce a concept of approximate pre-opacity by capturing the security level of control systems with respect to the measurement precision of the intruder. Based on this new notion of pre-opacity, we propose a verification approach for continuous-space control systems by leveraging abstraction-based techniques. In particular, a new concept of approximate pre-opacity preserving simulation relation is introduced to characterize the distance between two systems in terms of preserving pre-opacity. This new system relation allows us to verify pre-opacity of complex continuous-space control systems using their finite abstractions. We also present a method to construct pre-opacity preserving finite abstractions for a class of discrete-time control systems under certain stability assumptions. △ Less

Submitted 8 November, 2022; originally announced November 2022.

Comments: Discrete Event Systems, Opacity, Formal Abstractions

NET-TEN: a silicon neuromorphic network for low-latency detection of seizures in local field potentials

Authors: Margherita Ronchini, Yasser Rezaeiyan, Milad Zamani, Gabriella Panuccio, Farshad Moradi

Abstract: Therapeutic intervention in neurological disorders still relies heavily on pharmacological solutions, while the treatment of patients with drug resistance remains an open challenge. This is particularly true for patients with epilepsy, 30% of whom are refractory to medications. Implantable devices for chronic recording and electrical modulation of brain activity have proved a viable alternative in… ▽ More Therapeutic intervention in neurological disorders still relies heavily on pharmacological solutions, while the treatment of patients with drug resistance remains an open challenge. This is particularly true for patients with epilepsy, 30% of whom are refractory to medications. Implantable devices for chronic recording and electrical modulation of brain activity have proved a viable alternative in such cases. To operate, the device should detect the relevant electrographic biomarkers from Local Field Potentials (LFPs) and determine the right time for stimulation. To enable timely interventions, the ideal device should attain biomarker detection with low latency while operating under low power consumption to prolong the battery life. Neuromorphic networks have progressively gained reputation as low-latency low-power computing systems, which makes them a promising candidate as processing core of next-generation implantable neural interfaces. Here we introduce a fully-analog neuromorphic device implemented in CMOS technology for analyzing LFP signals in an in vitro model of acute ictogenesis. We show that the system can detect ictal and interictal events with ms-latency and with high precision, consuming on average 3.50 nW during the task. Our work paves the way to a new generation of brain implantable devices for personalized closed-loop stimulation for epilepsy treatment. △ Less

Submitted 19 October, 2022; originally announced October 2022.

Comments: 14 pages, 6 figures

In the realm of hybrid Brain: Human Brain and AI

Authors: Hoda Fares, Margherita Ronchini, Milad Zamani, Hooman Farkhani, Farshad Moradi

Abstract: With the recent developments in neuroscience and engineering, it is now possible to record brain signals and decode them. Also, a growing number of stimulation methods have emerged to modulate and influence brain activity. Current brain-computer interface (BCI) technology is mainly on therapeutic outcomes, it already demonstrated its efficiency as assistive and rehabilitative technology for patien… ▽ More With the recent developments in neuroscience and engineering, it is now possible to record brain signals and decode them. Also, a growing number of stimulation methods have emerged to modulate and influence brain activity. Current brain-computer interface (BCI) technology is mainly on therapeutic outcomes, it already demonstrated its efficiency as assistive and rehabilitative technology for patients with severe motor impairments. Recently, artificial intelligence (AI) and machine learning (ML) technologies have been used to decode brain signals. Beyond this progress, combining AI with advanced BCIs in the form of implantable neurotechnologies grants new possibilities for the diagnosis, prediction, and treatment of neurological and psychiatric disorders. In this context, we envision the development of closed loop, intelligent, low-power, and miniaturized neural interfaces that will use brain inspired AI techniques with neuromorphic hardware to process the data from the brain. This will be referred to as Brain Inspired Brain Computer Interfaces (BI-BCIs). Such neural interfaces would offer access to deeper brain regions and better understanding for brain's functions and working mechanism, which improves BCIs operative stability and system's efficiency. On one hand, brain inspired AI algorithms represented by spiking neural networks (SNNs) would be used to interpret the multimodal neural signals in the BCI system. On the other hand, due to the ability of SNNs to capture rich dynamics of biological neurons and to represent and integrate different information dimensions such as time, frequency, and phase, it would be used to model and encode complex information processing in the brain and to provide feedback to the users. This paper provides an overview of the different methods to interface with the brain, presents future applications and discusses the merger of AI and BCIs. △ Less

Submitted 17 January, 2024; v1 submitted 4 October, 2022; originally announced October 2022.

Comments: 44 Pages, 12 Figures, In review

Compositional Reinforcement Learning for Discrete-Time Stochastic Control Systems

Authors: Abolfazl Lavaei, Mateo Perez, Milad Kazemi, Fabio Somenzi, Sadegh Soudjani, Ashutosh Trivedi, Majid Zamani

Abstract: We propose a compositional approach to synthesize policies for networks of continuous-space stochastic control systems with unknown dynamics using model-free reinforcement learning (RL). The approach is based on implicitly abstracting each subsystem in the network with a finite Markov decision process with unknown transition probabilities, synthesizing a strategy for each abstract model in an assu… ▽ More We propose a compositional approach to synthesize policies for networks of continuous-space stochastic control systems with unknown dynamics using model-free reinforcement learning (RL). The approach is based on implicitly abstracting each subsystem in the network with a finite Markov decision process with unknown transition probabilities, synthesizing a strategy for each abstract model in an assume-guarantee fashion using RL, and then mapping the results back over the original network with approximate optimality guarantees. We provide lower bounds on the satisfaction probability of the overall network based on those over individual subsystems. A key contribution is to leverage the convergence results for adversarial RL (minimax Q-learning) on finite stochastic arenas to provide control strategies maximizing the probability of satisfaction over the network of continuous-space systems. We consider finite-horizon properties expressed in the syntactically co-safe fragment of linear temporal logic. These properties can readily be converted into automata-based reward functions, providing scalar reward signals suitable for RL. Since such reward functions are often sparse, we supply a potential-based reward shaping technique to accelerate learning by producing dense rewards. The effectiveness of the proposed approaches is demonstrated via two physical benchmarks including regulation of a room temperature network and control of a road traffic network. △ Less

Submitted 6 August, 2022; originally announced August 2022.

Constructing MDP Abstractions Using Data with Formal Guarantees

Authors: Abolfazl Lavaei, Sadegh Soudjani, Emilio Frazzoli, Majid Zamani

Abstract: This paper is concerned with a data-driven technique for constructing finite Markov decision processes (MDPs) as finite abstractions of discrete-time stochastic control systems with unknown dynamics while providing formal closeness guarantees. The proposed scheme is based on notions of stochastic bisimulation functions (SBF) to capture the probabilistic distance between state trajectories of an un… ▽ More This paper is concerned with a data-driven technique for constructing finite Markov decision processes (MDPs) as finite abstractions of discrete-time stochastic control systems with unknown dynamics while providing formal closeness guarantees. The proposed scheme is based on notions of stochastic bisimulation functions (SBF) to capture the probabilistic distance between state trajectories of an unknown stochastic system and those of finite MDP. In our proposed setting, we first reformulate corresponding conditions of SBF as a robust convex program (RCP). We then propose a scenario convex program (SCP) associated to the original RCP by collecting a finite number of data from trajectories of the system. We ultimately construct an SBF between the data-driven finite MDP and the unknown stochastic system with a given confidence level by establishing a probabilistic relation between optimal values of the SCP and the RCP. We also propose two different approaches for the construction of finite MDPs from data. We illustrate the efficacy of our results over a nonlinear jet engine compressor with unknown dynamics. We construct a data-driven finite MDP as a suitable substitute of the original system to synthesize controllers maintaining the system in a safe set with some probability of satisfaction and a desirable confidence level. △ Less

Submitted 29 June, 2022; originally announced June 2022.

Comments: This work has been accepted at IEEE Control Systems Letters

A Logistic Regression Approach to Field Estimation Using Binary Measurements

Authors: Alex S. Leong, Mohammad Zamani, Iman Shames

Abstract: In this letter, we consider the problem of field estimation using binary measurements. Previous work has formulated the problem as a parameter estimation problem, with the parameter estimation carried out in an online manner using sequential Monte Carlo techniques. In the current work, we consider an alternative approach to the parameter estimation based on online logistic regression. The develope… ▽ More In this letter, we consider the problem of field estimation using binary measurements. Previous work has formulated the problem as a parameter estimation problem, with the parameter estimation carried out in an online manner using sequential Monte Carlo techniques. In the current work, we consider an alternative approach to the parameter estimation based on online logistic regression. The developed algorithm is less computationally intensive than the sequential Monte Carlo approach, while having more reliable estimation performance. △ Less

Submitted 1 June, 2022; originally announced June 2022.

Synthesizing Safety Controllers for Uncertain Linear Systems: A Direct Data-driven Approach

Authors: Bingzhuo Zhong, Majid Zamani, Marco Caccamo

Abstract: In this paper, we provide a direct data-driven approach to synthesize safety controllers for unknown linear systems affected by unknown-but-bounded disturbances, in which identifying the unknown model is not required. First, we propose a notion of $γ$-robust safety invariant ($γ$-RSI) sets and their associated state-feedback controllers, which can be applied to enforce invariance properties. Then,… ▽ More In this paper, we provide a direct data-driven approach to synthesize safety controllers for unknown linear systems affected by unknown-but-bounded disturbances, in which identifying the unknown model is not required. First, we propose a notion of $γ$-robust safety invariant ($γ$-RSI) sets and their associated state-feedback controllers, which can be applied to enforce invariance properties. Then, we formulate a data-driven computation of these sets in terms of convex optimization problems with linear matrix inequalities (LMI) as constraints, which can be solved based on a finite number of data collected from a single input-state trajectory of the system. To show the effectiveness of the proposed approach, we apply our results to a 4-dimensional inverted pendulum. △ Less

Submitted 1 June, 2022; originally announced June 2022.

Comments: 6th IEEE Conference on Control Technology and Applications

Efficient Approximation of Action Potentials with High-Order Shape Preservation in Unsupervised Spike Sorting

Authors: Majid Zamani, Christian Okreghe, Andreas Demosthenous

Abstract: This paper presents a novel approximation unit added to the conventional spike processing chain which provides an appreciable reduction of complexity of the high-hardware cost feature extractors. The use of the Taylor polynomial is proposed and modelled employing its cascaded derivatives to non-uniformly capture the essential samples in each spike for reliable feature extraction and sorting. Inclu… ▽ More This paper presents a novel approximation unit added to the conventional spike processing chain which provides an appreciable reduction of complexity of the high-hardware cost feature extractors. The use of the Taylor polynomial is proposed and modelled employing its cascaded derivatives to non-uniformly capture the essential samples in each spike for reliable feature extraction and sorting. Inclusion of the approximation unit can provide 3X compression (i.e. from 66 to 22 samples) to the spike waveforms while preserving their shapes. Detailed spike waveform sequences based on in-vivo measurements have been generated using a customized neural simulator for performance assessment of the approximation unit tested on six published feature extractors. For noise levels σ_N between 0.05 and 0.3 and groups of 3 spikes in each channel, all the feature extractors provide almost same sorting performance before and after approximation. The overall implementation cost when including the approximation unit and feature extraction shows a large reduction (i.e. up to 8.7X) in the hardware costly and more accurate feature extractors, offering a substantial improvement in feature extraction design. △ Less

Submitted 28 April, 2022; originally announced April 2022.

Sandboxing (AI-based) Unverified Controllers in Stochastic Games: An Abstraction-based Approach with Safe-visor Architecture

Authors: Bingzhuo Zhong, Hongpeng Cao, Majid Zamani, Marco Caccamo

Abstract: In this paper, we propose a construction scheme for a Safe-visor architecture for sandboxing unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, in two-players non-cooperative stochastic games. Concretely, we leverage abstraction-based approaches to construct a supervisor that checks and decides whether or not to accept the inputs provided by the unverified c… ▽ More In this paper, we propose a construction scheme for a Safe-visor architecture for sandboxing unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, in two-players non-cooperative stochastic games. Concretely, we leverage abstraction-based approaches to construct a supervisor that checks and decides whether or not to accept the inputs provided by the unverified controller, and a safety advisor that provides fallback control inputs to ensure safety whenever the unverified controller is rejected. Moreover, by leveraging an ($ε,δ$)-approximate probabilistic relation between the original game and its finite abstraction, we provide a formal safety guarantee with respect to safety specifications modeled by deterministic finite automata (DFA), while the functionality of the unverified controllers is still exploited. To show the effectiveness of the proposed results, we apply them to a control problem of a quadrotor tracking a moving ground vehicle, in which an AI-based unverified controller is employed to control the quadrotor. △ Less

Submitted 28 March, 2022; originally announced March 2022.

Compositional Synthesis of Signal Temporal Logic Tasks via Assume-Guarantee Contracts

Authors: Siyuan Liu, Adnane Saoud, Pushpak Jagtap, Dimos V. Dimarogonas, Majid Zamani

Abstract: In this paper, we focus on the problem of compositional synthesis of controllers enforcing signal temporal logic (STL) tasks over a class of continuous-time nonlinear interconnected systems. By leveraging the idea of funnel-based control, we show that a fragment of STL specifications can be formulated as assume-guarantee contracts. A new concept of contract satisfaction is then defined to establis… ▽ More In this paper, we focus on the problem of compositional synthesis of controllers enforcing signal temporal logic (STL) tasks over a class of continuous-time nonlinear interconnected systems. By leveraging the idea of funnel-based control, we show that a fragment of STL specifications can be formulated as assume-guarantee contracts. A new concept of contract satisfaction is then defined to establish our compositionality result, which allows us to guarantee the satisfaction of a global contract by the interconnected system when all subsystems satisfy their local contracts. Based on this compositional framework, we then design closed-form continuous-time feedback controllers to enforce local contracts over subsystems in a decentralized manner. Finally, we demonstrate the effectiveness of our results on two numerical examples. △ Less

Submitted 18 March, 2022; originally announced March 2022.

Journal ref: IEEE 61st Conference on Decision and Control (CDC), Cancun, Mexico, 2022, pp. 2184-2189

Secure-by-Construction Synthesis of Cyber-Physical Systems

Authors: Siyuan Liu, Ashutosh Trivedi, Xiang Yin, Majid Zamani

Abstract: Correct-by-construction synthesis is a cornerstone of the confluence of formal methods and control theory towards designing safety-critical systems. Instead of following the time-tested, albeit laborious (re)design-verify-validate loop, correct-by-construction methodology advocates the use of continual refinements of formal requirements -- connected by chains of formal proofs -- to build a system… ▽ More Correct-by-construction synthesis is a cornerstone of the confluence of formal methods and control theory towards designing safety-critical systems. Instead of following the time-tested, albeit laborious (re)design-verify-validate loop, correct-by-construction methodology advocates the use of continual refinements of formal requirements -- connected by chains of formal proofs -- to build a system that assures the correctness by design. A remarkable progress has been made in scaling the scope of applicability of correct-by-construction synthesis -- with a focus on cyber-physical systems that tie discrete-event control with continuous environment -- to enlarge control systems by combining symbolic approaches with principled state-space reduction techniques. Unfortunately, in the security-critical control systems, the security properties are verified ex post facto the design process in a way that undermines the correct-by-construction paradigm. We posit that, to truly realize the dream of correct-by-construction synthesis for security-critical systems, security considerations must take center-stage with the safety considerations. Moreover, catalyzed by the recent progress on the opacity sub-classes of security properties and the notion of hyperproperties capable of combining security with safety properties, we believe that the time is ripe for the research community to holistically target the challenge of secure-by-construction synthesis. This paper details our vision by highlighting the recent progress and open challenges that may serve as bricks for providing a solid foundation for secure-by-construction synthesis of cyber-physical systems. △ Less

Submitted 14 February, 2022; originally announced February 2022.

Structural Consensus in Networks with Directed Topologies and Its Cryptographic Implementation

Authors: Wentuo Fang, Zhiyong Chen, Mohsen Zamani

Abstract: The existing cryptosystem based approaches for privacy-preserving consensus of networked systems are usually limited to those with undirected topologies. This paper proposes a new privacy-preserving algorithm for networked systems with directed topologies to reach confidential consensus. As a prerequisite for applying the algorithm, a structural consensus problem is formulated and the solvability… ▽ More The existing cryptosystem based approaches for privacy-preserving consensus of networked systems are usually limited to those with undirected topologies. This paper proposes a new privacy-preserving algorithm for networked systems with directed topologies to reach confidential consensus. As a prerequisite for applying the algorithm, a structural consensus problem is formulated and the solvability conditions are discussed for an explicitly constructed controller. The controller is then implemented with encryption to achieve consensus while avoiding individual's information leakage to external eavesdroppers and/or malicious internal neighbors. △ Less

Submitted 18 January, 2022; originally announced January 2022.

Comments: 24 pages, 7 figures. The paper has been submitted to ISA Transactions

Data-driven Safety Verification of Stochastic Systems via Barrier Certificates

Authors: Ali Salamati, Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

Abstract: In this paper, we propose a data-driven approach to formally verify the safety of (potentially) unknown discrete-time continuous-space stochastic systems. The proposed framework is based on a notion of barrier certificates together with data collected from trajectories of unknown systems. We first reformulate the barrier-based safety verification as a robust convex problem (RCP). Solving the acqui… ▽ More In this paper, we propose a data-driven approach to formally verify the safety of (potentially) unknown discrete-time continuous-space stochastic systems. The proposed framework is based on a notion of barrier certificates together with data collected from trajectories of unknown systems. We first reformulate the barrier-based safety verification as a robust convex problem (RCP). Solving the acquired RCP is hard in general because not only the state of the system lives in a continuous set, but also and more problematic, the unknown model appears in one of the constraints of RCP. Instead, we leverage a finite number of data, and accordingly, the RCP is casted as a scenario convex problem (SCP). We then relate the optimizer of the SCP to that of the RCP, and consequently, we provide a safety guarantee over the unknown stochastic system with a priori guaranteed confidence. We apply our approach to an unknown room temperature system by collecting sampled data from trajectories of the system and verify formally that temperature of the room lies in a comfort zone for a finite time horizon with a desired confidence. △ Less

Submitted 23 December, 2021; originally announced December 2021.

Data-driven verification and synthesis of stochastic systems via barrier certificates

Authors: Ali Salamati, Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

Abstract: In this work, we study verification and synthesis problems for safety specifications over unknown discrete-time stochastic systems. When a model of the system is available, barrier certificates have been successfully applied for ensuring the satisfaction of safety specifications. In this work, we formulate the computation of barrier certificates as a robust convex program (RCP). Solving the acquir… ▽ More In this work, we study verification and synthesis problems for safety specifications over unknown discrete-time stochastic systems. When a model of the system is available, barrier certificates have been successfully applied for ensuring the satisfaction of safety specifications. In this work, we formulate the computation of barrier certificates as a robust convex program (RCP). Solving the acquired RCP is hard in general because the model of the system that appears in one of the constraints of the RCP is unknown. We propose a data-driven approach that replaces the uncountable number of constraints in the RCP with a finite number of constraints by taking finitely many random samples from the trajectories of the system. We thus replace the original RCP with a scenario convex program (SCP) and show how to relate their optimizers. We guarantee that the solution of the SCP is a solution of the RCP with a priori guaranteed confidence when the number of samples is larger than a pre-computed value. This provides a lower bound on the safety probability of the original unknown system together with a controller in the case of synthesis. We also discuss an extension of our verification approach to a case where the associated robust program is non-convex and show how a similar methodology can be applied. Finally, the applicability of our proposed approach is illustrated through three case studies. △ Less

Submitted 9 September, 2023; v1 submitted 19 November, 2021; originally announced November 2021.

Formal Synthesis of Controllers for Uncertain Linear Systems against $ω$-Regular Properties: A Set-based Approach

Authors: Bingzhuo Zhong, Majid Zamani, Marco Caccamo

Abstract: In this paper, we present how to synthesize controllers to enforce $ω$-regular properties over linear control systems affected by bounded disturbances. In particular, these controllers are synthesized based on so-called hybrid controlled invariant (HCI) sets. To compute these sets, we first construct a product system between the linear control system and the deterministic Streett automata (DSA) mo… ▽ More In this paper, we present how to synthesize controllers to enforce $ω$-regular properties over linear control systems affected by bounded disturbances. In particular, these controllers are synthesized based on so-called hybrid controlled invariant (HCI) sets. To compute these sets, we first construct a product system between the linear control system and the deterministic Streett automata (DSA) modeling the desired property. Then, we compute the maximal HCI set over the state set of the product system by leveraging a set-based approach. To ensure termination of the computation of the HCI sets within a finite number of iterations, we also propose two iterative schemes to compute approximations of the maximal HCI set. Finally, we show the effectiveness of our results via two case studies. △ Less

Submitted 12 August, 2022; v1 submitted 16 November, 2021; originally announced November 2021.

Learning Safety Filters for Unknown Discrete-Time Linear Systems

Authors: Farhad Farokhi, Alex S. Leong, Mohammad Zamani, Iman Shames

Abstract: A learning-based safety filter is developed for discrete-time linear time-invariant systems with unknown models subject to Gaussian noises with unknown covariance. Safety is characterized using polytopic constraints on the states and control inputs. The empirically learned model and process noise covariance with their confidence bounds are used to construct a robust optimization problem for minima… ▽ More A learning-based safety filter is developed for discrete-time linear time-invariant systems with unknown models subject to Gaussian noises with unknown covariance. Safety is characterized using polytopic constraints on the states and control inputs. The empirically learned model and process noise covariance with their confidence bounds are used to construct a robust optimization problem for minimally modifying nominal control actions to ensure safety with high probability. The optimization problem relies on tightening the original safety constraints. The magnitude of the tightening is larger at the beginning since there is little information to construct reliable models, but shrinks with time as more data becomes available. △ Less

Submitted 8 May, 2023; v1 submitted 31 October, 2021; originally announced November 2021.

Compositional Construction of Abstractions for Infinite Networks of Switched Systems

Authors: Maryam Sharifi, Abdalla Swikir, Navid Noroozi, Majid Zamani

Abstract: We construct compositional continuous approximations for an interconnection of infinitely many discrete-time switched systems. An approximation (known as abstraction) is itself a continuous-space system, which can be used as a replacement of the original (known as concrete) system in a controller design process. Having synthesized a controller for the abstract system, the controller is refined to… ▽ More We construct compositional continuous approximations for an interconnection of infinitely many discrete-time switched systems. An approximation (known as abstraction) is itself a continuous-space system, which can be used as a replacement of the original (known as concrete) system in a controller design process. Having synthesized a controller for the abstract system, the controller is refined to a more detailed controller for the concrete system. To quantify the mismatch between the output trajectory of the approximation and of that the original system, we use the notion of so-called simulation functions. In particular, each subsystem in the concrete network and its corresponding one in the abstract network is related through a local simulation function. We show that if the local simulation functions satisfy a certain small-gain type condition developed for a network of infinitely many subsystems, then the aggregation of the individual simulation functions provides an overall simulation function between the overall abstraction and the concrete network. For a network of linear switched systems, we systematically construct local abstractions and local simulation functions, where the required conditions are expressed in terms of linear matrix inequalities and can be efficiently computed. We illustrate the effectiveness of our approach through an application to frequency control in a power gird with a switched (i.e. time-varying) topology. △ Less

Submitted 28 September, 2021; originally announced September 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:2101.08873

Compositional Abstractions of Interconnected Discrete-Time Switched Systems

Authors: Abdalla Swikir, Majid Zamani

Abstract: In this paper, we introduce a compositional method for the construction of finite abstractions of interconnected discrete-time switched systems. Particularly, we use a notion of so-called alternating simulation function as a relation between each switched subsystem and its finite abstraction. Based on some small-gain type conditions, we use those alternating simulation functions to construct compo… ▽ More In this paper, we introduce a compositional method for the construction of finite abstractions of interconnected discrete-time switched systems. Particularly, we use a notion of so-called alternating simulation function as a relation between each switched subsystem and its finite abstraction. Based on some small-gain type conditions, we use those alternating simulation functions to construct compositionally an overall alternating simulation function as a relation between an interconnection of finite abstractions and that of switched subsystems. This overall alternating simulation function allows one to quantify the mismatch between the output behavior of the interconnection of switched subsystems and that of their finite abstractions. Additionally, we provide an approach to construct finite abstractions together with their corresponding alternating simulation functions for discrete-time switched subsystems under standard assumptions ensuring incremental input-to-state stability of a switched subsystem. Finally, we apply our results to a model of road traffic by constructing compositionally a finite abstraction of the network containing $50$ cells of $1000$ meters each. We use the constructed finite abstractions as substitutes to design controllers compositionally keeping the density of traffic lower than $30$ vehicles per cell. △ Less

Submitted 28 September, 2021; originally announced September 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:1905.12808, arXiv:1805.06271

Verification of Switched Stochastic Systems via Barrier Certificates

Authors: Mahathi Anand, Pushpak Jagtap, Majid Zamani

Abstract: The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a complex temporal property is satisfied over a finite time horizon. The required temporal properties of the system are expressed using a fragment of linear temporal logic, called safe-LTL with respect to finite traces. Our app… ▽ More The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a complex temporal property is satisfied over a finite time horizon. The required temporal properties of the system are expressed using a fragment of linear temporal logic, called safe-LTL with respect to finite traces. Our approach combines automata-based verification and the use of barrier certificates. It relies on decomposing the automaton associated with the negation of specification into a sequence of simpler reachability tasks and compute upper bounds for these reachability probabilities by means of common or multiple barrier certificates. Theoretical results are illustrated by applying a counter-example guided inductive synthesis framework to find barrier certificates. △ Less

Submitted 25 September, 2021; originally announced September 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:1807.00064

Journal ref: IEEE 58th Conference on Decision and Control (CDC), 2019, pp. 4373-4378

Compositional Verification of Initial-State Opacity for Switched Systems

Authors: Siyuan Liu, Abdalla Swikir, Majid Zamani

Abstract: In this work, we propose a compositional framework for the verification of approximate initial-state opacity for networks of discrete-time switched systems. The proposed approach is based on a notion of approximate initial-state opacity-preserving simulation functions (InitSOPSFs), which characterize how close concrete networks and their finite abstractions are in terms of the satisfaction of appr… ▽ More In this work, we propose a compositional framework for the verification of approximate initial-state opacity for networks of discrete-time switched systems. The proposed approach is based on a notion of approximate initial-state opacity-preserving simulation functions (InitSOPSFs), which characterize how close concrete networks and their finite abstractions are in terms of the satisfaction of approximate initial state opacity. We show that such InitSOPSFs can be obtained compositionally by assuming some small-gain type conditions and composing so-called local InitSOPSFs constructed for each subsystem separately. Additionally, for switched systems satisfying certain stability properties, we provide an approach to construct their finite abstractions together with the corresponding local InitSOPSFs. Finally, the effectiveness of our results is illustrated through an example. △ Less

Submitted 24 September, 2021; originally announced September 2021.

Comments: This paper has been accepted and published in CDC 2020. arXiv admin note: substantial text overlap with arXiv:2006.16661

Journal ref: 59th IEEE Conference on Decision and Control (CDC), pp. 2146-2151, December 2020

Compositional synthesis of almost maximally permissible safety controllers

Authors: Siyuan Liu, Majid Zamani

Abstract: In this work, we present a compositional safety controller synthesis approach for the class of discrete-time linear control systems. Here, we leverage a state-of-the-art result on the computation of robust controlled invariant sets. To tackle the complexity of controller synthesis over complex interconnected systems, this paper introduces a decentralized controller synthesis scheme. Rather than tr… ▽ More In this work, we present a compositional safety controller synthesis approach for the class of discrete-time linear control systems. Here, we leverage a state-of-the-art result on the computation of robust controlled invariant sets. To tackle the complexity of controller synthesis over complex interconnected systems, this paper introduces a decentralized controller synthesis scheme. Rather than treating the interconnected system as a whole, we first design local safety controllers for each subsystem separately to enforce local safety properties, with polytopic state and input constraints as well as bounded disturbance set. Then, by composing the local controllers, the interconnected system is guaranteed to satisfy the overall safety specification. Finally, we provide a vehicular platooning example to illustrate the effectiveness of the proposed approach by solving the overall safety controller synthesis problem by computing less complex local safety controllers for subsystems and then composing them. △ Less

Submitted 24 September, 2021; originally announced September 2021.

Comments: This paper has been accepted and published in ACC 2019

Journal ref: American Control Conference (ACC), pp. 1678-1683, July 2019

Synthesis of Partially Observed Jump-Diffusion Systems via Control Barrier Functions

Authors: Niloofar Jahanshahi, Pushpak Jagtap, Majid Zamani

Abstract: In this paper, we study formal synthesis of control policies for partially observed jump-diffusion systems against complex logic specifications. Given a state estimator, we utilize a discretization-free approach for formal synthesis of control policies by using a notation of control barrier functions without requiring any knowledge of the estimation accuracy. Our goal is to synthesize an offline c… ▽ More In this paper, we study formal synthesis of control policies for partially observed jump-diffusion systems against complex logic specifications. Given a state estimator, we utilize a discretization-free approach for formal synthesis of control policies by using a notation of control barrier functions without requiring any knowledge of the estimation accuracy. Our goal is to synthesize an offline control policy providing (potentially maximizing) a lower bound on the probability that the trajectories of the partially observed jump-diffusion system satisfy some complex specifications expressed by deterministic finite automata. Finally, we illustrate the effectiveness of the proposed results by synthesizing a policy for a jet engine example. △ Less

Submitted 23 September, 2021; originally announced September 2021.

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

Sandboxing Controllers for Stochastic Cyber-Physical Systems

Authors: Bingzhuo Zhong, Majid Zamani, Marco Caccamo

Abstract: Current cyber-physical systems (CPS) are expected to accomplish complex tasks. To achieve this goal, high performance, but unverified controllers (e.g. deep neural network, black-box controllers from third parties) are applied, which makes it very challenging to keep the overall CPS safe. By sandboxing these controllers, we are not only able to use them but also to enforce safety properties over t… ▽ More Current cyber-physical systems (CPS) are expected to accomplish complex tasks. To achieve this goal, high performance, but unverified controllers (e.g. deep neural network, black-box controllers from third parties) are applied, which makes it very challenging to keep the overall CPS safe. By sandboxing these controllers, we are not only able to use them but also to enforce safety properties over the controlled physical systems at the same time. However, current available solutions for sandboxing controllers are just applicable to deterministic (a.k.a. non-stochastic) systems, possibly affected by bounded disturbances. In this paper, for the first time we propose a novel solution for sandboxing unverified complex controllers for CPS operating in noisy environments (a.k.a. stochastic CPS). Moreover, we also provide probabilistic guarantees on their safety. Here, the unverified control input is observed at each time instant and checked whether it violates the maximal tolerable probability of reaching the unsafe set. If this probability exceeds a given threshold, the unverified control input will be rejected, and the advisory input provided by the optimal safety controller will be used to maintain the probabilistic safety guarantee. The proposed approach is illustrated empirically and the results indicate that the expected safety probability is guaranteed. △ Less

Submitted 23 September, 2021; originally announced September 2021.

Comments: International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS 2019

Journal ref: In International Conference on Formal Modeling and Analysis of Timed Systems, pp. 247-264. Springer, Cham, 2019

Verification of Approximate Opacity via Barrier Certificates

Authors: Siyuan Liu, Majid Zamani

Abstract: This paper is motivated by the increasing security concerns of cyber-physical systems. Here, we develop a discretization-free verification scheme targeting an information-flow security property, called approximate initial-state opacity, for the class of discrete-time control systems. We propose notions of so-called augmented control barrier certificates in conjunction with specified regions of int… ▽ More This paper is motivated by the increasing security concerns of cyber-physical systems. Here, we develop a discretization-free verification scheme targeting an information-flow security property, called approximate initial-state opacity, for the class of discrete-time control systems. We propose notions of so-called augmented control barrier certificates in conjunction with specified regions of interest capturing the initial and secret sets of the system. Sufficient conditions for (the lack of) approximate initial-state opacity of discrete-time control systems are proposed based on the existence of the proposed barrier certificates. We further present an efficient computation method by casting the conditions for barrier certificates as sum-of-squares programming problems. The effectiveness of the proposed results is illustrated through two numerical examples. △ Less

Submitted 22 September, 2021; originally announced September 2021.

Comments: This paper has been accepted and published in L-CSS

Journal ref: IEEE Control Systems Letters, vol. 5, no. 4, pp. 1369-1374, Oct. 2021

Optimal Actor-Critic Policy with Optimized Training Datasets

Authors: Chayan Banerjee, Zhiyong Chen, Nasimul Noman, Mohsen Zamani

Abstract: Actor-critic (AC) algorithms are known for their efficacy and high performance in solving reinforcement learning problems, but they also suffer from low sampling efficiency. An AC based policy optimization process is iterative and needs to frequently access the agent-environment system to evaluate and update the policy by rolling out the policy, collecting rewards and states (i.e. samples), and le… ▽ More Actor-critic (AC) algorithms are known for their efficacy and high performance in solving reinforcement learning problems, but they also suffer from low sampling efficiency. An AC based policy optimization process is iterative and needs to frequently access the agent-environment system to evaluate and update the policy by rolling out the policy, collecting rewards and states (i.e. samples), and learning from them. It ultimately requires a huge number of samples to learn an optimal policy. To improve sampling efficiency, we propose a strategy to optimize the training dataset that contains significantly less samples collected from the AC process. The dataset optimization is made of a best episode only operation, a policy parameter-fitness model, and a genetic algorithm module. The optimal policy network trained by the optimized training dataset exhibits superior performance compared to many contemporary AC algorithms in controlling autonomous dynamical systems. Evaluation on standard benchmarks show that the method improves sampling efficiency, ensures faster convergence to optima, and is more data-efficient than its counterparts. △ Less

Submitted 1 December, 2021; v1 submitted 16 August, 2021; originally announced August 2021.

Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates

Authors: Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, Majid Zamani

Abstract: Hyperproperties are system properties that require quantification over multiple execution traces of a system. Hyperproperties can express several specifications of interest for cyber-physical systems--such as opacity, robustness, and noninterference--which cannot be expressed using linear-time properties. This paper presents for the first time a discretization-free approach for the formal verifica… ▽ More Hyperproperties are system properties that require quantification over multiple execution traces of a system. Hyperproperties can express several specifications of interest for cyber-physical systems--such as opacity, robustness, and noninterference--which cannot be expressed using linear-time properties. This paper presents for the first time a discretization-free approach for the formal verification of discrete-time uncertain dynamical systems against hyperproperties. The proposed approach involves decomposition of complex hyperproperties into several verification conditions by exploiting the automata-based structures corresponding to the complements of the original specifications. These verification conditions are then discharged by synthesizing so-called augmented barrier certificates, which provide certain safety guarantees for the underlying system. For systems with polynomial-type dynamics, we present a sound procedure to synthesize polynomial-type augmented barrier certificates by reducing the problem to sum-of-squares optimizations. We demonstrate the effectiveness of our proposed approaches on two physical case studies against two important hyperproperties: initial-state opacity and initial-state robustness. △ Less

Submitted 23 November, 2021; v1 submitted 12 May, 2021; originally announced May 2021.

Comments: 21 pages, 8 figures

Automata-based Controller Synthesis for Stochastic Systems: A Game Framework via Approximate Probabilistic Relations

Authors: Bingzhuo Zhong, Abolfazl Lavaei, Majid Zamani, Marco Caccamo

Abstract: In this work, we propose an abstraction and refinement methodology for the controller synthesis of discrete-time stochastic systems to enforce complex logical properties expressed by deterministic finite automata (a.k.a. DFA). Our proposed scheme is based on a notion of so-called $(ε,δ)$-approximate probabilistic relations, allowing one to quantify the similarity between stochastic systems modeled… ▽ More In this work, we propose an abstraction and refinement methodology for the controller synthesis of discrete-time stochastic systems to enforce complex logical properties expressed by deterministic finite automata (a.k.a. DFA). Our proposed scheme is based on a notion of so-called $(ε,δ)$-approximate probabilistic relations, allowing one to quantify the similarity between stochastic systems modeled by discrete-time stochastic games and their corresponding finite abstractions. Leveraging this type of relations, the lower bound for the probability of satisfying the desired specifications can be well ensured by refining controllers synthesized over abstract systems to the original games. Moreover, we propose an algorithmic procedure to construct such a relation for a particular class of nonlinear stochastic systems with slope restrictions on the nonlinearity. The proposed methods are demonstrated on a quadrotor example, and the results indicate that the desired lower bound for the probability of satisfaction is guaranteed. △ Less

Submitted 5 September, 2022; v1 submitted 23 April, 2021; originally announced April 2021.

Comments: 36 pages, 10 figures, to appear as a regular paper in Automatica

Inertial Collaborative Localisation for Autonomous Vehicles using a Minimum Energy Filter

Authors: Jack Henderson, Mohammad Zamani, Robert Mahony, Jochen Trumpf

Abstract: Collaborative Localisation has been studied extensively in recent years as a way to improve pose estimation of unmanned aerial vehicles in challenging environments. However little attention has been paid toward advancing the underlying filter design beyond standard Extended Kalman Filter-based approaches. In this paper, we detail a discrete-time collaborative localisation filter using the determin… ▽ More Collaborative Localisation has been studied extensively in recent years as a way to improve pose estimation of unmanned aerial vehicles in challenging environments. However little attention has been paid toward advancing the underlying filter design beyond standard Extended Kalman Filter-based approaches. In this paper, we detail a discrete-time collaborative localisation filter using the deterministic minimum-energy framework. The filter incorporates measurements from an inertial measurement unit and models the effects of sensor bias and gravitational acceleration. We present a simulation based on real-world vehicle trajectories and IMU data that demonstrates how collaborative localisation can improve performance over single-vehicle methods. △ Less

Submitted 12 April, 2021; originally announced April 2021.

Comments: Submitted to IEEE 2021 Conference on Decision and Control (CDC2021)

Compositional Construction of Safety Controllers for Networks of Continuous-Space POMDPs

Authors: Niloofar Jahanshahi, Abolfazl Lavaei, Majid Zamani

Abstract: In this paper, we propose a compositional framework for the synthesis of safety controllers for networks of partially-observed discrete-time stochastic control systems (a.k.a. continuous-space POMDPs). Given an estimator, we utilize a discretization-free approach to synthesize controllers ensuring safety specifications over finite-time horizons. The proposed framework is based on a notion of so-ca… ▽ More In this paper, we propose a compositional framework for the synthesis of safety controllers for networks of partially-observed discrete-time stochastic control systems (a.k.a. continuous-space POMDPs). Given an estimator, we utilize a discretization-free approach to synthesize controllers ensuring safety specifications over finite-time horizons. The proposed framework is based on a notion of so-called local control barrier functions computed for subsystems in two different ways. In the first scheme, no prior knowledge of estimation accuracy is needed. The second framework utilizes a probability bound on the estimation accuracy using a notion of so called stochastic simulation functions. In both proposed schemes, we drive sufficient small-gain type conditions in order to compositionally construct control barrier functions for interconnected POMDPs using local barrier functions computed for subsystems. Leveraging compositionality results, the constructed control barrier functions enable us to compute lower bounds on the probabilities that the interconnected POMDPs avoid certain unsafe regions in finite-time horizons. We demonstrate the effectiveness of our proposed approaches by applying them to an adaptive cruise control problem. △ Less

Submitted 10 March, 2021; originally announced March 2021.

Compositional Synthesis of Control Barrier Certificates for Networks of Stochastic Systems against $ω$-Regular Specifications

Authors: Mahathi Anand, Abolfazl Lavaei, Majid Zamani

Abstract: This paper is concerned with a compositional scheme for the construction of control barrier certificates for interconnected discrete-time stochastic systems. The main objective is to synthesize switching control policies against $ω$-regular properties that can be described by accepting languages of deterministic Streett automata (DSA) along with providing probabilistic guarantees for the satisfact… ▽ More This paper is concerned with a compositional scheme for the construction of control barrier certificates for interconnected discrete-time stochastic systems. The main objective is to synthesize switching control policies against $ω$-regular properties that can be described by accepting languages of deterministic Streett automata (DSA) along with providing probabilistic guarantees for the satisfaction of such specifications. The proposed framework leverages the interconnection topology and a notion of so-called \emph{control sub-barrier certificates} of subsystems, which are used to compositionally construct control barrier certificates of interconnected systems by imposing some dissipativity-type compositionality conditions. We propose a systematic approach to decompose high-level $ω$-regular specifications into simpler tasks by utilizing the automata corresponding to the specifications. In addition, we formulate an alternating direction method of multipliers (ADMM) optimization problem in order to obtain suitable control sub-barrier certificates of subsystems while satisfying compositionality conditions. For systems with polynomial dynamics, we provide a sum-of-squares (SOS) optimization problem for the computation of control sub-barrier certificates and local control policies of subsystems. Finally, we demonstrate the effectiveness of our proposed approaches by applying them to a physical case study. △ Less

Submitted 5 July, 2022; v1 submitted 3 March, 2021; originally announced March 2021.

Comments: 23 pages, 5 figures

Safe Learning of Uncertain Environments

Authors: Farhad Farokhi, Alex Leong, Iman Shames, Mohammad Zamani

Abstract: In many learning based control methodologies, learning the unknown dynamic model precedes the control phase, while the aim is to control the system such that it remains in some safe region of the state space. In this work, our aim is to guarantee safety while learning and control proceed simultaneously. Specifically, we consider the problem of safe learning in nonlinear control-affine systems subj… ▽ More In many learning based control methodologies, learning the unknown dynamic model precedes the control phase, while the aim is to control the system such that it remains in some safe region of the state space. In this work, our aim is to guarantee safety while learning and control proceed simultaneously. Specifically, we consider the problem of safe learning in nonlinear control-affine systems subject to unknown additive uncertainty. We first model the uncertainty as a Gaussian noise and use state measurements to learn its mean and covariance. We provide rigorous time-varying bounds on the mean and covariance of the uncertainty and employ them to modify the control input via an optimization program with potentially time-varying safety constraints. We show that with an arbitrarily large probability we can guarantee that the state will remain in the safe set, while learning and control are carried out simultaneously, provided that a feasible solution exists for the optimization problem. We provide a secondary formulation of this optimization that is computationally more efficient. This is based on tightening the safety constraints to counter the uncertainty about the learned mean and covariance. The magnitude of the tightening can be decreased as our confidence in the learned mean and covariance increases (i.e., as we gather more measurements about the environment). Extensions of the method are provided for non-Gaussian process noise with unknown mean and covariance as well as Gaussian uncertainties with state-dependent mean and covariance to accommodate more general environments. △ Less

Submitted 13 May, 2021; v1 submitted 1 March, 2021; originally announced March 2021.

Safe-visor Architecture for Sandboxing (AI-based) Unverified Controllers in Stochastic Cyber-Physical Systems

Authors: Bingzhuo Zhong, Abolfazl Lavaei, Hongpeng Cao, Majid Zamani, Marco Caccamo

Abstract: High performance but unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, are widely employed in cyber-physical systems (CPSs) to accomplish complex control missions. However, guaranteeing the safety and reliability of CPSs with this kind of controllers is currently very challenging, which is of vital importance in many real-life safety-critical applications.… ▽ More High performance but unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, are widely employed in cyber-physical systems (CPSs) to accomplish complex control missions. However, guaranteeing the safety and reliability of CPSs with this kind of controllers is currently very challenging, which is of vital importance in many real-life safety-critical applications. To cope with this difficulty, we propose in this work a Safe-visor architecture for sandboxing unverified controllers in CPSs operating in noisy environments (a.k.a. stochastic CPSs). The proposed architecture contains a history-based supervisor, which checks inputs from the unverified controller and makes a compromise between functionality and safety of the system, and a safety advisor that provides fallback when the unverified controller endangers the safety of the system. Both the history-based supervisor and the safety advisor are designed based on an approximate probabilistic relation between the original system and its finite abstraction. By employing this architecture, we provide formal probabilistic guarantees on preserving the safety specifications expressed by accepting languages of deterministic finite automata (DFA). Meanwhile, the unverified controllers can still be employed in the control loop even though they are not reliable. We demonstrate the effectiveness of our proposed results by applying them to two (physical) case studies. △ Less

Submitted 19 August, 2021; v1 submitted 10 February, 2021; originally announced February 2021.

Symbolic Models for Infinite Networks of Control Systems: A Compositional Approach

Authors: Siyuan Liu, Navid Noroozi, Majid Zamani

Abstract: This paper presents a compositional framework for the construction of symbolic models for a network composed of a countably infinite number of finite-dimensional discrete-time control subsystems. We refer to such a network as infinite network. The proposed approach is based on the notion of alternating simulation functions. This notion relates a concrete network to its symbolic model with guarante… ▽ More This paper presents a compositional framework for the construction of symbolic models for a network composed of a countably infinite number of finite-dimensional discrete-time control subsystems. We refer to such a network as infinite network. The proposed approach is based on the notion of alternating simulation functions. This notion relates a concrete network to its symbolic model with guaranteed mismatch bounds between their output behaviors. We propose a compositional approach to construct a symbolic model for an infinite network, together with an alternating simulation function, by composing symbolic models and alternating simulation functions constructed for subsystems. Assuming that each subsystem is incrementally input-to-state stable and under some small-gain type conditions, we present an algorithm for orderly constructing local symbolic models with properly designed quantization parameters. In this way, the proposed compositional approach can provide us a guideline for constructing an overall symbolic model with any desired approximation accuracy. A compositional controller synthesis scheme is also provided to enforce safety properties on the infinite network in a decentralized fashion. The effectiveness of our result is illustrated through a road traffic network consisting of infinitely many road cells. △ Less

Submitted 28 October, 2021; v1 submitted 5 February, 2021; originally announced February 2021.

Journal ref: Nonlinear Analysis: Hybrid Systems, vol. 43, December 2021