4.7 Article

Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties

Journal

IEEE TRANSACTIONS ON AUTOMATIC CONTROL
Volume 65, Issue 4, Pages 1468-1483

Publisher

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2019.2923049

Keywords

Uncertainty; Programming; Time-varying systems; Viscosity; Reachability analysis; Trajectory; Nonlinear systems; Convex computations; reachability analysis; uncertainties

Funding

  1. CAS Pioneer Hundred Talents Program [Y8YC235015]
  2. NSFC [61625206, 61732001, 61872341]
  3. Deutsche Forschungsgemeinschaft [DFG GRK 1765]
  4. Science of Design of SocietalScale Cyber-Physical Systems [FR 2715/4-1]

Ask authors/readers for more resources

In this paper, we propose a convex programming based method to address a long-standing problem of inner-approximating backward reachable sets of state-constrained polynomial systems subject to time-varying uncertainties. The backward reachable set is a set of states, from which all trajectories starting will surely enter a target region at the end of a given time horizon without violating a set of state constraints in spite of the actions of uncertainties. It is equal to the zero sublevel set of the unique Lipschitz viscosity solution to a Hamilton-Jacobi partial differential equation (HJE). We show that inner approximations of the backward reachable set can be formed by zero sublevel sets of its viscosity supersolutions. Consequently, we reduce the inner-approximation problem to a problem of synthesizing polynomial viscosity supersolutions to this HJE. Such a polynomial solution in our method is synthesized by solving a single semidefinite program. We also prove that polynomial solutions to the formulated semidefinite program exist and can produce a convergent sequence of inner approximations to the interior of the backward reachable set in measure under appropriate assumptions. This is the main contribution of this paper. Several illustrative examples demonstrate the merits of our approach.

Authors

I am an author on this paper
Click your name to claim this paper and add it to your profile.

Reviews

Primary Rating

4.7
Not enough ratings

Secondary Ratings

Novelty
-
Significance
-
Scientific rigor
-
Rate this paper

Recommended

Article Ethics

A comparative, sociotechnical design perspective on Responsible Innovation: multidisciplinary research and education on digitized energy and Automated Vehicles

David J. Hess, Dasom Lee, Bianca Biebl, Martin Fraenzle, Sebastian Lehnhoff, Himanshu Neema, Juergen Niehaus, Alexander Pretschner, Janos Sztipanovits

Summary: This study develops a comparative sociotechnical design perspective for interdisciplinary teams, focusing on technical and governance challenges and their interplay. With a triple comparative perspective, the research explores issues across different technological systems, societal implications, and continents, providing insights on values, solution portability, and policy harmonization potential. Through international collaboration, the study offers practical applications for research and teaching.

JOURNAL OF RESPONSIBLE INNOVATION (2021)

Article Computer Science, Information Systems

A sampling-based approach for handling delays in continuous and hybrid systems

Erzana Berani Abdelwahab, Martin Fraenzle

Summary: This research demonstrates that adding natural constraints to the model of delayed feedback channels effectively reduces the complexity caused by delays. The reduction is based on a sampling approach that is applicable when specific conditions on the feedback are satisfied. Furthermore, the method has potential for application in mixed discrete-continuous dynamics of delayed hybrid systems.

IT-INFORMATION TECHNOLOGY (2021)

Article Physics, Condensed Matter

Phase transition in the bipartite z-matching

Till Kahlke, Martin Fraenzle, Alexander K. Hartmann

Summary: Numerically studying the maximum z-matching problem on ensembles of bipartite random graphs has shown results on the capacity and energy of the optimum matchings. Confirming analytical results for bipartite regular graphs and observing the same scaling behavior as standard matching for finite size behavior indicate the universality of the problem. Investigating saturability in bipartite Erdos-Renyi random graphs based on average degree revealed phase transitions between unsaturable and saturable phases, coinciding with changes in the running time of the matching algorithm.

EUROPEAN PHYSICAL JOURNAL B (2021)

Article Automation & Control Systems

Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems

Bai Xue, Naijun Zhan

Summary: This article investigates the estimation problem of the maximal robust invariant set for discrete-time perturbed nonlinear systems within the optimal control framework. The main contribution is reducing the problem to solving a Bellman type equation, and using numerical methods to provide an approximation of the maximal robust invariant set. Two examples demonstrate the performance of the Bellman equation based method.

IEEE TRANSACTIONS ON AUTOMATIC CONTROL (2022)

Article Computer Science, Theory & Methods

Costs and rewards in priced timed automata

Martin Fraenzle, Mahsa Shirmohammadi, Mani Swaminathan, James Worrell

Summary: This paper investigates the Pareto analysis of multi-priced timed automata (MPTA) and studies the Pareto Domination Problem. The results show that this problem is decidable for MPTA with at most three observers, but undecidable in general. Additionally, an approximate Pareto Domination approach is considered, which can be decided in exponential time.

INFORMATION AND COMPUTATION (2022)

Article Computer Science, Theory & Methods

Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow

Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan

Summary: This paper presents a method to efficiently design safety-critical cyber-physical systems (CPS) by combining AADL and Simulink/Stateflow (S/S) for co-modeling and verification. The proposed approach provides a unified graphical modeling environment and supports simulation through C code generation.

THEORETICAL COMPUTER SCIENCE (2022)

Article Computer Science, Artificial Intelligence

A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation

Bernd Finkbeiner, Martin Fraenzle, Florian Kohn, Paul Kroeger

Summary: Signal Temporal Logic is a linear-time temporal logic used for classifying time-dependent signals and monitoring cyber-physical systems. Existing algorithms assume perfect identity between sensor readings and ground truth, but we proposed an extended analysis to address inexact measurements and provide more informative monitoring verdicts. We developed optimal evaluation algorithms based on affine arithmetic and SAT modulo theory to solve the problem of inconclusive state estimations.

ALGORITHMS (2022)

Article Computer Science, Theory & Methods

Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming

Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen

Summary: We present an invariant barrier-certificate condition for ensuring unbounded-time safety of differential dynamical systems. The condition, which is the weakest possible one to achieve inductive invariance, can be encoded as an optimization problem subject to bilinear matrix inequalities (BMIs). We propose a synthesis algorithm based on difference-of-convex programming that approaches a local optimum of the BMI problem through solving a series of convex optimization problems. Our method, incorporated in a branch-and-bound framework, demonstrates effectiveness and efficiency in finding barrier certificates for ensuring safety.

INFORMATION AND COMPUTATION (2022)

Article Automation & Control Systems

Stability Verification for Heterogeneous Complex Networks via Iterative SOS Programming

Shuyuan Zhang, Shizhong Song, Lei Wang, Bai Xue

Summary: This paper investigates stability verification for heterogeneous polynomial complex networks using an iterative sum-of-squares programming approach. By introducing polynomial Lyapunov functions, a global asymptotic stability criterion is established for the heterogeneous complex networks under directed topology. The stability verification problem is reduced to a sum-of-squares optimization problem for solving polynomial matrix inequalities based on the proposed criterion. An iterative sum-of-squares programming approach is presented to handle the non-convex terms of the polynomial matrix inequalities, effectively achieving stability verification with polynomial Lyapunov functions. A numerical example demonstrates the theoretical and algorithmic advantages of the proposed method in fully automatic verification of global asymptotic stability for heterogeneous polynomial complex networks.

IEEE CONTROL SYSTEMS LETTERS (2023)

Article Computer Science, Software Engineering

Lower Bounds for Possibly Divergent Probabilistic Programs

Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan

Summary: In this paper, a new proof rule is proposed for verifying lower bounds on quantities of probabilistic programs. Unlike existing rules, this proof rule is not limited to almost-surely terminating programs and can be applied to establish non-trivial lower bounds on termination probabilities and expected values for potentially divergent probabilistic loops, such as the well-known three-dimensional random walk on a lattice.

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL (2023)

Article Automation & Control Systems

Inner Approximating Robust Reach-Avoid Sets for Discrete-Time Polynomial Dynamical Systems

Changyuan Zhao, Shuyuan Zhang, Lei Wang, Bai Xue

Summary: This article investigates the problem of approximating robust reach-avoid sets for discrete-time polynomial dynamical systems subject to disturbances over open time horizons. The robust reach-avoid set can be characterized exactly via a Bellman-type equation, but due to the challenge in solving it analytically, a reformulation is proposed to approximate the solution using novel constraints. When the involved data are polynomials, the problem can be encoded into a semidefinite program and efficiently solved using interior point methods. Several examples are provided to demonstrate the performance of the proposed method.

IEEE TRANSACTIONS ON AUTOMATIC CONTROL (2023)

Article Computer Science, Software Engineering

Contract-based specification of mode-dependent timing behavior

Janis Kroeger, Bjoern Koopmann, Ingo Stierand, Martin Fraenzle

Summary: The design of safety-critical systems requires the rigorous application of specification and verification methods. This paper presents an extension of a framework for timing property specification, which addresses the explicit handling of operating modes and transitions, reducing the complexity of verification. Formal semantics are provided to reason about the specifications and contract operations, enabling statements about mode composition. The results are illustrated through a real-world example.

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING (2023)

Proceedings Paper Computer Science, Hardware & Architecture

Handling of Operating Modes in Contract-Based Timing Specifications

Janis Kroeger, Bjoern Koopmann, Ingo Stierand, Nadra Tabassam, Martin Fraenzle

Summary: This paper presents an extension of a framework for specifying timing properties in contract-based design paradigm. By enhancing the specification language, it allows for specifying mode-dependent behavior and mode transitions. A formal specification is provided for reasoning and making statements about mode composition.

VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS (VECOS 2021) (2022)

Proceedings Paper Automation & Control Systems

Reach-avoid Analysis for Stochastic Discrete-time Systems

Bai Xue, Renjue Li, Naijun Zhan, Martin Franzle

Summary: This paper investigates the reach-avoid problem of stochastic discrete-time systems over open time horizons, using iterative polynomial maps with stochastic disturbances to model the system and computing an inner approximation of its p-reach-avoid set to ensure safety.

2021 AMERICAN CONTROL CONFERENCE (ACC) (2021)

No Data Available