kth.sePublications
Change search
Link to record
Permanent link

Direct link
Publications (10 of 17) Show all publications
Gao, Y., Abate, A., Xie, L. & Johansson, K. H. (2024). Distributional Reachability for Markov Decision Processes: Theory and Applications. IEEE Transactions on Automatic Control, 69(7), 4598-4613
Open this publication in new window or tab >>Distributional Reachability for Markov Decision Processes: Theory and Applications
2024 (English)In: IEEE Transactions on Automatic Control, ISSN 0018-9286, E-ISSN 1558-2523, Vol. 69, no 7, p. 4598-4613Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2024
Keywords
Aerospace electronics, Computational modeling, distributional reachability, Markov decision processes, Markov processes, Probabilistic logic, probabilistic reachability, Probability distribution, reach-avoid problems, Safety, set invariance, Trajectory
National Category
Control Engineering
Identifiers
urn:nbn:se:kth:diva-350164 (URN)10.1109/TAC.2023.3341282 (DOI)001259639500010 ()2-s2.0-85179798691 (Scopus ID)
Note

QC 20240710

Available from: 2024-07-10 Created: 2024-07-10 Last updated: 2024-07-22Bibliographically approved
Gao, Y., Jiang, F., Xie, L. & Johansson, K. H. (2022). Risk-Aware Optimal Control for Automated Overtaking With Safety Guarantees. IEEE Transactions on Control Systems Technology, 30(4), 1460-1472
Open this publication in new window or tab >>Risk-Aware Optimal Control for Automated Overtaking With Safety Guarantees
2022 (English)In: IEEE Transactions on Control Systems Technology, ISSN 1063-6536, E-ISSN 1558-0865, Vol. 30, no 4, p. 1460-1472Article in journal (Refereed) Published
Abstract [en]

This article proposes a solution to the overtaking control problem where an automated vehicle tries to overtake another vehicle with uncertain motion. Our solution allows the automated vehicle to robustly overtake a human-driven vehicle under certain assumptions. Uncertainty in the predicted motion makes the automated overtaking problem hard to solve due to feasibility issues that arise from the fact that the overtaken vehicle (e.g., a vehicle driven by an aggressive driver) may accelerate to prevent the overtaking maneuver. To counteract them, we introduce the weak assumption that the predicted velocity of the overtaken vehicle respects a supermartingale, meaning that its velocity is not increasing in expectation during the maneuver. We show that this formulation presents a natural notion of risk. Based on the martingale assumption, we perform a risk-aware reachability analysis by analytically characterizing the predicted collision probability. Then, we design a risk-aware optimal overtaking algorithm with guaranteed levels of collision avoidance. Finally, we illustrate the effectiveness of the proposed algorithm with a simulated example. 

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2022
Keywords
Atmospheric measurements, Automated overtaking, automated vehicle, martingale, Optimal control, Particle measurements, reachability analysis, risk-aware optimal control., Safety, Trajectory, Vehicles, Risk analysis, Risk assessment, Risk perception, Safety engineering, Atmospheric measurement, Automated vehicles, Optimal controls, Particle measurement, Risk aware, Automation
National Category
Vehicle and Aerospace Engineering Control Engineering Transport Systems and Logistics
Identifiers
urn:nbn:se:kth:diva-311803 (URN)10.1109/TCST.2021.3112613 (DOI)000732104200001 ()2-s2.0-85115742842 (Scopus ID)
Note

QC 20250326

Available from: 2022-05-04 Created: 2022-05-04 Last updated: 2025-03-26Bibliographically approved
Gao, Y., Abate, A., Jiang, F., Giacobbe, M., Xie, L. & Johansson, K. H. (2022). Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-time Systems. IEEE Transactions on Automatic Control, 67(10), 5071-5086
Open this publication in new window or tab >>Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-time Systems
Show others...
2022 (English)In: IEEE Transactions on Automatic Control, ISSN 0018-9286, E-ISSN 1558-2523, Vol. 67, no 10, p. 5071-5086Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2022
Keywords
Automata, Control systems, Linear systems, Model checking, Reachability analysis, Trajectory, Uncertainty, Abstracting, Computer circuits, Control system synthesis, Digital control systems, Discrete time control systems, Forestry, Online systems, Trees (mathematics), Uncertainty analysis, Automaton, Control synthesis, Infinite system, Linear temporal logic, Logic tree, Models checking, Temporal logic formula, Transition system, Temporal logic
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-313272 (URN)10.1109/TAC.2021.3118335 (DOI)000861438100007 ()2-s2.0-85119608436 (Scopus ID)
Note

QC 20250324

Available from: 2022-06-01 Created: 2022-06-01 Last updated: 2025-03-24Bibliographically approved
Gao, Y., Johansson, K. H. & Xie, L. (2021). Computing Probabilistic Controlled Invariant Sets. IEEE Transactions on Automatic Control, 66(7), 3138-3151
Open this publication in new window or tab >>Computing Probabilistic Controlled Invariant Sets
2021 (English)In: IEEE Transactions on Automatic Control, ISSN 0018-9286, E-ISSN 1558-2523, Vol. 66, no 7, p. 3138-3151Article in journal (Refereed) Published
Abstract [en]

This article investigates stochastic invariance for control systems through probabilistic controlled invariant sets (PCISs). As a natural complement to robust controlled invariant sets (RCISs), we propose finite-, and infinite-horizon PCISs, and explore their relation to RICSs. We design iterative algorithms to compute the PCIS within a given set. For systems with discrete spaces, the computations of the finite-, and infinite-horizon PCISs at each iteration are based on linear programming, and mixed integer linear programming, respectively. The algorithms are computationally tractable, and terminate in a finite number of steps. For systems with continuous spaces, we show how to discretize the spaces, and prove the convergence of the approximation when computing the finite-horizon PCISs. In addition, it is shown that an infinite-horizon PCIS can be computed by the stochastic backward reachable set from the RCIS contained in it. These PCIS algorithms are applicable to practical control systems. Simulations are given to illustrate the effectiveness of the theoretical results for motion planning.

Place, publisher, year, edition, pages
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC, 2021
Keywords
Markov processes, Probabilistic logic, Control systems, Aerospace electronics, Stochastic systems, Reliability, Probabilistic controlled invariant set (PCIS), reachability analysis, stochastic control systems
National Category
Control Engineering
Identifiers
urn:nbn:se:kth:diva-298749 (URN)10.1109/TAC.2020.3018438 (DOI)000668858300015 ()2-s2.0-85112515286 (Scopus ID)
Note

QC 20210719

Available from: 2021-07-19 Created: 2021-07-19 Last updated: 2022-06-25Bibliographically approved
Gao, Y., Cannon, M., Xie, L. & Johansson, K. H. (2021). Invariant cover: Existence, cardinality bounds, and computation. Automatica, 129, Article ID 109588.
Open this publication in new window or tab >>Invariant cover: Existence, cardinality bounds, and computation
2021 (English)In: Automatica, ISSN 0005-1098, E-ISSN 1873-2836, Vol. 129, article id 109588Article in journal (Refereed) Published
Abstract [en]

An invariant cover quantifies the information needed by a controller to enforce an invariance specification. This paper investigates some fundamental problems concerning existence and computation of an invariant cover for uncertain discrete-time linear control systems subject to state and control constraints. We develop necessary and sufficient conditions on the existence of an invariant cover for a polytopic set of states. The conditions can be checked by solving a set of linear programs, one for each extreme point of the state set. Based on these conditions, we give upper and lower bounds on the minimal cardinality of the invariant cover, and design an iterative algorithm with finite-time convergence to compute an invariant cover. We further show in two examples how to use an invariant cover in the design of a coder-controller pair that ensures invariance of a given set for a networked control system with a finite communication data rate.

Place, publisher, year, edition, pages
PERGAMON-ELSEVIER SCIENCE LTD, 2021
Keywords
Invariant cover, Invariance feedback entropy, Networked control systems
National Category
Control Engineering
Identifiers
urn:nbn:se:kth:diva-298166 (URN)10.1016/j.automatica.2021.109588 (DOI)000655689600020 ()2-s2.0-85103767640 (Scopus ID)
Note

QC 20210630

Available from: 2021-06-30 Created: 2021-06-30 Last updated: 2022-06-25Bibliographically approved
Zhang, S., Dai, L., Gao, Y. & Xia, Y. (2020). Adaptive interpolating control for constrained systems with parametric uncertainty and disturbances. International Journal of Robust and Nonlinear Control, 30(16), 6838-6852
Open this publication in new window or tab >>Adaptive interpolating control for constrained systems with parametric uncertainty and disturbances
2020 (English)In: International Journal of Robust and Nonlinear Control, ISSN 1049-8923, E-ISSN 1099-1239, Vol. 30, no 16, p. 6838-6852Article in journal (Refereed) Published
Abstract [en]

An adaptive interpolating control (AIC) algorithm is proposed for constrained linear systems with parametric uncertainty and additive disturbance. This adaptive algorithm consists of an iterative set membership identification algorithm, which updates the uncertain parameter set at each time step, and an interpolating controller, which robustly stabilizes the uncertain system with state and input constraints. We prove that the AIC algorithm is recursively feasible and guarantees robust constraint satisfaction and robust asymptotic stability of the closed-loop system in the presence of uncertainties. Moreover, we detail two possible extensions of the AIC algorithm: (a) persistent excitation conditions can be embedded into the AIC algorithm to accelerate the convergence of system parameters and (b) the combination of the AIC algorithm and aggressive learning is able to enlarge the size of the feasible region with every iteration by exploiting information from previous iterations. We illustrate the effectiveness of the proposed algorithms through comparisons with adaptive model predictive control and one example of mobile carrier robot.

Place, publisher, year, edition, pages
John Wiley and Sons Ltd, 2020
Keywords
adaptive control, constraint satisfaction problem, interpolating control, set membership identification, Adaptive algorithms, Asymptotic stability, Closed loop systems, Interpolation, Iterative methods, Linear systems, Model predictive control, Parameter estimation, Predictive control systems, Uncertainty analysis, Adaptive model predictive control, Constrained linear systems, Constraint Satisfaction, Parametric uncertainties, Persistent excitation conditions, Robust asymptotic stability, Set-membership identification, State and input constraints, Adaptive control systems
National Category
Control Engineering
Identifiers
urn:nbn:se:kth:diva-287938 (URN)10.1002/rnc.5140 (DOI)000564474100001 ()2-s2.0-85090059340 (Scopus ID)
Note

QC 20201221

Available from: 2020-12-21 Created: 2020-12-21 Last updated: 2022-06-25Bibliographically approved
Jiang, F., Gao, Y., Xie, L. & Johansson, K. H. (2020). Ensuring safety for vehicle parking tasks using Hamilton-Jacobi reachability analysis. In: Proceedings of the IEEE Conference on Decision and Control: . Paper presented at 59th IEEE Conference on Decision and Control, CDC 2020, 14 December 2020 through 18 December 2020 (pp. 1416-1421). Institute of Electrical and Electronics Engineers Inc.
Open this publication in new window or tab >>Ensuring safety for vehicle parking tasks using Hamilton-Jacobi reachability analysis
2020 (English)In: Proceedings of the IEEE Conference on Decision and Control, Institute of Electrical and Electronics Engineers Inc. , 2020, p. 1416-1421Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we propose an approach for ensuring the safety of a vehicle throughout a parking task, even when the vehicle is being operated at varying levels of automation. We start by specifying a vehicle parking task using linear temporal logic formulae that can be model checked for feasibility. The model-checking is facilitated by the construction of a temporal logic tree via Hamilton-Jacobi reachability analysis. Once we know the parking task is feasible for our vehicle model, we utilize the constructed temporal logic tree to directly synthesize control sets. Our approach synthesizes control sets that are least-restrictive in the context of the specification, since they permit any control inputs that are guaranteed not to violate the specification. This least-restrictive characteristic allows for the application of our approach to vehicles under different modes of operation (e.g., human-in-the-loop shared autonomy or fully-automated schemes). Implementing in both simulation and on hardware, we demonstrate the approach's potential for ensuring the safety of vehicles throughout parking tasks, whether they are operated by humans or automated driving systems. 

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc., 2020
Keywords
Automation, Computer circuits, Model checking, Specifications, Temporal logic, Automated driving systems, Hamilton-Jacobi, Human-in-the-loop, Levels of automation, Linear temporal logic, Modes of operation, Reachability analysis, Safety of vehicles, Vehicles
National Category
Control Engineering Robotics and automation Computer Sciences
Identifiers
urn:nbn:se:kth:diva-301189 (URN)10.1109/CDC42340.2020.9304186 (DOI)000717663401035 ()2-s2.0-85099886725 (Scopus ID)
Conference
59th IEEE Conference on Decision and Control, CDC 2020, 14 December 2020 through 18 December 2020
Funder
Knut and Alice Wallenberg FoundationSwedish Research Council
Note

QC 20210907

Available from: 2021-09-07 Created: 2021-09-07 Last updated: 2025-02-05Bibliographically approved
Jiang, F., Gao, Y., Xie, L. & Johansson, K. H. (2020). Human-Centered Design for Safe Teleoperation of Connected Vehicles. In: IFAC papersonline: . Paper presented at 3rd IFAC Workshop pn Cyber-Physical and Human Systems (CPHS), DEC 03-05, 2020, Beijing, PEOPLES R CHINA (pp. 224-231). Elsevier BV, 53(5)
Open this publication in new window or tab >>Human-Centered Design for Safe Teleoperation of Connected Vehicles
2020 (English)In: IFAC papersonline, Elsevier BV , 2020, Vol. 53, no 5, p. 224-231Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we propose a framework for the safe teleoperation of connected vehicles by remote human operators. The proposed framework combines model-checking, reachability analysis, and human factor design into a unified approach that checks the feasibility of linear temporal logic (LTL) specified teleoperation tasks, guarantees safety throughout the execution of the tasks, and keeps the remote operator as the primary decision maker in the control loop. We apply the general approach to a remote parking example to illustrate the framework. Then, to evaluate the framework's benefits and usability, we conduct a user study on an experimental remote control operator's room and a 1/10th scale vehicle. In the user study, we validate the approach's ability to ensure the completion of LTL-specified tasks and gain initial insight into whether human users find the teleoperation system intuitive.

Place, publisher, year, edition, pages
Elsevier BV, 2020
Keywords
teleoperation, human-centered design, linear temporal logic, reachability analysis, safety automated vehicles
National Category
Control Engineering
Identifiers
urn:nbn:se:kth:diva-298153 (URN)10.1016/j.ifacol.2021.04.101 (DOI)000656589700040 ()2-s2.0-85107891909 (Scopus ID)
Conference
3rd IFAC Workshop pn Cyber-Physical and Human Systems (CPHS), DEC 03-05, 2020, Beijing, PEOPLES R CHINA
Note

QC 20210629

Available from: 2021-06-29 Created: 2021-06-29 Last updated: 2022-09-19Bibliographically approved
Gao, Y., Xie, L. & Johansson, K. H. (2020). Probabilistic Characterization of Target Set and Region of Attraction for Discrete-time Control Systems. In: IEEE International Conference on Control and Automation, ICCA: . Paper presented at 16th IEEE International Conference on Control and Automation, ICCA 2020, 9 October 2020 through 11 October 2020 (pp. 594-599). IEEE Computer Society
Open this publication in new window or tab >>Probabilistic Characterization of Target Set and Region of Attraction for Discrete-time Control Systems
2020 (English)In: IEEE International Conference on Control and Automation, ICCA, IEEE Computer Society , 2020, p. 594-599Conference paper, Published paper (Refereed)
Abstract [en]

This paper proposes a new notion of stabilization in probability for discrete-time stochastic systems that may be with unbounded disturbances and bounded control input. This new notion builds on two sets: target set and region of attraction. The target set is a set within which the controller is able to keep the system state with a certain probability. The region of attraction is a set from which the controller is able to drive the system state to the target set with a prescribed probability. We investigate the probabilistic characterizations of these two sets for linear stochastic control systems. We provide sufficient conditions for a compact set to be a target set with a given horizon and probability level. Given a target set, we use two methods to characterize the region of attraction: one is based on the solution to a stochastic optimal first-entry time problem while the other is based on stochastic backward reachable sets. For linear scalar systems, we provide analytic representations for the target set and the region of attraction. Simulations are given to illustrate the effectiveness of the theoretical results.

Place, publisher, year, edition, pages
IEEE Computer Society, 2020
Keywords
Control system synthesis, Controllers, Probability, Stochastic control systems, Stochastic systems, Analytic representation, Bounded controls, Discrete-time stochastic systems, Linear stochastic control systems, Prescribed probability, Probability levels, Region of attraction, Scalar systems, Discrete time control systems
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:kth:diva-290326 (URN)10.1109/ICCA51439.2020.9264433 (DOI)000646357300102 ()2-s2.0-85098084492 (Scopus ID)
Conference
16th IEEE International Conference on Control and Automation, ICCA 2020, 9 October 2020 through 11 October 2020
Note

QC 20210224

Available from: 2021-02-24 Created: 2021-02-24 Last updated: 2022-06-25Bibliographically approved
Gao, Y., Jiang, F., Ren, X., Xie, L. & Johansson, K. H. (2020). Reachability-based Human-in-the-Loop Control with Uncertain Specifications. In: IFAC PAPERSONLINE: . Paper presented at 21st IFAC World Congress on Automatic Control - Meeting Societal Challenges, JUL 11-17, 2020, ELECTR NETWORK (pp. 1880-1887). Elsevier BV, 53(2)
Open this publication in new window or tab >>Reachability-based Human-in-the-Loop Control with Uncertain Specifications
Show others...
2020 (English)In: IFAC PAPERSONLINE, Elsevier BV , 2020, Vol. 53, no 2, p. 1880-1887Conference paper, Published paper (Refereed)
Abstract [en]

We propose a shared autonomy approach for implementing human operator decisions onto an automated system during multi-objective missions, while guaranteeing safety and mission completion. A mission is specified as a set of linear temporal logic (LTL) formulae. Then, using a novel correspondence between LTL and reachability analysis, we synthesize a set of controllers for assisting the human operator to complete the mission, while guaranteeing that the system maintains specified spatial and temporal properties. We assume the human operator's exact preference of how to complete the mission is unknown. Instead, we use a datadriven approach to infer and update the automated system's internal belief of which specified objective the human intends to complete. If, while the human is operating the system, she provides inputs that violate any of the invariances prescribed by the LTL formula, our verified controller will use its internal belief of the human operator's intended objective to guide the operator back on track. Moreover, we show that as long as the specifications are initially feasible, our controller will stay feasible and can guide the human to complete the mission despite some unexpected human errors. We illustrate our approach with a simple, but practical, experimental setup where a remote operator is parking a vehicle in a parking lot with multiple parking options. In these experiments, we show that our approach is able to infer the human operator's preference over parking spots in real-time and guarantee that the human will park in the spot safely. 

Place, publisher, year, edition, pages
Elsevier BV, 2020
Keywords
shared autonomy, linear temporal logic, reachability analysis, robotic missions, safety, automated vehicles
National Category
Robotics and automation
Identifiers
urn:nbn:se:kth:diva-298156 (URN)10.1016/j.ifacol.2020.12.2572 (DOI)000652592500303 ()2-s2.0-85095554411 (Scopus ID)
Conference
21st IFAC World Congress on Automatic Control - Meeting Societal Challenges, JUL 11-17, 2020, ELECTR NETWORK
Note

QC 20210802

Available from: 2021-08-02 Created: 2021-08-02 Last updated: 2025-02-09Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0003-2338-5487

Search in DiVA

Show all publications