| 1. |
- Gao, Yulong, et al.
(författare)
-
CTL Model Checking of MDPs over Distribution Spaces: Algorithms and Sampling-based Computations
- 2024
-
Ingår i: HSCC 2024 - Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, part of CPS-IoT Week. - : Association for Computing Machinery (ACM).
-
Konferensbidrag (refereegranskat)abstract
- This work studies computation tree logic (CTL) model checking for finite-state Markov decision processes (MDPs) over the space of their distributions. Instead of investigating properties over states of the MDP, as encoded by formulae in standard probabilistic CTL (PCTL), the focus of this work is on the associated transition system, which is induced by the MDP, and on its dynamics over the (transient) MDP distributions. CTL is thus used to specify properties over the space of distributions, and is shown to provide an alternative way to express probabilistic specifications or requirements over the given MDP. We discuss the distinctive semantics of CTL formulae over distribution spaces, compare them to existing non-branching logics that reason on probability distributions, and juxtapose them to traditional PCTL specifications. We then propose reachability-based CTL model checking algorithms over distribution spaces, as well as computationally tractable, sampling-based procedures for computing the relevant reachable sets: it is in particular shown that the satisfaction set of the CTL specification can be soundly under-approximated by the union of convex polytopes. Case studies display the scalability of these procedures to large MDPs.
|
|
| 2. |
- Gao, Yulong, et al.
(författare)
-
Distributional Reachability for Markov Decision Processes : Theory and Applications
- 2024
-
Ingår i: IEEE Transactions on Automatic Control. - : Institute of Electrical and Electronics Engineers (IEEE). - 0018-9286 .- 1558-2523. ; 69:7, s. 4598-4613
-
Tidskriftsartikel (refereegranskat)abstract
- We study distributional reachability for finite Markov decision processes (MDPs) from a control theoretical perspective. Unlike standard probabilistic reachability notions, which are defined over MDP states or trajectories, in this paper reachability is formulated over the space of probability distributions. We propose two set-valued maps for the forward and backward distributional reachability problems: the forward map collects all state distributions that can be reached from a set of initial distributions, while the backward map collects all state distributions that can reach a set of final distributions. We show that there exists a maximal invariant set under the forward map and this set is the region where the state distributions eventually always belong to, regardless of the initial state distribution and policy. The backward map provides an alternative way to solve a class of important problems for MDPs: the study of controlled invariance, the characterization of the domain of attraction, and reach-avoid problems. Three case studies illustrate the effectiveness of our approach.
|
|
| 3. |
- Gao, Yulong, et al.
(författare)
-
Robust Tube Model Predictive Control with Uncertainty Quantification for Discrete-Time Linear Systems
-
Annan publikation (övrigt vetenskapligt/konstnärligt)abstract
- This paper is concerned with model predictive control (MPC) of discrete-time linear systems subject to bounded additive disturbance and hard constraints on the state and input, whereas the true disturbance set is unknown. Unlike most existing work on robust MPC, we propose an MPC algorithm incorporating online uncertainty quantification that builds on prior knowledge of the disturbance, i.e., a known but conservative disturbance set. We approximate the true disturbance set at each time step with a parameterised set, which is referred to as a quantified disturbance set, using the scenario approach with additional disturbance realisations collected online. A key novelty of this paper is that the parameterisation of these quantified disturbance sets enjoy desirable properties such that the quantified disturbance set and its corresponding rigid tube bounding disturbance propagation can be efficiently updated online. We provide statistical gaps between the true and quantified disturbance sets, based on which, probabilistic recursive feasibility of MPC optimisation problems are discussed. Numerical simulations are provided to demonstrate the efficacy of our proposed algorithm and compare with conventional robust MPC algorithms.
|
|
| 4. |
- Gao, Yulong
(författare)
-
Stochastic Invariance and Aperiodic Control for Uncertain Constrained Systems
- 2018
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Uncertainties and constraints are present in most control systems. For example, robot motion planning and building climate regulation can be modeled as uncertain constrained systems. In this thesis, we develop mathematical and computational tools to analyze and synthesize controllers for such systems.As our first contribution, we characterize when a set is a probabilistic controlled invariant set and we develop tools to compute such sets. A probabilistic controlled invariantset is a set within which the controller is able to keep the system state with a certainprobability. It is a natural complement to the existing notion of robust controlled invariantsets. We provide iterative algorithms to compute a probabilistic controlled invariantset within a given set based on stochastic backward reachability. We prove that thesealgorithms are computationally tractable and converge in a finite number of iterations. The computational tools are demonstrated on examples of motion planning, climate regulation, and model predictive control.As our second contribution, we address the control design problem for uncertain constrained systems with aperiodic sensing and actuation. Firstly, we propose a stochastic self-triggered model predictive control algorithm for linear systems subject to exogenous disturbances and probabilistic constraints. We prove that probabilistic constraint satisfaction, recursive feasibility, and closed-loop stability can be guaranteed. The control algorithm is computationally tractable as we are able to reformulate the problem into a quadratic program. Secondly, we develop a robust self-triggered control algorithm for time-varying and uncertain systems with constraints based on reachability analysis. In the particular case when there is no uncertainty, the design leads to a control system requiring minimum number of samples over finite time horizon. Furthermore, when the plant is linear and the constraints are polyhedral, we prove that the previous algorithms can be reformulated as mixed integer linear programs. The method is applied to a motion planning problem with temporal constraints.
|
|
| 5. |
- Gao, Yulong, et al.
(författare)
-
Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-time Systems
- 2021
-
Ingår i: IEEE Transactions on Automatic Control. - : Institute of Electrical and Electronics Engineers (IEEE). - 0018-9286 .- 1558-2523. ; , s. 1-1
-
Tidskriftsartikel (refereegranskat)abstract
- We propose algorithms for performing model checking and control synthesis for discrete-time uncertain systems under linear temporal logic (LTL) specifications. We construct temporal logic trees (TLT) from LTL formulae via reachability analysis. In contrast to automaton-based methods, the construction of the TLT is abstraction-free for infinite systems, that is, we do not construct discrete abstractions of the infinite systems. Moreover, for a given transition system and an LTL formula, we prove that there exist both a universal TLT and an existential TLT via minimal and maximal reachability analysis, respectively. We show that the universal TLT is an underapproximation for the LTL formula and the existential TLT is an overapproximation. We provide sufficient conditions and necessary conditions to verify whether a transition system satisfies an LTL formula by using the TLT approximations. As a major contribution of this work, for a controlled transition system and an LTL formula, we prove that a controlled TLT can be constructed from the LTL formula via control-dependent reachability analysis. Based on the controlled TLT, we design an online control synthesis algorithm, under which a set of feasible control inputs can be generated at each time step. We also prove that this algorithm is recursively feasible. We illustrate the proposed methods for both finite and infinite systems and highlight the generality and online scalability with two simulated examples.
|
|
| 6. |
- Haesaert, Sofie, et al.
(författare)
-
Formal Control Synthesis via Simulation Relations and Behavioral Theory for Discrete-Time Descriptor Systems
- 2021
-
Ingår i: IEEE Transactions on Automatic Control. - : Institute of Electrical and Electronics Engineers (IEEE). - 0018-9286 .- 1558-2523. ; 66:3, s. 1024-1039
-
Tidskriftsartikel (refereegranskat)abstract
- The control and verification of industrial processes, modeled as discrete-time descriptor systems, is often computationally hard due to the presence of both algebraic couplings and difference equations. In this article, we introduce a new control synthesis method for descriptor systems which is based on formal abstractions and enables control design over related reduced-order models. We leverage notions of exact and approximate similarity relations, which hold for the algebraic couplings that are inherent to descriptor systems. Using the behavioral framework, we extend a control refinement scheme for classical dynamical systems and develop a corresponding notion for descriptor systems: We show that any given well-posed controller of the abstract (reduced-order) descriptor system can be refined to a controller for the original descriptor system. The resulting controlled system preserves the same controlled output behavior in the case of exact similarity, whereas in the case of approximate similarity, the output behavior of the controlled descriptor system is shown to have a bounded deviation from that of the abstract model where the controller is designed.
|
|
| 7. |
- Kamgarpour, Maryam, et al.
(författare)
-
Modeling options for demand side participation of thermostatically controlled loads
- 2013
-
Ingår i: Bulk Power System Dynamics and Control-IX Optimization, Security and Control of the Emerging Power Grid (IREP), 2013 IREP IREP2013. - 9781479901999
-
Konferensbidrag (refereegranskat)abstract
- Residential thermostatically controlled loads (TCLs) have potential for participation in electricity markets. This is because we can control a large group of these loads to achieve aggregate system behavior such as providing frequency reserves while ensuring the control actions are non-disruptive to the end users. A main challenge in controlling aggregations of TCLs is developing dynamical system models that are simple enough for optimization and control, but rich enough to capture the behavior of the loads. In this work, we propose three classes of models that approximate aggregate TCL dynamics. We analyze these models in terms of their accuracy and computational tractability. The models demonstrate a progression from models that help us analyze and predict TCL population behavior to those that help us develop large-scale automatic control strategies. Specifically, we demonstrate how formal methods from computer science and optimal control can be used to derive bounds on model error, guarantees for trajectory tracking, and algorithms for price arbitrage. We find that the accuracy of the analytic results decreases as TCL parameter heterogeneity is introduced. Thus, we motivate further development of analytical tools and modeling approaches to investigate realistic TCL behavior in power systems.
|
|
| 8. |
- Phung, Nga, et al.
(författare)
-
Photoprotection in metal halide perovskites by ionic defect formation
- 2022
-
Ingår i: Joule. - : Elsevier BV. - 2542-4351. ; 6:9, s. 2152-2174
-
Tidskriftsartikel (refereegranskat)abstract
- Photostability is critical for long-term solar cell operation. While light-triggered defects are usually reported as evidence of material degradation, we reveal that the formation of certain defects in metal halide perovskites is crucial for protection against intense or prolonged light exposure. We identify an inherent self-regulating cycle of formation and recovery of ionic defects under light exposure that mitigates the overheating of the lattice due to hot carrier cooling, which allows exposure to several thousand suns without degrading. The excess energy instead dissipates by forming defects, which in turn alters the optoelectronic properties of the absorber, resulting in a temporary reduction of photon absorption. Defects gradually recover to restore the original optoelectronic properties of the absorber. Photoprotection is a key feature for the photostability in plants. Thus, finding a protection mechanism in metal halide perovskites similar to those in nature is encouraging for the development of long-term sustainable solar cells.
|
|
| 9. |
- Phung, Nga, et al.
(författare)
-
The Role of Grain Boundaries on Ionic Defect Migration in Metal Halide Perovskites
- 2020
-
Ingår i: Advanced Energy Materials. - : Wiley. - 1614-6832 .- 1614-6840. ; 10:20
-
Tidskriftsartikel (refereegranskat)abstract
- Halide perovskites are emerging as revolutionary materials for optoelectronics. Their ionic nature and the presence of mobile ionic defects within the crystal structure have a dramatic influence on the operation of thin-film devices such as solar cells, light-emitting diodes, and transistors. Thin films are often polycrystalline and it is still under debate how grain boundaries affect the migration of ions and corresponding ionic defects. Laser excitation during photoluminescence (PL) microscopy experiments leads to formation and subsequent migration of ionic defects, which affects the dynamics of charge carrier recombination. From the microscopic observation of lateral PL distribution, the change in the distribution of ionic defects over time can be inferred. Resolving the PL dynamics in time and space of single crystals and thin films with different grain sizes thus, provides crucial information about the influence of grain boundaries on the ionic defect movement. In conjunction with experimental observations, atomistic simulations show that defects are trapped at the grain boundaries, thus inhibiting their diffusion. Hence, with this study, a comprehensive picture highlighting a fundamental property of the material is provided while also setting a theoretical framework in which the interaction between grain boundaries and ionic defect migration can be understood.
|
|
| 10. |
- Wang, Zifan, et al.
(författare)
-
Policy Evaluation in Distributional LQR
- 2023
-
Ingår i: Proceedings of the 5th Annual Learning for Dynamics and Control Conference, L4DC 2023. - : ML Research Press. ; , s. 1245-1256
-
Konferensbidrag (refereegranskat)abstract
- Distributional reinforcement learning (DRL) enhances the understanding of the effects of the randomness in the environment by letting agents learn the distribution of a random return, rather than its expected value as in standard RL. At the same time, a main challenge in DRL is that policy evaluation in DRL typically relies on the representation of the return distribution, which needs to be carefully designed. In this paper, we address this challenge for a special class of DRL problems that rely on discounted linear quadratic regulator (LQR) for control, advocating for a new distributional approach to LQR, which we call distributional LQR. Specifically, we provide a closed-form expression of the distribution of the random return which, remarkably, is applicable to all exogenous disturbances on the dynamics, as long as they are independent and identically distributed (i.i.d.). While the proposed exact return distribution consists of infinitely many random variables, we show that this distribution can be approximated by a finite number of random variables, and the associated approximation error can be analytically bounded under mild assumptions. Using the approximate return distribution, we propose a zeroth-order policy gradient algorithm for risk-averse LQR using the Conditional Value at Risk (CVaR) as a measure of risk. Numerical experiments are provided to illustrate our theoretical results.
|
|
