A5011080021- Formal Methods in Verification
- Petri Nets in System Modeling
- Fault Detection and Control Systems
- Advanced Control Systems Optimization
- Software Reliability and Analysis Research
- Gene Regulatory Network Analysis
- Risk and Safety Analysis
- Bayesian Modeling and Causal Inference
- Control Systems and Identification
- Stability and Control of Uncertain Systems
- Simulation Techniques and Applications
- Safety Systems Engineering in Autonomy
- Smart Grid Security and Resilience
- Embedded Systems Design Techniques
- Traffic control and management
- Adversarial Robustness in Machine Learning
- Real-Time Systems Scheduling
- Probabilistic and Robust Engineering Design
- Guidance and Control Systems
- Numerical Methods and Algorithms
- Radiation Effects in Electronics
- Model Reduction and Neural Networks
- Control and Dynamics of Mobile Robots
- Reliability and Maintenance Optimization
- Control and Stability of Dynamical Systems
Newcastle University
2022-2024
ETH Zurich
2021-2023
University of Colorado Boulder
2020
LMU Klinikum
2019-2020
Ludwig-Maximilians-Universität München
2018-2020
Technical University of Munich
2017-2019
University of Tehran
2014-2017
A novel reinforcement learning scheme to synthesize policies for continuous-space Markov decision processes (MDPs) is proposed. This enables one apply model-free, off-the- shelf algorithms finite MDPs compute optimal strategies the corresponding without explicitly constructing finite-state abstraction. The proposed approach based on abstracting system with a MDP (without it explicitly) unknown transition probabilities, synthesizing over abstract MDP, and then mapping results back concrete...
This work is concerned with a compositional technique for the construction of finite abstractions ( <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">a.k.a.,</i> Markov decision processes (MDPs)) networks discrete-time stochastic switched systems. We propose framework based on notion xmlns:xlink="http://www.w3.org/1999/xlink">stochastic simulation functions</i> , using which one can quantify probabilistic distance between original...
This article is concerned with a formal verification scheme for both discrete- and continuous-time deterministic systems unknown mathematical models. The main target to verify the safety of based on construction barrier certificates via set data collected from trajectories while providing an a-priori guaranteed confidence safety. In our proposed framework, we first cast original problem as robust convex program (RCP). Solving RCP not tractable in general since model appears one constraints....
Model order reduction (MOR) involves offering low-dimensional models that effectively approximate the behavior of complex high-order systems. Due to potential model complexities and computational costs, designing controllers for high-dimensional systems with behaviors can be challenging, rendering MOR a practical alternative achieve results closely resemble those original To construct such effective reduced-order (ROMs), existing literature generally necessitates precise knowledge systems,...
This paper is concerned with a compositional approach for constructing finite Markov decision processes of interconnected discrete-time stochastic control systems. The proposed leverages the interconnection topology and notion so-called storage functions describing joint dissipativity-type properties subsystems their abstractions. In first part paper, we derive conditions quantifying error between that second propose an to construct together corresponding classes systems satisfying some...
This article is concerned with a compositional approach for constructing both infinite (reduced-order models) and finite abstractions [a.k.a. Markov decision processes (MDPs)] of large-scale interconnected discrete-time stochastic systems. The proposed framework based on the notion simulation functions enabling us to employ an abstract system as substitution original one in controller design process guaranteed error bounds. In first part this article, we derive sufficient small-gain-type...
In this paper, we propose a compositional scheme for the safety controller synthesis of stochastic switched networks with <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">dwell-time</i> conditions. The proposed framework is based on notion so-called xmlns:xlink="http://www.w3.org/1999/xlink">transition sub-barrier certificates</i> constructed each subsystem, by employing which one can compositionally synthesize controllers interconnected over...
This paper is concerned with a compositional approach for constructing abstractions of interconnected discrete-time stochastic control systems. The abstraction framework based on new notions so-called simulation functions, using which one can quantify the distance between original systems and their in probabilistic setting. Accordingly, leverage proposed results to perform analysis synthesis over abstract systems, then carry concrete ones. In first part paper, we derive sufficient small-gain...
This letter is concerned with a data-driven technique for constructing finite Markov decision processes (MDPs) as abstractions of discrete-time stochastic control systems <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">unknown</i> dynamics while providing formal closeness guarantees. The proposed scheme based on notions xmlns:xlink="http://www.w3.org/1999/xlink">stochastic bisimulation functions</i> (SBF) to capture the probabilistic distance...
This article is concerned with a compositional approach for the construction of control barrier certificates large-scale interconnected stochastic systems while synthesizing hybrid controllers against high-level logic properties. Our proposed methodology involves decomposition into smaller subsystems and leverages notion <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">control</i> xmlns:xlink="http://www.w3.org/1999/xlink">sub-barrier...
This paper is concerned with a compositional approach for constructing finite abstractions (a.k.a. Markov decision processes) of interconnected discrete-time stochastic control systems. The proposed framework based on notion so-called simulation function enabling us to use an abstract system as substitution the original one in controller design process guaranteed error bounds. In first part paper, we derive sufficient small-gain type conditions quantification distance probability between...
In this paper, we provide a compositional technique for constructing finite abstractions (a.k.a. Markov decision processes) networks of discrete-time stochastic switched systems. The proposed framework is based on the notion simulation functions, using which one can employ MDP as substitution original in controller design process with guaranteed error bounds their output trajectories. respect, first leverage dissipativity-type conditions quantifying between interconnection subsystems and...
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 notion barrier certificates together with data collected from trajectories We first reformulate barrier-based verification as robust convex problem (RCP). Solving acquired RCP hard in general because not only state system lives continuous set, but also and more problematic, model appears one constraints...
In this letter, we propose a data-driven approach for the construction of finite abstractions ( <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">a.k.a.,</i> symbolic models) discrete-time deterministic control systems with unknown dynamics. We leverage notions so-called xmlns:xlink="http://www.w3.org/1999/xlink">alternating bisimulation functions</i> (ABF), as relation between each system and its model, to quantify mismatch state behaviors two...
This report presents the results of a friendly competition for formal verification and policy synthesis stochastic models. It also introduces new benchmarks their properties within this category recommends next steps towards year’s edition competition. In comparison with tools on non-probabilistic models, models are at early stages development that do not allow full standard set benchmarks. We an initiative to collect minimal all such can run, thus facilitating between efficiency implemented...