Risk assessment is a crucial component of collision warning and avoidance systems for intelligent vehicles.Reachability-based formal approaches have been developed to ensure driving safety to accurately detect potenti...Risk assessment is a crucial component of collision warning and avoidance systems for intelligent vehicles.Reachability-based formal approaches have been developed to ensure driving safety to accurately detect potential vehicle collisions.However,they suffer from over-conservatism,potentially resulting in false–positive risk events in complicated real-world applications.In this paper,we combine two reachability analysis techniques,a backward reachable set(BRS)and a stochastic forward reachable set(FRS),and propose an integrated probabilistic collision–detection framework for highway driving.Within this framework,we can first use a BRS to formally check whether a two-vehicle interaction is safe;otherwise,a prediction-based stochastic FRS is employed to estimate the collision probability at each future time step.Thus,the framework can not only identify non-risky events with guaranteed safety but also provide accurate collision risk estimation in safety-critical events.To construct the stochastic FRS,we develop a neural network-based acceleration model for surrounding vehicles and further incorporate a confidence-aware dynamic belief to improve the prediction accuracy.Extensive experiments were conducted to validate the performance of the acceleration prediction model based on naturalistic highway driving data.The efficiency and effectiveness of the framework with infused confidence beliefs were tested in both naturalistic and simulated highway scenarios.The proposed risk assessment framework is promising for real-world applications.展开更多
Reachability analysis is an important approach for acquiring Petri net (PN) properties. The reachability tree and the solution of the state equation are two commonly used methods for reachability analysis, but they ca...Reachability analysis is an important approach for acquiring Petri net (PN) properties. The reachability tree and the solution of the state equation are two commonly used methods for reachability analysis, but they can result in state explosion and spurious solutions in some cases. As a significant complementary method, the PN reduction technique simplifies the reachability analysis by reducing the net size while preserving the reachability. This paper introduces several useful reduction rules and defines a reduction process for the analysis of reachability which is easy to understand and implement. Some examples are given to explain the method to solve the reachability problem. The analysis shows that the proposed reduction method preserves the visualization feature of PN and can be easily used.展开更多
For symbolic reachability analysis of rectangular hybrid systems, the basic issue is finding a formal structure to represent and manipulate its infinite state spaces. Firstly, this structure must be closed to the reac...For symbolic reachability analysis of rectangular hybrid systems, the basic issue is finding a formal structure to represent and manipulate its infinite state spaces. Firstly, this structure must be closed to the reachability operation which means that reachable states from states expressed by this structure can be presented by it too. Secondly, the operation of finding reachable states with this structure should take as less computation as possible. To this end, a constraint system called rectangular zone is formalized, which is a conjunction of fixed amount of inequalities that compare fixed types of linear expressions with two variables to rational numbers. It is proved that the rectangular zone is closed to those reachability operations-intersection, elapsing of time and edge transition. Since the number of inequalities and the linear expression of each inequality is fixed in rectangular zones, so to obtain reachable rectangular zones, it just needs to change the rational numbers to which these linear expressions need to compare. To represent rectangular zones and unions of rectangular zones, a data structure called three dimensional constraint matrix(TDCM) and a BDD-like structure rectangular hybrid diagram(RHD) are introduced.展开更多
Qualitative spacecraft pursuit-evasion problem which focuses on feasibility is rarely studied because of high-dimensional dynamics,intractable terminal constraints and heavy computational cost.In this paper,A physics-...Qualitative spacecraft pursuit-evasion problem which focuses on feasibility is rarely studied because of high-dimensional dynamics,intractable terminal constraints and heavy computational cost.In this paper,A physics-informed framework is proposed for the problem,providing an intuitive method for spacecraft threat relationship determination,situation assessment,mission feasibility analysis and orbital game rules summarization.For the first time,situation adjustment suggestions can be provided for the weak player in orbital game.First,a dimension-reduction dynamics is derived in the line-of-sight rotation coordinate system and the qualitative model is determined,reducing complexity and avoiding the difficulty of target set presentation caused by individual modeling.Second,the Backwards Reachable Set(BRS)of the target set is used for state space partition and capture zone presentation.Reverse-time analysis can eliminate the influence of changeable initial state and enable the proposed framework to analyze plural situations simultaneously.Third,a time-dependent Hamilton-Jacobi-Isaacs(HJI)Partial Differential Equation(PDE)is established to describe BRS evolution driven by dimension-reduction dynamics,based on level set method.Then,Physics-Informed Neural Networks(PINNs)are extended to HJI PDE final value problem,supporting orbital game rules summarization through capture zone evolution analysis.Finally,numerical results demonstrate the feasibility and efficiency of the proposed framework.展开更多
For a class of time-delay discrete-time linear systems with external disturbance and measurement noise, the interval estimation problems of state and measurement noise are investigated in this paper. First, the system...For a class of time-delay discrete-time linear systems with external disturbance and measurement noise, the interval estimation problems of state and measurement noise are investigated in this paper. First, the system state together with the time-delay term and measurement noise is augmented as a new state, and a singular system is then constructed. Subsequently, a kind of decoupling technique is employed to eliminate the effect of external disturbance, and an observer is designed to simultaneously estimate the system state and measurement noise. Based on the estimated state and measurement noise, the interval estimations of system state and measurement noise are obtained by reachability analysis technique. Finally, the effectiveness of the proposed method is verified by a four-tank liquid level system.展开更多
Resilient motion planning and control,without prior knowledge of disturbances,are crucial to ensure the safe and robust flight of quadrotors.The development of a motion planning and control architecture for quadrotors...Resilient motion planning and control,without prior knowledge of disturbances,are crucial to ensure the safe and robust flight of quadrotors.The development of a motion planning and control architecture for quadrotors,considering both internal and external disturbances(i.e.,motor damages and suspended payloads),is addressed.Firstly,the authors introduce the use of exponential functions to formulate trajectory planning.This choice is driven by its ability to predict thrust responses with minimal computational overhead.Additionally,a reachability analysis is incorporated for error dynamics resulting from multiple disturbances.This analysis sits at the interface between the planner and controller,contributing to the generation of more robust and safe spatial–temporal trajectories.Lastly,the authors employ a cascade controller,with the assistance of internal and external loop observers,to further enhance resilience and compensate the disturbances.The authors’benchmark experiments demonstrate the effectiveness of the proposed strategy in enhancing flight safety,particularly when confronted with motor damages and payload disturbances.展开更多
This paper investigates the transition function and the reachability conditions of finite automata by using a semitensor product of matrices, which is a new powerful matrix analysis tool. The states and input symbols ...This paper investigates the transition function and the reachability conditions of finite automata by using a semitensor product of matrices, which is a new powerful matrix analysis tool. The states and input symbols are first expressed in vector forms, then the transition function is described in an algebraic form. Using this algebraic representation, a sufficient and necessary condition of the reachability of any two states is proposed, based on which an algorithm is developed for discovering all the paths from one state to another. Furthermore, a mechanism is established to recognize the language acceptable by a finite automaton. Finally, illustrative examples show that the results/algorithms presented in this paper are suitable for both deterministic finite automata (DFA) and nondeterministic finite automata (NFA).展开更多
In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory i...In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams (ROBDDs) to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae (DF). Then, the MDGs operations are defined and the correctness proof of each operation is provided. The MDG teachability algorithm is then defined as a conversion that uses our MDG theory within HOL. Finally, a set of experimentations over benchmark circuits has been conducted to ensure the applicability and to measure the performance of our approach.展开更多
A novel reachable set(RS) model is developed within a framework of exoatmospheric interceptor engagement analysis. The boost phase steering scheme and trajectory distortion mechanism of the interceptor are firstly e...A novel reachable set(RS) model is developed within a framework of exoatmospheric interceptor engagement analysis. The boost phase steering scheme and trajectory distortion mechanism of the interceptor are firstly explored. A mathematical model of the distorted RS is then formulated through a dimension–reduction analysis. By treating the outer boundary of the RS on sphere surface as a spherical convex hull, two relevant theorems are proposed and the RS envelope is depicted by the computational geometry theory. Based on RS model, the algorithms of intercept window analysis and launch parameters determination are proposed, and numerical simulations are carried out for interceptors with different energy or launch points. Results show that the proposed method can avoid intensive on-line computation and provide an accurate and effective approach for interceptor engagement analysis. The suggested RS model also serves as a ready reference to other related problems such as interceptor effectiveness evaluation and platform disposition.展开更多
基金supported by the proactive SAFEty systems and tools for a constantly UPgrading road environment(SAFE-UP)projectfunding from the European Union’s Horizon 2020 Research and Innovation Program(861570)。
文摘Risk assessment is a crucial component of collision warning and avoidance systems for intelligent vehicles.Reachability-based formal approaches have been developed to ensure driving safety to accurately detect potential vehicle collisions.However,they suffer from over-conservatism,potentially resulting in false–positive risk events in complicated real-world applications.In this paper,we combine two reachability analysis techniques,a backward reachable set(BRS)and a stochastic forward reachable set(FRS),and propose an integrated probabilistic collision–detection framework for highway driving.Within this framework,we can first use a BRS to formally check whether a two-vehicle interaction is safe;otherwise,a prediction-based stochastic FRS is employed to estimate the collision probability at each future time step.Thus,the framework can not only identify non-risky events with guaranteed safety but also provide accurate collision risk estimation in safety-critical events.To construct the stochastic FRS,we develop a neural network-based acceleration model for surrounding vehicles and further incorporate a confidence-aware dynamic belief to improve the prediction accuracy.Extensive experiments were conducted to validate the performance of the acceleration prediction model based on naturalistic highway driving data.The efficiency and effectiveness of the framework with infused confidence beliefs were tested in both naturalistic and simulated highway scenarios.The proposed risk assessment framework is promising for real-world applications.
文摘Reachability analysis is an important approach for acquiring Petri net (PN) properties. The reachability tree and the solution of the state equation are two commonly used methods for reachability analysis, but they can result in state explosion and spurious solutions in some cases. As a significant complementary method, the PN reduction technique simplifies the reachability analysis by reducing the net size while preserving the reachability. This paper introduces several useful reduction rules and defines a reduction process for the analysis of reachability which is easy to understand and implement. Some examples are given to explain the method to solve the reachability problem. The analysis shows that the proposed reduction method preserves the visualization feature of PN and can be easily used.
基金supported by the National Natural Science Foundation of China(Grant Nos.61373043&61003079)the Fundamental Research Funds for the Central Universities(Grant No.JB140316)
文摘For symbolic reachability analysis of rectangular hybrid systems, the basic issue is finding a formal structure to represent and manipulate its infinite state spaces. Firstly, this structure must be closed to the reachability operation which means that reachable states from states expressed by this structure can be presented by it too. Secondly, the operation of finding reachable states with this structure should take as less computation as possible. To this end, a constraint system called rectangular zone is formalized, which is a conjunction of fixed amount of inequalities that compare fixed types of linear expressions with two variables to rational numbers. It is proved that the rectangular zone is closed to those reachability operations-intersection, elapsing of time and edge transition. Since the number of inequalities and the linear expression of each inequality is fixed in rectangular zones, so to obtain reachable rectangular zones, it just needs to change the rational numbers to which these linear expressions need to compare. To represent rectangular zones and unions of rectangular zones, a data structure called three dimensional constraint matrix(TDCM) and a BDD-like structure rectangular hybrid diagram(RHD) are introduced.
基金This study was supported by the Independent Innovation Science Foundation Project of National University of Defense Technology,China(No.22-ZZCX-083).
文摘Qualitative spacecraft pursuit-evasion problem which focuses on feasibility is rarely studied because of high-dimensional dynamics,intractable terminal constraints and heavy computational cost.In this paper,A physics-informed framework is proposed for the problem,providing an intuitive method for spacecraft threat relationship determination,situation assessment,mission feasibility analysis and orbital game rules summarization.For the first time,situation adjustment suggestions can be provided for the weak player in orbital game.First,a dimension-reduction dynamics is derived in the line-of-sight rotation coordinate system and the qualitative model is determined,reducing complexity and avoiding the difficulty of target set presentation caused by individual modeling.Second,the Backwards Reachable Set(BRS)of the target set is used for state space partition and capture zone presentation.Reverse-time analysis can eliminate the influence of changeable initial state and enable the proposed framework to analyze plural situations simultaneously.Third,a time-dependent Hamilton-Jacobi-Isaacs(HJI)Partial Differential Equation(PDE)is established to describe BRS evolution driven by dimension-reduction dynamics,based on level set method.Then,Physics-Informed Neural Networks(PINNs)are extended to HJI PDE final value problem,supporting orbital game rules summarization through capture zone evolution analysis.Finally,numerical results demonstrate the feasibility and efficiency of the proposed framework.
基金supported in part by the National Nature Science Foundation of China(No.61973105)the Natural Science Foundation of Henan Province(No.232300420147)the Fundamental Research Funds for the Universities of Henan Province(No.NSFRF180335).
文摘For a class of time-delay discrete-time linear systems with external disturbance and measurement noise, the interval estimation problems of state and measurement noise are investigated in this paper. First, the system state together with the time-delay term and measurement noise is augmented as a new state, and a singular system is then constructed. Subsequently, a kind of decoupling technique is employed to eliminate the effect of external disturbance, and an observer is designed to simultaneously estimate the system state and measurement noise. Based on the estimated state and measurement noise, the interval estimations of system state and measurement noise are obtained by reachability analysis technique. Finally, the effectiveness of the proposed method is verified by a four-tank liquid level system.
基金National Natural Science Foundation of China,Grant/Award Numbers:62303412,62322314China Postdoctoral Science Foundation,Grant/Award Number:2022M722739Natural Science Foundation of Zhejiang Province,Grant/Award Number:2023YZ01。
文摘Resilient motion planning and control,without prior knowledge of disturbances,are crucial to ensure the safe and robust flight of quadrotors.The development of a motion planning and control architecture for quadrotors,considering both internal and external disturbances(i.e.,motor damages and suspended payloads),is addressed.Firstly,the authors introduce the use of exponential functions to formulate trajectory planning.This choice is driven by its ability to predict thrust responses with minimal computational overhead.Additionally,a reachability analysis is incorporated for error dynamics resulting from multiple disturbances.This analysis sits at the interface between the planner and controller,contributing to the generation of more robust and safe spatial–temporal trajectories.Lastly,the authors employ a cascade controller,with the assistance of internal and external loop observers,to further enhance resilience and compensate the disturbances.The authors’benchmark experiments demonstrate the effectiveness of the proposed strategy in enhancing flight safety,particularly when confronted with motor damages and payload disturbances.
基金Acknowledgements This work was supported by the National Natural Science Foundation of China (Grant No. 61174094), and the Tianjin Natural Science Foundation of China under (14JCYBJC18700 and 13JCY- BJC17400).
文摘This paper investigates the transition function and the reachability conditions of finite automata by using a semitensor product of matrices, which is a new powerful matrix analysis tool. The states and input symbols are first expressed in vector forms, then the transition function is described in an algebraic form. Using this algebraic representation, a sufficient and necessary condition of the reachability of any two states is proposed, based on which an algorithm is developed for discovering all the paths from one state to another. Furthermore, a mechanism is established to recognize the language acceptable by a finite automaton. Finally, illustrative examples show that the results/algorithms presented in this paper are suitable for both deterministic finite automata (DFA) and nondeterministic finite automata (NFA).
文摘In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams (ROBDDs) to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae (DF). Then, the MDGs operations are defined and the correctness proof of each operation is provided. The MDG teachability algorithm is then defined as a conversion that uses our MDG theory within HOL. Finally, a set of experimentations over benchmark circuits has been conducted to ensure the applicability and to measure the performance of our approach.
基金co-supported by the National Natural Science Foundation of China (No. 11272346)the National Basic Research Program of China (No. 2013CB733100)
文摘A novel reachable set(RS) model is developed within a framework of exoatmospheric interceptor engagement analysis. The boost phase steering scheme and trajectory distortion mechanism of the interceptor are firstly explored. A mathematical model of the distorted RS is then formulated through a dimension–reduction analysis. By treating the outer boundary of the RS on sphere surface as a spherical convex hull, two relevant theorems are proposed and the RS envelope is depicted by the computational geometry theory. Based on RS model, the algorithms of intercept window analysis and launch parameters determination are proposed, and numerical simulations are carried out for interceptors with different energy or launch points. Results show that the proposed method can avoid intensive on-line computation and provide an accurate and effective approach for interceptor engagement analysis. The suggested RS model also serves as a ready reference to other related problems such as interceptor effectiveness evaluation and platform disposition.