Showing 1–50 of 210 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.

A Scalable Synthesis Algorithm for Reversible Functions

Authors: Moein Sarvaghad-Moghaddam, Morteza Saheb Zamani, Mehdi Sedighi

Abstract: Reversible computation is an emerging technology that has gained significant attention due to its critical role in quantum circuit synthesis and low-power design. This paper introduces a transformation-based method for exact synthesis of reversible circuits. The proposed approach utilizes a novel adaptation of the Quine-McCluskey algorithm to eliminate input-output discrepancies in the truth table… ▽ More Reversible computation is an emerging technology that has gained significant attention due to its critical role in quantum circuit synthesis and low-power design. This paper introduces a transformation-based method for exact synthesis of reversible circuits. The proposed approach utilizes a novel adaptation of the Quine-McCluskey algorithm to eliminate input-output discrepancies in the truth table, transforming the permutation matrix into an identity matrix. Furthermore, a novel search space reduction technique is presented which, combined with the primary method, enables the synthesis algorithm to handle high-input reversible functions. This approach combines the influence of multiple control qubits on a target qubit, evaluating their collective impact. This aggregation can decrease the control qubit count within quantum gates. Consequently, it proves beneficial for applications like surface code error correction architectures as well as current Noisy Intermediate-Scale Quantum (NISQ) hardwares. Experimental results demonstrate significant improvements over the state-of-the-art exact synthesis methods, achieving up to 99% improvements in terms of the number of levels of T-gates. △ Less

Submitted 25 April, 2025; v1 submitted 3 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

Are Convex Optimization Curves Convex?

Authors: Guy Barzilai, Ohad Shamir, Moslem Zamani

Abstract: In this paper, we study when we might expect the optimization curve induced by gradient descent to be \emph{convex} -- precluding, for example, an initial plateau followed by a sharp decrease, making it difficult to decide when optimization should stop. Although such undesirable behavior can certainly occur when optimizing general functions, might it also occur in the benign and well-studied case… ▽ More In this paper, we study when we might expect the optimization curve induced by gradient descent to be \emph{convex} -- precluding, for example, an initial plateau followed by a sharp decrease, making it difficult to decide when optimization should stop. Although such undesirable behavior can certainly occur when optimizing general functions, might it also occur in the benign and well-studied case of smooth convex functions? As far as we know, this question has not been tackled in previous work. We show, perhaps surprisingly, that the answer crucially depends on the choice of the step size. In particular, for the range of step sizes which are known to result in monotonic convergence to an optimal value, we characterize a regime where the optimization curve will be provably convex, and a regime where the curve can be non-convex. We also extend our results to gradient flow, and to the closely-related but different question of whether the gradient norm decreases monotonically. △ Less

Submitted 2 April, 2025; v1 submitted 13 March, 2025; originally announced March 2025.

Comments: 14 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

LSEBMCL: A Latent Space Energy-Based Model for Continual Learning

Authors: Xiaodi Li, Dingcheng Li, Rujun Gao, Mahmoud Zamani, Latifur Khan

Abstract: Continual learning has become essential in many practical applications such as online news summaries and product classification. The primary challenge is known as catastrophic forgetting, a phenomenon where a model inadvertently discards previously learned knowledge when it is trained on new tasks. Existing solutions involve storing exemplars from previous classes, regularizing parameters during t… ▽ More Continual learning has become essential in many practical applications such as online news summaries and product classification. The primary challenge is known as catastrophic forgetting, a phenomenon where a model inadvertently discards previously learned knowledge when it is trained on new tasks. Existing solutions involve storing exemplars from previous classes, regularizing parameters during the fine-tuning process, or assigning different model parameters to each task. The proposed solution LSEBMCL (Latent Space Energy-Based Model for Continual Learning) in this work is to use energy-based models (EBMs) to prevent catastrophic forgetting by sampling data points from previous tasks when training on new ones. The EBM is a machine learning model that associates an energy value with each input data point. The proposed method uses an EBM layer as an outer-generator in the continual learning framework for NLP tasks. The study demonstrates the efficacy of EBM in NLP tasks, achieving state-of-the-art results in all experiments. △ Less

Submitted 9 January, 2025; originally announced January 2025.

Comments: In the 7th International Conference on Artificial Intelligence in Information and Communication (ICAIIC 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.

Measuring Statistical Evidence: A Short Report

Authors: Mahdi Zamani

Abstract: This short text tried to establish a big picture of what evidential statistics is about and how an ideal inference method should behave. Moreover, by examining shortcomings of some of the currently used methods for measuring evidence and utilizing some intuitive principles, we motivated the Relative Belief Ratio as the primary method of characterizing statistical evidence. Number of topics has bee… ▽ More This short text tried to establish a big picture of what evidential statistics is about and how an ideal inference method should behave. Moreover, by examining shortcomings of some of the currently used methods for measuring evidence and utilizing some intuitive principles, we motivated the Relative Belief Ratio as the primary method of characterizing statistical evidence. Number of topics has been omitted for the interest of this text and the reader is strongly advised to refer to (Evans, 2015) as the primary source for further readings of the subject. △ Less

Submitted 27 November, 2024; v1 submitted 25 November, 2024; originally announced November 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.

Exact Convergence rate of the subgradient method by using Polyak step size

Authors: Moslem Zamani, François Glineur

Abstract: This paper studies the last iterate of subgradient method with Polyak step size when applied to the minimization of a nonsmooth convex function with bounded subgradients. We show that the subgradient method with Polyak step size achieves a convergence rate $\mathcal{O}\left(\tfrac{1}{\sqrt[4]{N}}\right)$ in terms of the final iterate. An example is provided to show that this rate is exact and cann… ▽ More This paper studies the last iterate of subgradient method with Polyak step size when applied to the minimization of a nonsmooth convex function with bounded subgradients. We show that the subgradient method with Polyak step size achieves a convergence rate $\mathcal{O}\left(\tfrac{1}{\sqrt[4]{N}}\right)$ in terms of the final iterate. An example is provided to show that this rate is exact and cannot be improved. We introduce an adaptive Polyak step size for which the subgradient method enjoys a convergence rate $\mathcal{O}\left(\tfrac{1}{\sqrt{N}}\right)$ for the last iterate. Its convergence rate matches exactly the lower bound on the performance of any black-box method on the considered problem class. Additionally, we propose an adaptive Polyak method with a momentum term, where the step sizes are independent of the number of iterates. We establish that the algorithm also attains the optimal convergence rate. We investigate the alternating projection method. We derive a convergence rate $\left( \frac{2N }{ 2N+1 } \right)^N\tfrac{R}{\sqrt{2N+1}}$ for the last iterate, where $R$ is a bound on the distance between the initial iterate and a solution. An example is also provided to illustrate the exactness of the rate. △ Less

Submitted 21 July, 2024; originally announced July 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 the Set of Possible Minimizers of a Sum of Convex Functions

Authors: Moslem Zamani, François Glineur, Julien M. Hendrickx

Abstract: Consider a sum of convex functions, where the only information known about each individual summand is the location of a minimizer. In this work, we give an exact characterization of the set of possible minimizers of the sum. Our results cover several types of assumptions on the summands, such as smoothness or strong convexity. Our main tool is the use of necessary and sufficient conditions for int… ▽ More Consider a sum of convex functions, where the only information known about each individual summand is the location of a minimizer. In this work, we give an exact characterization of the set of possible minimizers of the sum. Our results cover several types of assumptions on the summands, such as smoothness or strong convexity. Our main tool is the use of necessary and sufficient conditions for interpolating the considered function classes, which leads to shorter and more direct proofs in comparison with previous work. We also address the setting where each summand minimizer is assumed to lie in a unit ball, and prove a tight bound on the norm of any minimizer of the sum. △ Less

Submitted 8 March, 2024; originally announced March 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.

Privacy-Preserving Financial Anomaly Detection via Federated Learning & Multi-Party Computation

Authors: Sunpreet Arora, Andrew Beams, Panagiotis Chatzigiannis, Sebastian Meiser, Karan Patel, Srinivasan Raghuraman, Peter Rindal, Harshal Shah, Yizhen Wang, Yuhang Wu, Hao Yang, Mahdi Zamani

Abstract: One of the main goals of financial institutions (FIs) today is combating fraud and financial crime. To this end, FIs use sophisticated machine-learning models trained using data collected from their customers. The output of machine learning models may be manually reviewed for critical use cases, e.g., determining the likelihood of a transaction being anomalous and the subsequent course of action.… ▽ More One of the main goals of financial institutions (FIs) today is combating fraud and financial crime. To this end, FIs use sophisticated machine-learning models trained using data collected from their customers. The output of machine learning models may be manually reviewed for critical use cases, e.g., determining the likelihood of a transaction being anomalous and the subsequent course of action. While advanced machine learning models greatly aid an FI in anomaly detection, model performance could be significantly improved using additional customer data from other FIs. In practice, however, an FI may not have appropriate consent from customers to share their data with other FIs. Additionally, data privacy regulations may prohibit FIs from sharing clients' sensitive data in certain geographies. Combining customer data to jointly train highly accurate anomaly detection models is therefore challenging for FIs in operational settings. In this paper, we describe a privacy-preserving framework that allows FIs to jointly train highly accurate anomaly detection models. The framework combines the concept of federated learning with efficient multi-party computation and noisy aggregates inspired by differential privacy. The presented framework was submitted as a winning entry to the financial crime detection track of the US/UK PETs Challenge. The challenge considered an architecture where banks hold customer data and execute transactions through a central network. We show that our solution enables the network to train a highly accurate anomaly detection model while preserving privacy of customer data. Experimental results demonstrate that use of additional customer data using the proposed approach results in improvement of our anomaly detection model's AUPRC from 0.6 to 0.7. We discuss how our framework, can be generalized to other similar scenarios. △ Less

Submitted 6 October, 2023; originally announced October 2023.

Comments: 12 pages

Exact convergence rate of the last iterate in subgradient methods

Authors: Moslem Zamani, François Glineur

Abstract: We study the convergence of the last iterate in subgradient methods applied to the minimization of a nonsmooth convex function with bounded subgradients. We first introduce a proof technique that generalizes the standard analysis of subgradient methods. It is based on tracking the distance between the current iterate and a different reference point at each iteration. Using this technique, we obt… ▽ More We study the convergence of the last iterate in subgradient methods applied to the minimization of a nonsmooth convex function with bounded subgradients. We first introduce a proof technique that generalizes the standard analysis of subgradient methods. It is based on tracking the distance between the current iterate and a different reference point at each iteration. Using this technique, we obtain the exact worst-case convergence rate for the objective accuracy of the last iterate of the projected subgradient method with either constant step sizes or constant step lengths. Tightness is shown with a worst-case instance matching the established convergence rate. We also derive the value of the optimal constant step size when performing $N$ iterations, for which we find that the last iterate accuracy is smaller than $B R \sqrt{1+\log(N)/4}/{\sqrt{N+1}}$ %$\frac{B R \log N}{\sqrt{N+1}}$ , where $B$ is a bound on the subgradient norm and $R$ is a bound on the distance between the initial iterate and a minimizer. Finally, we introduce a new optimal subgradient method that achieves the best possible last-iterate accuracy after a given number $N$ of iterations. Its convergence rate ${B R}/{\sqrt{N+1}}$ matches exactly the lower bound on the performance of any black-box method on the considered problem class. We also show that there is no universal sequence of step sizes that simultaneously achieves this optimal rate at each iteration, meaning that the dependence of the step size sequence in $N$ is unavoidable. △ Less

Submitted 20 July, 2023; originally announced July 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.

Privacy-Enhancing Technologies for Financial Data Sharing

Authors: Panagiotis Chatzigiannis, Wanyun Catherine Gu, Srinivasan Raghuraman, Peter Rindal, Mahdi Zamani

Abstract: Today, financial institutions (FIs) store and share consumers' financial data for various reasons such as offering loans, processing payments, and protecting against fraud and financial crime. Such sharing of sensitive data have been subject to data breaches in the past decade. While some regulations (e.g., GDPR, FCRA, and CCPA) help to prevent institutions from freely sharing clients' sensitive… ▽ More Today, financial institutions (FIs) store and share consumers' financial data for various reasons such as offering loans, processing payments, and protecting against fraud and financial crime. Such sharing of sensitive data have been subject to data breaches in the past decade. While some regulations (e.g., GDPR, FCRA, and CCPA) help to prevent institutions from freely sharing clients' sensitive information, some regulations (e.g., BSA 1970) require FIs to share certain financial data with government agencies to combat financial crime. This creates an inherent tension between the privacy and the integrity of financial transactions. In the past decade, significant progress has been made in building efficient privacy-enhancing technologies that allow computer systems and networks to validate encrypted data automatically. In this paper, we investigate some of these technologies to identify the benefits and limitations of each, in particular, for use in data sharing among FIs. As a case study, we look into the emerging area of Central Bank Digital Currencies (CBDCs) and how privacy-enhancing technologies can be integrated into the CBDC architecture. Our study, however, is not limited to CBDCs and can be applied to other financial scenarios with tokenized bank deposits such as cross-border payments, real-time settlements, and card payments. △ Less

Submitted 16 June, 2023; originally announced June 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

Equilibriums of extremely magnetized compact stars with force-free magnetotunnels

Authors: Koji Uryu, Shijun Yoshida, Eric Gourgoulhon, Charalampos Markakis, Kotaro Fujisawa, Antonios Tsokaros, Keisuke Taniguchi, Mina Zamani

Abstract: We present numerical solutions for stationary and axisymmetric equilibriums of compact stars associated with extremely strong magnetic fields. The interior of the compact stars is assumed to satisfy ideal magnetohydrodynamic (MHD) conditions, while in the region of negligible mass density the force-free conditions or electromagnetic vacuum are assumed. Solving all components of Einstein's equation… ▽ More We present numerical solutions for stationary and axisymmetric equilibriums of compact stars associated with extremely strong magnetic fields. The interior of the compact stars is assumed to satisfy ideal magnetohydrodynamic (MHD) conditions, while in the region of negligible mass density the force-free conditions or electromagnetic vacuum are assumed. Solving all components of Einstein's equations, Maxwell's equations, ideal MHD equations, and force-free conditions, equilibriums of rotating compact stars associated with mixed poloidal and toroidal magnetic fields are obtained. It is found that in the extreme cases the strong mixed magnetic fields concentrating in a toroidal region near the equatorial surface expel the matter and form a force-free toroidal magnetotunnel. We also introduce a new differential rotation law for computing solutions associated with force-free magnetosphere, and present other extreme models without the magnetotunnel. △ Less

Submitted 31 March, 2023; originally announced March 2023.

Comments: 13 pages, 4 figures

Convergence rate analysis of randomized and cyclic coordinate descent for convex optimization through semidefinite programming

Authors: Hadi Abbaszadehpeivasti, Etienne de Klerk, Moslem Zamani

Abstract: In this paper, we study randomized and cyclic coordinate descent for convex unconstrained optimization problems. We improve the known convergence rates in some cases by using the numerical semidefinite programming performance estimation method. As a spin-off we provide a method to analyse the worst-case performance of the Gauss-Seidel iterative method for linear systems where the coefficient matri… ▽ More In this paper, we study randomized and cyclic coordinate descent for convex unconstrained optimization problems. We improve the known convergence rates in some cases by using the numerical semidefinite programming performance estimation method. As a spin-off we provide a method to analyse the worst-case performance of the Gauss-Seidel iterative method for linear systems where the coefficient matrix is positive semidefinite with a positive diagonal. △ Less

Submitted 23 December, 2022; originally announced December 2022.

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

MechProNet: Machine Learning Prediction of Mechanical Properties in Metal Additive Manufacturing

Authors: Parand Akbari, Masoud Zamani, Amir Mostafaei

Abstract: Predicting mechanical properties in metal additive manufacturing (MAM) is essential for ensuring the performance and reliability of printed parts, as well as their suitability for specific applications. However, conducting experiments to estimate mechanical properties in MAM processes can be laborious and expensive, and they are often limited to specific materials and processes. Machine learning (… ▽ More Predicting mechanical properties in metal additive manufacturing (MAM) is essential for ensuring the performance and reliability of printed parts, as well as their suitability for specific applications. However, conducting experiments to estimate mechanical properties in MAM processes can be laborious and expensive, and they are often limited to specific materials and processes. Machine learning (ML) methods offer a more flexible and cost-effective approach to predicting mechanical properties based on processing parameters and material properties. In this study, we introduce a comprehensive framework for benchmarking ML models for predicting mechanical properties. We compiled an extensive experimental dataset from over 90 MAM articles and data sheets from a diverse range of sources, encompassing 140 different MAM data sheets. This dataset includes information on MAM processing conditions, machines, materials, and resulting mechanical properties such as yield strength, ultimate tensile strength, elastic modulus, elongation, hardness, and surface roughness. Our framework incorporates physics-aware featurization specific to MAM, adjustable ML models, and tailored evaluation metrics to construct a comprehensive learning framework for predicting mechanical properties. Additionally, we explore the Explainable AI method, specifically SHAP analysis, to elucidate and interpret the predicted values of ML models for mechanical properties. Furthermore, data-driven explicit models were developed to estimate mechanical properties based on processing parameters and material properties, offering enhanced interpretability compared to conventional ML models. △ Less

Submitted 17 March, 2024; v1 submitted 21 August, 2022; originally announced September 2022.

Journal ref: Additive Manufacturing, Volume 91, 2024, 104320, ISSN 2214-8604

Convergence rate analysis of the gradient descent-ascent method for convex-concave saddle-point problems

Authors: Moslem Zamani, Hadi Abbaszadehpeivasti, Etienne de Klerk

Abstract: In this paper, we study the gradient descent-ascent method for convex-concave saddle-point problems. We derive a new non-asymptotic global convergence rate in terms of distance to the solution set by using the semidefinite programming performance estimation method. The given convergence rate incorporates most parameters of the problem and it is exact for a large class of strongly convex-strongly c… ▽ More In this paper, we study the gradient descent-ascent method for convex-concave saddle-point problems. We derive a new non-asymptotic global convergence rate in terms of distance to the solution set by using the semidefinite programming performance estimation method. The given convergence rate incorporates most parameters of the problem and it is exact for a large class of strongly convex-strongly concave saddle-point problems for one iteration. We also investigate the algorithm without strong convexity and we provide some necessary and sufficient conditions under which the gradient descent-ascent enjoys linear convergence. △ Less

Submitted 15 September, 2022; v1 submitted 2 September, 2022; originally announced September 2022.

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

The exact worst-case convergence rate of the alternating direction method of multipliers

Authors: Moslem Zamani, Hadi Abbaszadehpeivasti, Etienne de Klerk

Abstract: Recently, semidefinite programming performance estimation has been employed as a strong tool for the worst-case performance analysis of first order methods. In this paper, we derive new non-ergodic convergence rates for the alternating direction method of multipliers (ADMM) by using performance estimation. We give some examples which show the exactness of the given bounds. We also study the linear… ▽ More Recently, semidefinite programming performance estimation has been employed as a strong tool for the worst-case performance analysis of first order methods. In this paper, we derive new non-ergodic convergence rates for the alternating direction method of multipliers (ADMM) by using performance estimation. We give some examples which show the exactness of the given bounds. We also study the linear and R-linear convergence of ADMM. We establish that ADMM enjoys a global linear convergence rate if and only if the dual objective satisfies the Polyak-Lojasiewicz (PL)inequality in the presence of strong convexity. In addition, we give an explicit formula for the linear convergence rate factor. Moreover, we study the R-linear convergence of ADMM under two new scenarios. △ Less

Submitted 24 May, 2023; v1 submitted 20 June, 2022; originally announced June 2022.

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

Collective behavior of stock prices in the time of crisis as a response to the external stimulus

Authors: Maryam Zamani, Sander Paekivi, Philipp Meyer, Holger Kantz

Abstract: We analyze the interaction between stock prices of big companies in the USA and Germany using Granger Causality. We claim that the increase in pair-wise Granger causality interaction between prices in the times of crisis is the consequence of simultaneous response of the markets to the outside events or external stimulus that is considered as a common driver to all the stocks, not a result of real… ▽ More We analyze the interaction between stock prices of big companies in the USA and Germany using Granger Causality. We claim that the increase in pair-wise Granger causality interaction between prices in the times of crisis is the consequence of simultaneous response of the markets to the outside events or external stimulus that is considered as a common driver to all the stocks, not a result of real causal predictability between the prices themselves. An alternative approach through recurrence analysis in single stock price series supports this claim. The observed patterns in the price of stocks are modelled by adding a multiplicative exogenous term as the representative for external factors to the geometric Brownian motion model for stock prices. Altogether, we can detect and model the effects of the Great Recession as a consequence of the mortgage crisis in 2007/2008 as well as the impacts of the Covid out-break in early 2020 △ Less

Submitted 9 May, 2022; originally announced May 2022.

Comments: 9 pages, 6 figures

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.

Conditions for linear convergence of the gradient method for non-convex optimization

Authors: Hadi Abbaszadehpeivasti, Etienne de Klerk, Moslem Zamani

Abstract: In this paper, we derive a new linear convergence rate for the gradient method with fixed step lengths for non-convex smooth optimization problems satisfying the Polyak-Lojasiewicz (PL) inequality. We establish that the PL inequality is a necessary and sufficient condition for linear convergence to the optimal value for this class of problems. We list some related classes of functions for which th… ▽ More In this paper, we derive a new linear convergence rate for the gradient method with fixed step lengths for non-convex smooth optimization problems satisfying the Polyak-Lojasiewicz (PL) inequality. We establish that the PL inequality is a necessary and sufficient condition for linear convergence to the optimal value for this class of problems. We list some related classes of functions for which the gradient method may enjoy linear convergence rate. Moreover, we investigate their relationship with the PL inequality. △ Less

Submitted 1 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

On Tail Triviality of Negatively Dependent Stochastic Processes

Authors: Kasra Alishahi, Milad Barzegar, Mohammadsadegh Zamani

Abstract: We prove that every negatively associated sequence of Bernoulli random variables with "summable covariances" has a trivial tail sigma-field. A corollary of this result is the tail triviality of strongly Rayleigh processes. This is a generalization of a result due to Lyons which establishes tail triviality for discrete determinantal processes. We also study the tail behavior of negatively associate… ▽ More We prove that every negatively associated sequence of Bernoulli random variables with "summable covariances" has a trivial tail sigma-field. A corollary of this result is the tail triviality of strongly Rayleigh processes. This is a generalization of a result due to Lyons which establishes tail triviality for discrete determinantal processes. We also study the tail behavior of negatively associated Gaussian and Gaussian threshold processes. We show that these processes are tail trivial though they do not in general satisfy the summable covariances property. Furthermore, we construct negatively associated Gaussian threshold vectors that are not strongly Rayleigh. This identifies a natural family of negatively associated measures that is not a subset of the class of strongly Rayleigh measures. △ Less

Submitted 22 May, 2022; v1 submitted 8 March, 2022; originally announced March 2022.

Comments: 11 pages

On a notion of entropy for reachability properties

Authors: Mahendra Singh Tomar, Majid Zamani

Abstract: In this work, we introduce a notion of reachability entropy to characterize the smallest data rate which is sufficient enough to enforce reach-while-stay specification. We also define data rates of coder-controllers that can enforce this specification in finite time. Then, we establish the data-rate theorem which states that the reachability entropy is a tight lower bound of the data rates that al… ▽ More In this work, we introduce a notion of reachability entropy to characterize the smallest data rate which is sufficient enough to enforce reach-while-stay specification. We also define data rates of coder-controllers that can enforce this specification in finite time. Then, we establish the data-rate theorem which states that the reachability entropy is a tight lower bound of the data rates that allow satisfaction of the reach-while-stay specification. For a system which is related to an another system under feedback refinement relation, we show that the entropy of the former will not be larger than that of the latter. We also provide a procedure to numerically compute an upper bound of the reachability entropy for discrete-time control systems by leveraging their finite abstractions. Finally, we present some examples to demonstrate the effectiveness of the proposed results. △ Less

Submitted 20 June, 2022; v1 submitted 1 March, 2022; originally announced March 2022.

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.

A small-gain theory for infinite networks via infinite-dimensional gain operators

Authors: Christoph Kawan, Majid Zamani

Abstract: In this paper, we develop a new approach to study gain operators built from the interconnection gains of infinite networks of dynamical systems. Our focus is on the construction of paths of strict decay which are used for building Lyapunov functions for the network and thus proving various stability properties, including input-to-state stability. Our approach is based on the study of an augmented… ▽ More In this paper, we develop a new approach to study gain operators built from the interconnection gains of infinite networks of dynamical systems. Our focus is on the construction of paths of strict decay which are used for building Lyapunov functions for the network and thus proving various stability properties, including input-to-state stability. Our approach is based on the study of an augmented gain operator whose fixed points are precisely the points of decay for the original gain operator. We show that plenty of such fixed points exist under a uniform version of the no-joint-increase condition. Using these fixed points to construct a path of strict decay, in general, requires specific dynamical properties of associated monotone operators. For particular types of gain operators such as max-type operators and subadditive operators, these properties follow from uniform global asymptotic stability of the system induced by the original gain operator. This is consistent with former results in the literature which can readily be recovered from our theory. △ Less

Submitted 10 December, 2021; originally announced December 2021.

MSC Class: 37B25; 37L15; 93D05; 93A15

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.