arXiv subjects

Sadegh Soudjani

Publications and source records attributed to Sadegh Soudjani.

At least 55 records · Page 3Linked to original sources

arXiv2025

Robust Control of Uncertain Switched Affine Systems via Scenario Optimization

Switched affine systems are often used to model and control complex dynamical systems that operate in multiple modes. However, uncertainties in the system matrices can challenge their stability and performance. This paper introduces a new approach for designing switching control laws for uncertain switched affine systems using data-driven scenario optimization. Instead of relaxing invariant sets, our method creates smaller invariant sets with quadratic Lyapunov functions through scenario-based optimization, effectively reducing chattering effects and regulation error. The framework ensures robustness against parameter uncertainties while improving accuracy. We validate our method with applications in multi-objective interval Markov decision processes and power electronic converters, demonstrating its effectiveness.

eess.SY↗

arXiv2025

Logic-based Resilience Computation of Power Systems Against Frequency Requirements

Incorporating renewable energy sources into modern power grids has significantly decreased system inertia, which has raised concerns about power system vulnerability to disturbances and frequency instability. The conventional methods for evaluating transient stability by bounding frequency deviations are often conservative and may not accurately reflect real-world conditions and operational constraints. To address this, we propose a framework for assessing the resilience of power systems against disturbances while adhering to realistic operational frequency constraints. Our approach leverages the Lure system representation of power system dynamics and Signal Temporal Logic (STL) to capture the essential frequency response requirements set by grid operators. This enables us to translate frequency constraints into formal robustness semantics. We then formulate an optimization problem to identify the maximum disturbance that the system can withstand without violating these constraints. The resulting optimization is translated into a scenario optimization while addressing the uncertainty in the obtained solution. The proposed methodology has been simulated on the Single Machine Infinite Bus case study and 9-Bus IEEE benchmark system, demonstrating its effectiveness in assessing resilience across various operating conditions and delivering promising results.

eess.SY↗

arXiv2025

Robust Model Predictive Control for Aircraft Intent-Aware Collision Avoidance

This paper presents the use of robust model predictive control for the design of an intent-aware collision avoidance system for multi-agent aircraft engaged in horizontal maneuvering scenarios. We assume that information from other agents is accessible in the form of waypoints or destinations. Consequently, we consider that other agents follow their optimal Dubin's path--a trajectory that connects their current state to their intended state--while accounting for potential uncertainties. We propose using scenario tree model predictive control as a robust approach that demonstrates computational efficiency. We demonstrate that the proposed method can easily integrate intent information and offer a robust scheme that handles different uncertainties. The method is illustrated through simulation results.

eess.SY↗

arXiv2025

Intent-Aware MPC for Aircraft Detect-and-Avoid with Response Delay: A Comparative Study with ACAS Xu

In this paper, we propose an intent-aware Model Predictive Control (MPC) approach for the remain-well-clear (RWC) functionality of a multi-agent aircraft detect-and-avoid (DAA) system and compare its performance with the standardized Airborne Collision Avoidance System Xu (ACAS Xu). The aircraft system is modeled as a linear system for horizontal maneuvering, with advisories on the rate of turn as the control input. Both deterministic and stochastic time delays are considered to account for the lag between control guidance issuance and the response of the aircraft. The capability of the MPC scheme in producing an optimal control profile over the entire horizon is used to mitigate the impact of the delay. We compare the proposed MPC method with ACAS Xu using various evaluation metrics, including loss of DAA well-clear percentage, near mid-air collision percentage, horizontal miss distance, and additional flight distance across different encounter scenarios. It is shown that the MPC scheme achieves better evaluation metrics than ACAS Xu for both deterministic and stochastic scenarios.

eess.SY↗

arXiv2025

Data-Driven Distributionally Robust Control for Interacting Agents under Logical Constraints

In this paper, we propose a distributionally robust control synthesis for an agent with stochastic dynamics that interacts with other agents under uncertainties and constraints expressed by signal temporal logic (STL). We formulate the control synthesis as a chance-constrained program (CCP) with STL specifications that must be satisfied with high probability under all uncertainty tubes induced by the other agents. To tackle the CCP, we propose two methods based on concentration of measure (CoM) theory and conditional value at risk (CVaR) and compare the required assumptions and resulting optimizations. These approaches convert the CCP into an expectation-constrained program (ECP), which is simpler to solve than the original CCP. To estimate the expectation using a finite set of observed data, we adopt a distributionally robust optimization (DRO) approach. The underlying DRO can be approximated as a robust data-driven optimization that provides a probabilistic under-approximation to the original ECP, where the probability depends on the number of samples. Therefore, under feasibility, the original STL constraints are satisfied with two layers of designed confidence: the confidence of the chance constraint and the confidence of the approximated data-driven optimization, which depends on the number of samples. We then provide details on solving the resulting robust data-driven optimization numerically. Finally, we compare the two proposed approaches through case studies.

eess.SY↗

arXiv2024

Logic-based Knowledge Awareness for Autonomous Agents in Continuous Spaces

This paper presents a step towards a formal controller design method for autonomous agents based on knowledge awareness to improve decision-making. Our approach is to first create an organized repository of information (a knowledge base) for autonomous agents which can be accessed and then translated into temporal specifications. Secondly, to develop a controller with formal guarantees that meets a combination of mission-specific objective and the specification from the knowledge base, we utilize an abstraction-based controller design (ABCD) approach, capable of managing both nonlinear dynamics and temporal requirements. Unlike the conventional offline ABCD approach, our method dynamically updates the controller whenever the knowledge base prompts changes in the specifications. A three-dimensional nonlinear car model navigating an urban road scenario with traffic signs and obstacles is considered for validation. Results show the effectiveness of the method in guiding the autonomous agents to the target while complying with the knowledge base and the mission-specific objective.

eess.SY↗

arXiv2024

SymAware: A Software Development Framework for Trustworthy Multi-Agent Systems with Situational Awareness

Developing trustworthy multi-agent systems for practical applications is challenging due to the complicated communication of situational awareness (SA) among agents. This paper showcases a novel efficient and easy-to-use software framework for multi-agent simulation, named SymAware which provides a rich set of predefined data structures to compute, store, and communicate SA for agents. It also provides an abstract interface for the agents to compute their control inputs taking into account the awareness of the situation, knowledge, and risk of surrounding agents. Besides, utilizing a cluster of specialized components, SymAware hides the heavy computation of physical rendering and communication interfacing of simulation engines behind the control threads, resulting in high implementation efficiency in bridging the gap between conceptual prototyping and practical applications. Three multi-agent case studies are used to validate the efficacy and efficiency of this software framework.

cs.RO↗

arXiv2024

Distributionally Robust Control for Chance-Constrained Signal Temporal Logic Specifications

We consider distributionally robust optimal control of stochastic linear systems under signal temporal logic (STL) chance constraints when the disturbance distribution is unknown. By assuming that the underlying predicate functions are Lipschitz continuous and the noise realizations are drawn from a distribution having a concentration of measure property, we first formulate the underlying chance-constrained control problem as stochastic programming with constraints on expectations and propose a solution using a distributionally robust approach based on the Wasserstein metric. We show that by choosing a proper Wasserstein radius, the original chance-constrained optimization can be satisfied with a user-defined confidence level. A numerical example illustrates the efficacy of the method.

eess.SY↗

arXiv2024

Verification of Quantum Circuits through Discrete-Time Barrier Certificates

Current methods for verifying quantum computers are predominately based on interactive or automatic theorem provers. Considering that quantum computers are dynamical in nature, this paper employs and extends the concepts from the verification of dynamical systems to verify properties of quantum circuits. Our main contribution is to propose k-inductive barrier certificates over complex variables and show how to compute them using Hermitian Sum of Squares optimization. We apply this new technique to verify properties of different quantum circuits.

quant-ph↗

arXiv2024

Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

To advance formal verification of stochastic systems against temporal logic requirements for handling unknown dynamics, researchers have been designing data-driven approaches inspired by breakthroughs in the underlying machine learning techniques. As one promising research direction, abstraction-based solutions based on Gaussian process (GP) regression have become popular for their ability to learn a representation of the latent system from data with a quantified error. Results obtained based on this model are then translated to the true system via various methods. In a recent publication, GPs using a so-called binary-tree kernel have demonstrated a polynomial speedup w.r.t. the size of the data compared to their vanilla version, outcompeting all existing sparse GP approximations. Incidentally, the resulting binary-tree Gaussian process (BTGP) is characteristic for its piecewise-constant posterior mean and covariance functions, naturally abstracting the input space into discrete partitions. In this paper, we leverage this natural abstraction of the BTGP for formal verification, eliminating the need for cumbersome abstraction and error quantification procedures. We show that the BTGP allows us to construct an interval Markov chain model of the unknown system with a speedup that is polynomial w.r.t. the size of the abstraction compared to alternative approaches. We provide a delocalized error quantification via a unified formula even when the true dynamics do not live in the function space of the BTGP. This allows us to compute upper and lower bounds on the probability of satisfying reachability specifications that are robust to both aleatoric and epistemic uncertainties.

cs.LO↗

arXiv2024

Specification-guided temporal logic control for stochastic systems: a multi-layered approach

Designing controllers to satisfy temporal requirements has proven to be challenging for dynamical systems that are affected by uncertainty. This is mainly due to the states evolving in a continuous uncountable space, the stochastic evolution of the states, and infinite-horizon temporal requirements on the system evolution, all of which makes closed-form solutions generally inaccessible. A promising approach for designing provably correct controllers on such systems is to utilize the concept of abstraction, which is based on building simplified abstract models that can be used to approximate optimal controllers with provable closeness guarantees. The available abstraction-based methods are further divided into discretization-based approaches that build a finite abstract model by discretizing the continuous space of the system, and discretization-free approaches that work directly on the continuous state space without the need for building a finite space. To reduce the conservatism in the sub-optimality of the designed controller originating from the abstraction step, this paper develops an approach that naturally has the flexibility to combine different abstraction techniques from the aforementioned classes and to combine the same abstraction technique with different parameters. First, we develop a multi-layered discretization-based approach with variable precision by combining abstraction layers with different precision parameters. Then, we exploit the advantages of both classes of abstraction-based methods by extending this multi-layered approach guided by the specification to combinations of layers with respectively discretization-based and discretization-free abstractions. We achieve an efficient implementation that is less conservative and improves the computation time and memory usage. We illustrate the benefits of the proposed multi-layered approach on several case studies.

eess.SY↗

arXiv2024

T-Count Optimizing Genetic Algorithm for Quantum State Preparation

Quantum state preparation is a crucial process within numerous quantum algorithms, and the need for efficient initialization of quantum registers is ever increasing as demand for useful quantum computing grows. The problem arises as the number of qubits to be initialized grows, the circuits required to implement the desired state also exponentially increase in size leading to loss of fidelity to noise. This is mainly due to the susceptibility to environmental effects of the non-Clifford T gate, whose use should thus be reduced as much as possible. In this paper, we present and utilize a genetic algorithm for state preparation circuits consisting of gates from the Clifford + T gate set and optimize them in T-Count as to reduce the impact of noise. Whilst the method presented here does not always produce the most accurate circuits in terms of fidelity, it can generate high-fidelity, non-trivial quantum states such as quantum Fourier transform states. In addition, our algorithm does automatically generate fault tolerantly implementable solutions where the number of the most error prone components is reduced. We present an evaluation of the algorithm when trialed against preparing random, Poisson probability distribution, W, GHZ, and quantum Fourier transform states. We also experimentally demonstrate the scalability issues as qubit count increases, which highlights the need for further optimization of the search process.

quant-ph↗

arXiv2024

Automated Verification of Silq Quantum Programs using SMT Solvers

We present SilVer (Silq Verification), an automated tool for verifying behaviors of quantum programs written in Silq, which is a high-level programming language for quantum computing. The goal of the verification is to ensure correctness of the Silq quantum program against user-defined specifications using SMT solvers. We introduce a programming model that is based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations, allowing for control of quantum operations using both classical and quantum conditions. Additionally, users can employ measurement flags within the specification to easily specify conditions that measurement results require to satisfy for being a valid behavior. We provide case studies on the verification of generating entangled states and multiple oracle-based algorithms.

quant-ph↗

arXiv2024

Vagus nerve stimulation: Laying the groundwork for predictive network-based computer models

Vagus Nerve Stimulation (VNS) is an established palliative treatment for drug resistant epilepsy. While effective for many patients, its mechanism of action is incompletely understood. Predicting individuals' response, or optimum stimulation parameters, is challenging. Computational modelling has informed other problems in epilepsy but, to our knowledge, has not been applied to VNS. We started with an established, four-population neural mass model (NMM), capable of reproducing the seizure-like dynamics of a thalamocortical circuit. We extended this to include 18 further neural populations, representing nine other brain regions relevant to VNS, with connectivity based on existing literature. We modelled stimulated afferent vagal fibres as projecting to the nucleus tractus solitarius (NTS), which receives input from the vagus nerve in vivo. Bifurcation analysis of a deterministic version of the model showed higher background NTS input made the model monostable at a fixed point (FP), representing normal activity, while lower inputs produce bistability between the FP and a limit cycle (LC), representing the seizure state. Adding noise produced transitions between seizure and normal states. This stochastic model spent decreasing time in the seizure state with increasing background NTS input, until seizures were abolished, consistent with the deterministic model. Simulated VNS stimulation, modelled as a 30 Hz square wave, was summed with the background input to the NTS and was found to reduce total seizure duration in a dose-dependent manner, similar to expectations in vivo. We have successfully produced an in silico model of VNS in epilepsy, capturing behaviour seen in vivo. This may aid understanding therapeutic mechanisms of VNS in epilepsy and provides a starting point to (i) determine which patients might respond best to VNS, and (ii) optimise individuals' treatments.

q-bio.NC↗

arXiv2024

Rare Collision Risk Estimation of Autonomous Vehicles with Multi-Agent Situation Awareness

This paper offers a formal framework for the rare collision risk estimation of autonomous vehicles (AVs) with multi-agent situation awareness, affected by different sources of noise in a complex dynamic environment. In our proposed setting, the situation awareness is considered for one of the ego vehicles by aggregating a range of diverse information gathered from other vehicles into a vector. We model AVs equipped with the situation awareness as general stochastic hybrid systems (GSHS) and assess the probability of collision in a lane-change scenario where two self-driving vehicles simultaneously intend to switch lanes into a shared one, while utilizing the time-to-collision measure for decision-making as required. Due to the substantial data requirements of simulation-based methods for the rare collision risk estimation, we leverage a multi-level importance splitting technique, known as interacting particle system-based estimation with fixed assignment splitting (IPS-FAS). This approach allows us to estimate the probability of a rare event by employing a group of interacting particles. Specifically, each particle embodies a system trajectory and engages with others through resampling and branching, focusing computational resources on trajectories with the highest probability of encountering the rare event. The effectiveness of our proposed approach is demonstrated through an extensive simulation of a lane-change scenario.

eess.SY↗

arXiv2024

Temporal Logic Resilience for Dynamical Systems

We consider the notion of resilience for cyber-physical systems, that is, the ability of the system to withstand adverse events while maintaining acceptable functionality. We use finite temporal logic to express the requirements on the acceptable functionality and define the resilience metric as the maximum disturbance under which the system satisfies the temporal requirements. We fix a parameterized template for the set of disturbances and form a robust optimization problem under the system dynamics and the temporal specifications to find the maximum value of the parameter. Additionally, we introduce two novel classes of specifications: closed and convex finite temporal logics specifications, offering a comprehensive analysis of the resilience metric within these specific frameworks. From a computational standpoint, we present an exact solution for linear systems and exact-time reachability and finite-horizon safety, complemented by an approximate solution for finite-horizon reachability. Extending our findings to nonlinear systems, we leverage linear approximations and SMT-based approaches to offer viable computational methodologies. The theoretical results are demonstrated on the temperature regulation of buildings, adaptive cruise control and DC motors.

eess.SY↗

arXiv2024

Safe Reach Set Computation via Neural Barrier Certificates

We present a novel technique for online safety verification of autonomous systems, which performs reachability analysis efficiently for both bounded and unbounded horizons by employing neural barrier certificates. Our approach uses barrier certificates given by parameterized neural networks that depend on a given initial set, unsafe sets, and time horizon. Such networks are trained efficiently offline using system simulations sampled from regions of the state space. We then employ a meta-neural network to generalize the barrier certificates to state space regions that are outside the training set. These certificates are generated and validated online as sound over-approximations of the reachable states, thus either ensuring system safety or activating appropriate alternative actions in unsafe scenarios. We demonstrate our technique on case studies from linear models to nonlinear control-dependent models for online autonomous driving scenarios.

eess.SY↗

arXiv2024

Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings

Algorithmic verification of realistic systems to satisfy safety and other temporal requirements has suffered from poor scalability of the employed formal approaches. To design systems with rigorous guarantees, many approaches still rely on exact models of the underlying systems. Since this assumption can rarely be met in practice, models have to be inferred from measurement data or are bypassed completely. Whilst former usually requires the model structure to be known a-priori and immense amounts of data to be available, latter gives rise to a plethora of restrictive mathematical assumptions about the unknown dynamics. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates, which can guarantee safety of the system, and learn the certificate directly from a compact set of system trajectories. We use conditional mean embeddings to embed data from the system into a reproducing kernel Hilbert space (RKHS) and construct an RKHS ambiguity set that can be inflated to robustify the result w.r.t. a set of plausible transition kernels. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope. Our approach lifts the need for restrictive assumptions on the system dynamics and uncertainty, and suggests an improvement in the sample complexity of verifying the safety of a system on a tested case study compared to a state-of-the-art approach.

eess.SY↗