arXiv subjects

Sadegh Soudjani

Publications and source records attributed to Sadegh Soudjani.

At least 73 records · Page 4Linked to original sources

arXiv2024

Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation

A novel data-driven method for formal verification is proposed to study complex systems operating in safety-critical domains. The proposed approach is able to formally verify discrete-time stochastic dynamical systems against temporal logic specifications only using observation samples and without the knowledge of the model, and provide a probabilistic guarantee on the satisfaction of the specification. We first propose the theoretical results for using non-parametric estimation to estimate an asymptotic upper bound for the \emph{Lipschitz constant} of the stochastic system, which can determine a finite abstraction of the system. Our results prove that the asymptotic convergence rate of the estimation is $O(n^{-\frac{1}{3+d}})$, where $d$ is the dimension of the system and $n$ is the data scale. We then construct interval Markov decision processes using two different data-driven methods, namely non-parametric estimation and empirical estimation of transition probabilities, to perform formal verification against a given temporal logic specification. Multiple case studies are presented to validate the effectiveness of the proposed methods.

eess.SY↗

arXiv2024

Awareness in robotics: An early perspective from the viewpoint of the EIC Pathfinder Challenge "Awareness Inside''

Consciousness has been historically a heavily debated topic in engineering, science, and philosophy. On the contrary, awareness had less success in raising the interest of scholars in the past. However, things are changing as more and more researchers are getting interested in answering questions concerning what awareness is and how it can be artificially generated. The landscape is rapidly evolving, with multiple voices and interpretations of the concept being conceived and techniques being developed. The goal of this paper is to summarize and discuss the ones among these voices connected with projects funded by the EIC Pathfinder Challenge called ``Awareness Inside'', a nonrecurring call for proposals within Horizon Europe designed specifically for fostering research on natural and synthetic awareness. In this perspective, we dedicate special attention to challenges and promises of applying synthetic awareness in robotics, as the development of mature techniques in this new field is expected to have a special impact on generating more capable and trustworthy embodied systems.

cs.RO↗

arXiv2024

Bayesian Formal Synthesis of Unknown Systems via Robust Simulation Relations

This paper addresses the problem of data-driven computation of controllers that are correct by design for safety-critical systems and can provably satisfy (complex) functional requirements. With a focus on continuous-space stochastic systems with parametric uncertainty, we propose a two-stage approach that decomposes the problem into a learning stage and a robust formal controller synthesis stage. The first stage utilizes available Bayesian regression results to compute robust credible sets for the true parameters of the system. For the second stage, we introduce methods for systems subject to both stochastic and parametric uncertainties. We provide simulation relations for enabling correct-by-design control refinement that are founded on coupling uncertainties of stochastic systems via sub-probability measures. The presented relations are essential for constructing abstract models that are related to not only one model but to a set of parameterized models. The results are demonstrated on three case studies, including a nonlinear and a high-dimensional system.

eess.SY↗

arXiv2023

Assume-Guarantee Reinforcement Learning

We present a modular approach to \emph{reinforcement learning} (RL) in environments consisting of simpler components evolving in parallel. A monolithic view of such modular environments may be prohibitively large to learn, or may require unrealizable communication between the components in the form of a centralized controller. Our proposed approach is based on the assume-guarantee paradigm where the optimal control for the individual components is synthesized in isolation by making \emph{assumptions} about the behaviors of neighboring components, and providing \emph{guarantees} about their own behavior. We express these \emph{assume-guarantee contracts} as regular languages and provide automatic translations to scalar rewards to be used in RL. By combining local probabilities of satisfaction for each component, we provide a lower bound on the probability of satisfaction of the complete system. By solving a Markov game for each component, RL can produce a controller for each component that maximizes this lower bound. The controller utilizes the information it receives through communication, observations, and any knowledge of a coarse model of other agents. We experimentally demonstrate the efficiency of the proposed approach on a variety of case studies.

cs.LG↗

arXiv2023

Using Knowledge Awareness to improve Safety of Autonomous Driving

We present a method, which incorporates knowledge awareness into the symbolic computation of discrete controllers for reactive cyber physical systems, to improve decision making about the unknown operating environment under uncertain/incomplete inputs. Assuming an abstract model of the system and the environment, we translate the knowledge awareness of the operating context into linear temporal logic formulas and incorporate them into the system specifications to synthesize a controller. The knowledge base is built upon an ontology model of the environment objects and behavioural rules, which includes also symbolic models of partial input features. The resulting symbolic controller support smoother, early reactions, which improves the security of the system over existing approaches based on incremental symbolic perception. A motion planning case study for an autonomous vehicle has been implemented to validate the approach, and presented results show significant improvements with respect to safety of state-of-the-art symbolic controllers for reactive systems.

eess.SY↗

arXiv2023

Generalized Stochastic Dynamic Aggregative Game for Demand-Side Management in Microgrids with Shared Battery

In this paper, we focus on modeling and analysis of demand-side management in a microgrid where agents utilize grid energy and a shared battery charged by renewable energy sources. We model the problem as a generalized stochastic dynamic aggregative game with chance constraints that capture the effects of uncertainties in the renewable generation and agents' demands. Computing the solution of the game is a complex task due to probabilistic and coupling constraints among the agents through the state of charge of the shared battery. We investigate the Nash equilibrium of this game under uncertainty considering both the uniqueness of the solution and the effect of uncertainty on the solution. Simulation results demonstrate that the presented stochastic method is superior to deterministic methods.

eess.SY↗

arXiv2023

Safety Barrier Certificates for Stochastic Control Systems with Wireless Communication Networks

This work is concerned with a formal approach for safety controller synthesis of stochastic control systems with both process and measurement noises while considering wireless communication networks between sensors, controllers, and actuators. The proposed scheme is based on control barrier certificates (CBC), which allows us to provide safety certifications for wirelessly-connected stochastic control systems. Despite the available literature on designing control barrier certificates, there has been unfortunately no consideration of wireless communication networks to capture potential packet losses and end-to-end delays, which is absolutely crucial in safety-critical real-world applications. In our proposed setting, the key objective is to construct a control barrier certificate together with a safety controller while providing a lower bound on the satisfaction probability of the safety property over a finite time horizon. We propose a systematic approach in the form of sum-of-squares optimization and matrix inequalities for the synthesis of CBC and its associated controller. We demonstrate the efficacy of our approach on a permanent magnet synchronous motor. For the application of automotive electric steering under a wireless communication network, we design a CBC together with a safety controller to maintain the electrical current of the motor in a safe set within a finite time horizon while providing a formal probabilistic guarantee.

eess.SY↗

arXiv2023

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

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.

eess.SY↗

arXiv2023

Verifying the Unknown: Correct-by-Design Control Synthesis for Networks of Stochastic Uncertain Systems

In this paper, we present an approach for designing correct-by-design controllers for cyber-physical systems composed of multiple dynamically interconnected uncertain systems. We consider networked discrete-time uncertain nonlinear systems with additive stochastic noise and model parametric uncertainty. Such settings arise when multiple systems interact in an uncertain environment and only observational data is available. We address two limitations of existing approaches for formal synthesis of controllers for networks of uncertain systems satisfying complex temporal specifications. Firstly, whilst existing approaches rely on the stochasticity to be Gaussian, the heterogeneous nature of composed systems typically yields a more complex stochastic behavior. Secondly, exact models of the systems involved are generally not available or difficult to acquire. To address these challenges, we show how abstraction-based control synthesis for uncertain systems based on sub-probability couplings can be extended to networked systems. We design controllers based on parameter uncertainty sets identified from observational data and approximate possibly arbitrary noise distributions using Gaussian mixture models whilst quantifying the incurred stochastic coupling. Finally, we demonstrate the effectiveness of our approach on a nonlinear package delivery case study with a complex specification, and a platoon of cars.

eess.SY↗

arXiv2023

Verification of Quantum Systems using Barrier Certificates

Various techniques have been used in recent years for verifying quantum computers, that is, for determining whether a quantum computer/system satisfies a given formal specification of correctness. Barrier certificates are a recent novel concept developed for verifying properties of dynamical systems. In this article, we investigate the usage of barrier certificates as a means for verifying behaviours of quantum systems. To do this, we extend the notion of barrier certificates from real to complex variables. We then develop a computational technique based on linear programming to automatically generate polynomial barrier certificates with complex variables taking real values. Finally, we apply our technique to several simple quantum systems to demonstrate their usage.

quant-ph↗

arXiv2023

Formal Control of New England 39-Bus Test System: An Assume-Guarantee Approach

This work is concerned with an assume-guarantee approach to compositionally control a New England 39-bus Test System (NETS). The proposed scheme is based on the new notion of robust simulation functions with disturbance refinement alongside the composition of multiple subsystems to tackle the difficulties associated with scalability, also known as the curse of dimensionality. In our proposed setting, we approximate concrete subsystems with abstractions that have lower dimensions (a.k.a. reduced-order models) while providing mathematical guarantees on controller synthesis through the quantification of an upper bound on the closeness between output trajectories of original systems and their abstractions. We propose two control methods to provide guarantees for NETS: one using the principle of interconnected synchronous machines and another considering the power flows in the network between neighbouring subsystems.

eess.SY↗

arXiv2023

Neural Abstraction-Based Controller Synthesis and Deployment

Abstraction-based techniques are an attractive approach for synthesizing correct-by-construction controllers to satisfy high-level temporal requirements. A main bottleneck for successful application of these techniques is the memory requirement, both during controller synthesis and in controller deployment. We propose memory-efficient methods for mitigating the high memory demands of the abstraction-based techniques using neural network representations. To perform synthesis for reach-avoid specifications, we propose an on-the-fly algorithm that relies on compressed neural network representations of the forward and backward dynamics of the system. In contrast to usual applications of neural representations, our technique maintains soundness of the end-to-end process. To ensure this, we correct the output of the trained neural network such that the corrected output representations are sound with respect to the finite abstraction. For deployment, we provide a novel training algorithm to find a neural network representation of the synthesized controller and experimentally show that the controller can be correctly represented as a combination of a neural network and a look-up table that requires a substantially smaller memory. We demonstrate experimentally that our approach significantly reduces the memory requirements of abstraction-based methods. For the selected benchmarks, our approach reduces the memory requirements respectively for the synthesis and deployment by a factor of $1.31\times 10^5$ and $7.13\times 10^3$ on average, and up to $7.54\times 10^5$ and $3.18\times 10^4$. Although this reduction is at the cost of increased off-line computations to train the neural networks, all the steps of our approach are parallelizable and can be implemented on machines with higher number of processing units to reduce the required computational time.

eess.SY↗

arXiv2023

SySCoRe: Synthesis via Stochastic Coupling Relations

We present SySCoRe, a MATLAB toolbox that synthesizes controllers for stochastic continuous-state systems to satisfy temporal logic specifications. Starting from a system description and a co-safe temporal logic specification, SySCoRe provides all necessary functions for synthesizing a robust controller and quantifying the associated formal robustness guarantees. It distinguishes itself from other available tools by supporting nonlinear dynamics, complex co-safe temporal logic specifications over infinite horizons and model-order reduction. To achieve this, SySCoRe generates a finite-state abstraction of the provided model and performs probabilistic model checking. Then, it establishes a probabilistic coupling to the original stochastic system encoded in an approximate simulation relation, based on which a lower bound on the satisfaction probability is computed. SySCoRe provides non-trivial lower bounds for infinite-horizon properties and unbounded disturbances since its computed error does not grow linearly in the horizon of the specification. It exploits a tensor representation to facilitate the efficient computation of transition probabilities. We showcase these features on several benchmarks and compare the performance of the tool with existing tools.

eess.SY↗

arXiv2023

Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness

We consider fixpoint algorithms for two-player games on graphs with $ω$-regular winning conditions, where the environment is constrained by a strong transition fairness assumption. Strong transition fairness is a widely occurring special case of strong fairness, which requires that any execution is strongly fair with respect to a specified set of live edges: whenever the source vertex of a live edge is visited infinitely often along a play, the edge itself is traversed infinitely often along the play as well. We show that, surprisingly, strong transition fairness retains the algorithmic characteristics of the fixpoint algorithms for $ω$-regular games -- the new algorithms have the same alternation depth as the classical algorithms but invoke a new type of predecessor operator. For Rabin games with $k$ pairs, the complexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which is independent of the number of live edges in the strong transition fairness assumption. Further, we show that GR(1) specifications with strong transition fairness assumptions can be solved with a 3-nested fixpoint algorithm, same as the usual algorithm. In contrast, strong fairness necessarily requires increasing the alternation depth depending on the number of fairness assumptions. We get symbolic algorithms for (generalized) Rabin, parity and GR(1) objectives under strong transition fairness assumptions as well as a direct symbolic algorithm for qualitative winning in stochastic $ω$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improving the state of the art. Finally, we have implemented a BDD-based synthesis engine based on our algorithm. We show on a set of synthetic and real benchmarks that our algorithm is scalable, parallelizable, and outperforms previous algorithms by orders of magnitude.

cs.FL↗

arXiv2022

Formal Verification of Quantum Programs: Theory, Tools and Challenges

Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backed up by the increase of research in the field. Significant efforts are being made to improve the reliability of quantum hardware and to develop suitable software to program quantum computers. In contrast, the verification of quantum programs has received relatively less attention. Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware. Research into creating verification frameworks for quantum programs has seen recent development, with a variety of tools implemented using a collection of theoretical ideas. This survey aims to be a short introduction into the area of formal verification of quantum programs, bringing together theory and tools developed to date. Further, this survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.

cs.LO↗

arXiv2022

Correct-by-Design Control of Parametric Stochastic Systems

This paper addresses the problem of computing controllers that are correct by design for safety-critical systems and can provably satisfy (complex) functional requirements. We develop new methods for models of systems subject to both stochastic and parametric uncertainties. We provide for the first time novel simulation relations for enabling correct-by-design control refinement, that are founded on coupling uncertainties of stochastic systems via sub-probability measures. Such new relations are essential for constructing abstract models that are related to not only one model but to a set of parameterized models. We provide theoretical results for establishing this new class of relations and the associated closeness guarantees for both linear and nonlinear parametric systems with additive Gaussian uncertainty. The results are demonstrated on a linear model and the nonlinear model of the Van der Pol Oscillator.

eess.SY↗

arXiv2022

Symbolic Control for Stochastic Systems via Finite Parity Games

We consider the problem of computing the maximal probability of satisfying an omega-regular specification for stochastic nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we show that a lower bound on this probability can be obtained by (I) computing an under-approximation of the qualitative winning region, i.e., states from which the parity condition can be enforced almost surely, and (II) computing the maximal probability of reaching this qualitative winning region. The heart of our approach is a technique to symbolically compute the under-approximation of the qualitative winning region in step (I) via a finite-state abstraction of the original system as a 2.5-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We prove that the winning set in the abstract 2.5-player game induces an under-approximation of the qualitative winning region in the original synthesis problem, along with a policy to solve it. By combining these contributions with (a) a symbolic fixpoint algorithm to solve 2.5-player games and (b) existing techniques for reachability policy synthesis in stochastic nonlinear systems, we get an abstraction-based algorithm for finding a lower bound on the maximal satisfaction probability. We have implemented the abstraction-based algorithm in Mascot-SDS (Majumdar et al., 2020), where we combined the outlined abstraction step with our recent tool FairSyn. We evaluated our implementation on the nonlinear model of a perturbed bistable switch from the literature. We outperform a recently proposed tool for solving this problem by a large margin.

eess.SY↗

arXiv2022

Safety Barrier Certificates for Stochastic Hybrid Systems

This work is concerned with the safety controller synthesis of stochastic hybrid systems, in which continuous evolutions are described by stochastic differential equations with both Brownian motions and Poisson processes, and instantaneous jumps are governed by stochastic difference equations with additive noises. Our proposed framework leverages the notion of control barrier certificates (CBC), as a discretization-free approach, to synthesize safety controllers for stochastic hybrid systems while providing safety guarantees in finite time horizons. In our proposed scheme, we first provide an augmented framework to characterize each stochastic hybrid system containing continuous evolutions and instantaneous jumps with a unified system covering both scenarios. We then introduce an augmented control barrier certificate (ACBC) for augmented systems and propose sufficient conditions to construct an ACBC based on CBC of original hybrid systems. By utilizing the constructed ACBC, we quantify upper bounds on the probability that the stochastic hybrid system reaches certain unsafe regions in a finite time horizon. The proposed approach is verified over a nonlinear case study.

eess.SY↗