129 citations · 349 across the 72 of their papers we have counts for
23 papers · 1 filter
Data-driven Safety Verification of Stochastic Systems via Barrier Certificates
Ali Salamati, Abolfazl Lavaei, Sadegh Soudjani +1
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…
A small-gain theory for infinite networks via infinite-dimensional gain operators
Christoph Kawan, Majid Zamani
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…
Data-driven verification and synthesis of stochastic systems via barrier certificates
Ali Salamati, Abolfazl Lavaei, Sadegh Soudjani +1
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…
Formal Synthesis of Controllers for Uncertain Linear Systems against -Regular Properties: A Set-based Approach
Bingzhuo Zhong, Majid Zamani, Marco Caccamo
In this paper, we present how to synthesize controllers to enforce -regular properties over linear control systems affected by bounded disturbances. In particular, these control…
Compositional Construction of Abstractions for Infinite Networks of Switched Systems
Maryam Sharifi, Abdalla Swikir, Navid Noroozi +1
We construct compositional continuous approximations for an interconnection of infinitely many discrete-time switched systems. An approximation (known as abstraction) is itself a c…
Compositional Abstractions of Interconnected Discrete-Time Switched Systems
Abdalla Swikir, Majid Zamani
In this paper, we introduce a compositional method for the construction of finite abstractions of interconnected discrete-time switched systems. Particularly, we use a notion of so…
Verification of Switched Stochastic Systems via Barrier Certificates
Mahathi Anand, Pushpak Jagtap, Majid Zamani
The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a compl…
Compositional Verification of Initial-State Opacity for Switched Systems
Siyuan Liu, Abdalla Swikir, Majid Zamani
In this work, we propose a compositional framework for the verification of approximate initial-state opacity for networks of discrete-time switched systems. The proposed approach i…
Compositional synthesis of almost maximally permissible safety controllers
Siyuan Liu, Majid Zamani
In this work, we present a compositional safety controller synthesis approach for the class of discrete-time linear control systems. Here, we leverage a state-of-the-art result on…
Synthesis of Partially Observed Jump-Diffusion Systems via Control Barrier Functions
Niloofar Jahanshahi, Pushpak Jagtap, Majid Zamani
In this paper, we study formal synthesis of control policies for partially observed jump-diffusion systems against complex logic specifications. Given a state estimator, we utilize…
Sandboxing Controllers for Stochastic Cyber-Physical Systems
Bingzhuo Zhong, Majid Zamani, Marco Caccamo
Current cyber-physical systems (CPS) are expected to accomplish complex tasks. To achieve this goal, high performance, but unverified controllers (e.g. deep neural network, black-b…
Verification of Approximate Opacity via Barrier Certificates
Siyuan Liu, Majid Zamani
This paper is motivated by the increasing security concerns of cyber-physical systems. Here, we develop a discretization-free verification scheme targeting an information-flow secu…
Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates
Mahathi Anand, Vishnu Murali, Ashutosh Trivedi +1
Hyperproperties are system properties that require quantification over multiple execution traces of a system. Hyperproperties can express several specifications of interest for cyb…
Automata-based Controller Synthesis for Stochastic Systems: A Game Framework via Approximate Probabilistic Relations
Bingzhuo Zhong, Abolfazl Lavaei, Majid Zamani +1
In this work, we propose an abstraction and refinement methodology for the controller synthesis of discrete-time stochastic systems to enforce complex logical properties expressed…
ISS small-gain criteria for infinite networks with linear gain functions
Andrii Mironchenko, Navid Noroozi, Christoph Kawan +1
This paper provides a Lyapunov-based small-gain theorem for input-to-state stability (ISS) of networks composed of infinitely many finite-dimensional systems. We model these networ…
Compositional Construction of Safety Controllers for Networks of Continuous-Space POMDPs
Niloofar Jahanshahi, Abolfazl Lavaei, Majid Zamani
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. cont…
A Lyapunov-based ISS small-gain theorem for infinite networks of nonlinear systems
Christoph Kawan, Andrii Mironchenko, Majid Zamani
In this paper, we show that an infinite network of input-to-state stable (ISS) subsystems, admitting ISS Lyapunov functions, itself admits an ISS Lyapunov function, provided that t…
Compositional Synthesis of Control Barrier Certificates for Networks of Stochastic Systems against -Regular Specifications
Mahathi Anand, Abolfazl Lavaei, Majid Zamani
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…
Safe-visor Architecture for Sandboxing (AI-based) Unverified Controllers in Stochastic Cyber-Physical Systems
Bingzhuo Zhong, Abolfazl Lavaei, Hongpeng Cao +2
High performance but unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, are widely employed in cyber-physical systems (CPSs) to accomplish c…
Symbolic Models for Infinite Networks of Control Systems: A Compositional Approach
Siyuan Liu, Navid Noroozi, Majid Zamani
This paper presents a compositional framework for the construction of symbolic models for a network composed of a countably infinite number of finite-dimensional discrete-time cont…
Compositional Construction of Abstractions for Infinite Networks of Discrete-Time Switched Systems
Maryam Sharifi, Abdalla Swikir, Navid Noroozi +1
In this paper, we develop a compositional scheme for the construction of continuous approximations for interconnections of infinitely many discrete-time switched systems. An approx…
Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey
Abolfazl Lavaei, Sadegh Soudjani, Alessandro Abate +1
Stochastic hybrid systems have received significant attentions as a relevant modelling framework describing many systems, from engineering to the life sciences: they enable the stu…
From Small-Gain Theory to Compositional Construction of Barrier Certificates for Large-Scale Stochastic Systems
Mahathi Anand, Abolfazl Lavaei, Majid Zamani
This paper is concerned with a compositional approach for the construction of control barrier certificates for large-scale interconnected stochastic systems while synthesizing hybr…