BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Abolfazl Lavaei

Abolfazl Lavaei contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
eess.SYSystems and ControlLogic in Computer ScienceMachine LearningArtificial Intelligencemath.OC

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
15works
0followers
6topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

15 published item(s)

preprint2026arXiv

k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics

While conventional (k=1) discrete-time barrier certificate conditions impose strict safety constraints by requiring the function to be non-increasing at every step, k-inductive barrier certificates relax this by allowing a temporary increase -- up to k-1 times, each within a threshold $ε$ -- while maintaining overall safety, and improving flexibility. This paper leverages neural networks and constructs k-inductive neural barrier certificates (k-NBCs) for (partially) unknown nonlinear systems. While neural networks offer scalability in the design process, they lack formal guarantees, requiring additional approaches such as counterexample-guided inductive synthesis (CEGIS) with satisfiability modulo theories (SMT) for verification. However, the CEGIS-SMT framework requires knowledge of system dynamics, which is unavailable in practical settings. To address this, we leverage the generalization of the Willems et al.'s fundamental lemma, using a single state trajectory, to construct a data-driven representation of (partially) unknown models for SMT verification without sacrificing accuracy. Additionally, CEGIS-SMT further removes the constraint of restricting barrier certificates to specific function classes, such as sum-of-squares, enabling greater flexibility in their design. We validate our approach on three nonlinear case studies with (partially) unknown dynamics.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey

Stochastic hybrid systems have received significant attentions as a relevant modelling framework describing many systems, from engineering to the life sciences: they enable the study of numerous applications, including transportation networks, biological systems and chemical reaction networks, smart energy and power grids, and beyond. Automated verification and policy synthesis for stochastic hybrid systems can be inherently challenging: this is due to the heterogeneity of their dynamics (presence of continuous and discrete components), the presence of uncertainty, and in some applications the large dimension of state and input sets. Over the past few years, a few hundred articles have investigated these models, and developed diverse and powerful approaches to mitigate difficulties encountered in the analysis and synthesis of such complex stochastic systems. In this survey, we overview the most recent results in the literature and discuss different approaches, including (in)finite abstractions, verification and synthesis for temporal logic specifications, stochastic similarity relations, (control) barrier certificates, compositional techniques, and a selection of results on continuous-time stochastic systems; we finally survey recently developed software tools that implement the discussed approaches. Throughout the manuscript we discuss a few open topics to be considered as potential future research directions: we hope that this survey will guide younger researchers through a comprehensive understanding of the various challenges, tools, and solutions in this enticing and rich scientific area.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Compositional Controller Synthesis for Interconnected Stochastic Systems with Markovian Switching

In this work, we propose a compositional scheme for the safety controller synthesis of interconnected discrete-time stochastic systems with Markovian switching signals. Our proposed approach is based on a notion of so-called control storage certificates computed for individual subsystems, by leveraging which, one can synthesize state-feedback controllers for interconnected systems to enforce safety specifications over finite time horizons. To do so, we employ a sum-of-squares (SOS) optimization approach to search for multiple storage certificates of each switching subsystem while synthesizing its corresponding safety controller. We then utilize dissipativity theory to compositionally construct barrier certificates for interconnected systems based on storage certificates of individual subsystems. The proposed dissipativity-type compositional conditions can leverage the structure of the interconnection topology and be fulfilled independently of the number or gains of subsystems. We eventually employ the constructed barrier certificate and quantify upper bounds on the probability that the interconnected system reaches certain unsafe regions in a finite time horizon. We apply our results to a room temperature network of 200 rooms with Markovian switching signals while accepting multiple storage certificates. We compositionally synthesize safety controllers to maintain the temperature of each room in a comfort zone for a bounded time horizon.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Compositional Reinforcement Learning for Discrete-Time Stochastic Control Systems

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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

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

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Constructing MDP Abstractions Using Data with Formal Guarantees

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Data-Driven Synthesis of Symbolic Abstractions with Guaranteed Confidence

In this work, we propose a data-driven approach for the construction of finite abstractions (a.k.a., symbolic models) for discrete-time deterministic control systems with unknown dynamics. We leverage notions of so-called alternating bisimulation functions (ABF), as a relation between each unknown system and its symbolic model, to quantify the mismatch between state behaviors of two systems. Accordingly, one can employ our proposed results to perform formal verification and synthesis over symbolic models and then carry the results back over unknown original systems. In our data-driven setting, we first cast the required conditions for constructing ABF as a robust optimization program (ROP). Solving the provided ROP is not tractable due to the existence of unknown models in the constraints of ROP. To tackle this difficulty, we collect finite numbers of data from trajectories of unknown systems and propose a scenario optimization program (SOP) corresponding to the original ROP. By establishing a probabilistic relation between optimal values of SOP and ROP, we formally construct ABF between unknown systems and their symbolic models based on the number of data and a required confidence level. We verify the effectiveness of our data-driven results over two physical case studies with unknown models including (i) a DC motor and (ii) a nonlinear jet engine compressor. We construct symbolic models from data as appropriate substitutes of original systems and synthesize policies maintaining states of unknown systems in a safe set within infinite time horizons with some guaranteed confidence levels.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Formal Estimation of Collision Risks for Autonomous Vehicles: A Compositional Data-Driven Approach

In this work, we propose a compositional data-driven approach for the formal estimation of collision risks for autonomous vehicles (AVs) while acting in a stochastic multi-agent framework. The proposed approach is based on the construction of sub-barrier certificates for each stochastic agent via a set of data collected from its trajectories while providing an a-priori guaranteed confidence on the data-driven estimation. In our proposed setting, we first cast the original collision risk problem for each agent as a robust optimization program (ROP). Solving the acquired ROP is not tractable due to an unknown model that appears in one of its constraints. To tackle this difficulty, we collect finite numbers of data from trajectories of each agent and provide a scenario optimization program (SOP) corresponding to the original ROP. We then establish a probabilistic bridge between the optimal value of SOP and that of ROP, and accordingly, we formally construct the sub-barrier certificate for each unknown agent based on the number of data and a required level of confidence. We then propose a compositional technique based on small-gain reasoning to quantify the collision risk for multi-agent AVs with some desirable confidence based on sub-barrier certificates of individual agents constructed from data. For the case that the proposed compositionality conditions are not satisfied, we provide a relaxed version of compositional results without requiring any compositionality conditions but at the cost of providing a potentially conservative collision risk. Eventually, we also present our approaches for non-stochastic multi-agent AVs. We demonstrate the effectiveness of our proposed results by applying them to a vehicle platooning consisting of 100 vehicles with 1 leader and 99 followers. We formally estimate the collision risk by collecting data from trajectories of each agent.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

From Small-Gain Theory to Compositional Construction of Barrier Certificates for Large-Scale Stochastic Systems

This paper is concerned with a compositional approach for the construction of control barrier certificates for large-scale interconnected stochastic systems while synthesizing hybrid controllers against high-level logic properties. Our proposed methodology involves decomposition of interconnected systems into smaller subsystems and leverages the notion of control sub-barrier certificates of subsystems, enabling one to construct control barrier certificates of interconnected systems by employing some max-type small-gain conditions. The main goal is to synthesize hybrid controllers enforcing complex logic properties including the ones represented by the accepting language of deterministic finite automata, while providing probabilistic guarantees on the satisfaction of given specifications in bounded-time horizons. To do so, we propose a systematic approach to first decompose high-level specifications into simple reachability tasks by utilizing automata corresponding to the complement of specifications. We then construct control sub-barrier certificates and synthesize local controllers for those simpler tasks and combine them to obtain a hybrid controller that ensures satisfaction of the complex specification with some lower bound on the probability of satisfaction. To compute control sub-barrier certificates and corresponding local controllers, we provide two systematic approaches based on sum-of-squares (SOS) optimization program and counter-example guided inductive synthesis (CEGIS) framework. We finally apply our proposed techniques to two physical case studies.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

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

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

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems

In this paper, we propose a software tool, called AMYTISS, implemented in C++/OpenCL, for designing correct-by-construction controllers for large-scale discrete-time stochastic systems. This tool is employed to (i) build finite Markov decision processes (MDPs) as finite abstractions of given original systems, and (ii) synthesize controllers for the constructed finite MDPs satisfying bounded-time high-level properties including safety, reachability and reach-avoid specifications. In AMYTISS, scalable parallel algorithms are designed such that they support the parallel execution within CPUs, GPUs and hardware accelerators (HWAs). Unlike all existing tools for stochastic systems, AMYTISS can utilize high-performance computing (HPC) platforms and cloud-computing services to mitigate the effects of the state-explosion problem, which is always present in analyzing large-scale stochastic systems. We benchmark AMYTISS against the most recent tools in the literature using several physical case studies including robot examples, room temperature and road traffic networks. We also apply our algorithms to a 3-dimensional autonomous vehicle and 7-dimensional nonlinear model of a BMW 320i car by synthesizing an autonomous parking controller.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Compositional (In)Finite Abstractions for Large-Scale Interconnected Stochastic Systems

This paper is concerned with a compositional approach for constructing both infinite (reduced-order models) and finite abstractions (a.k.a. finite Markov decision processes (MDPs)) of large-scale interconnected discrete-time stochastic systems. The proposed framework is based on the notion of stochastic simulation functions enabling us to employ an abstract system as a substitution of the original one in the controller design process with guaranteed error bounds. In the first part of the paper, we derive sufficient small-gain type conditions for the compositional quantification of the probabilistic distance between the interconnection of stochastic control subsystems and that of their infinite abstractions. We then construct infinite abstractions together with their corresponding stochastic simulation functions for a particular class of discrete-time nonlinear stochastic control systems. In the second part of the paper, we leverage small-gain type conditions for the compositional construction of finite abstractions. We propose an approach to construct finite MDPs as finite abstractions of concrete models or their reduced-order versions satisfying an incremental input-to-state stability property. We demonstrate the effectiveness of the proposed results by applying our approaches to a fully interconnected network of 20 nonlinear subsystems (totally 100 dimensions). We construct finite MDPs from their reduced-order versions (together 20 dimensions) with guaranteed error bounds on their output trajectories. We also apply the proposed results to a temperature regulation in a circular building and construct compositionally a finite abstraction of a network containing 1000 rooms. We employ the constructed finite abstractions as substitutes to compositionally synthesize policies regulating the temperature in each room for a bounded time horizon.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Compositional Abstraction of Large-Scale Stochastic Systems: A Relaxed Dissipativity Approach

In this paper, we propose a compositional approach for the construction of finite abstractions (a.k.a. finite Markov decision processes (MDPs)) for networks of discrete-time stochastic control subsystems that are not necessarily stabilizable. The proposed approach leverages the interconnection topology and a notion of finite-step stochastic storage functions, that describes joint dissipativity-type properties of subsystems and their abstractions, and establishes a finite-step stochastic simulation function as a relation between the network and its abstraction. To this end, we first develop a new type of compositionality conditions which is less conservative than the existing ones. In particular, using a relaxation via a finite-step stochastic simulation function, it is possible to construct finite abstractions such that stabilizability of each subsystem is not necessarily required. We then propose an approach to construct finite MDPs together with their corresponding finite-step storage functions for general discrete-time stochastic control systems satisfying an incremental passivablity property. We also construct finite MDPs for a particular class of nonlinear stochastic control systems. To demonstrate the effectiveness of the proposed results, we apply our results on three different case studies.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Formal Controller Synthesis for Continuous-Space MDPs via Model-Free Reinforcement Learning

A novel reinforcement learning scheme to synthesize policies for continuous-space Markov decision processes (MDPs) is proposed. This scheme enables one to apply model-free, off-the-shelf reinforcement learning algorithms for finite MDPs to compute optimal strategies for the corresponding continuous-space MDPs without explicitly constructing the finite-state abstraction. The proposed approach is based on abstracting the system with a finite MDP (without constructing it explicitly) with unknown transition probabilities, synthesizing strategies over the abstract MDP, and then mapping the results back over the concrete continuous-space MDP with approximate optimality guarantees. The properties of interest for the system belong to a fragment of linear temporal logic, known as syntactically co-safe linear temporal logic (scLTL), and the synthesis requirement is to maximize the probability of satisfaction within a given bounded time horizon. A key contribution of the paper is to leverage the classical convergence results for reinforcement learning on finite MDPs and provide control strategies maximizing the probability of satisfaction over unknown, continuous-space MDPs while providing probabilistic closeness guarantees. Automata-based reward functions are often sparse; we present a novel potential-based reward shaping technique to produce dense rewards to speed up learning. The effectiveness of the proposed approach is demonstrated by applying it to three physical benchmarks concerning the regulation of a room's temperature, control of a road traffic cell, and of a 7-dimensional nonlinear model of a BMW 320i car.

0 citations0 reviewsNo code linkedOpen access