Reachability-Based Confidence-Aware Probabilistic Collision Detection in Highway Driving

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.

An Algorithm to Construct Concurrent Reachability Graph of Petri Nets

Reachability graph is a very important tool to analyze the dynamic properties of Petri nets, but the concurrent relation of transitions in Petri nets cannot be represented by reachability graph. Petri net is a concurrent system, while reachability graph is a serial one. However, concurrency is a kind of property which is not only very significant but also difficult to be analyzed and controlled. This paper presents the concepts of concurrent reachable marking and concurrent reachable graph in order to represent and analyze the concurrent system. The algorithm constructing concurrent reachable marking set and concurrent reachability graph is also shown so that we can study the response problems among services in a network computing environment and analyze the throughput of the system. The Dining Philosophers Problem, which is a classic problem of describing the management of concurrent resources, is given as an example to illustrate the significance of concurrent reachability graph.

Reachability analysis of switched linear discrete singular systems

This paper studies the reachability problem of the switched linear discrete singular （SLDS） systems. Under the condition that all subsystems are regular, the reachability of the SLDS systems is characterized based on a peculiar repeatedly introduced switching sequence. The necessary and sufficient conditions are obtained for the reachability of the SLDS systems.

Safety Assessment for Autonomous Aerial Refueling Based on Reachability Analysis

Autonomous aerial refueling(AAR)has demonstrated significant benefits to aviation by extending the aircraft range and endurance.It is of significance to assess system safety for autonomous aerial refueling.In this paper,the reachability analysis method is adopted to assess system safety.Due to system uncertainties,the aerial refueling system can be considered as a stochastic system.Thus,probabilistic reachability is considered.Since there is a close relationship between reachability probability and collision probability,the collision probability of the AAR system is analyzed by using reachability analysis techniques.Then,the collision probability is accessed by using the Monte-Carlo experiment method.Finally,simulations demonstrate the effectiveness of the proposed safety assessment method.

Approximate Reachability and Bisimulation Equivalences for Transition Systems

Using Baire metric, this paper proposes a generalized framework of transition system approximation by developing the notions of approximate reachability and approximate bisimulation equivalences. The proposed framework captures the traditional exact equivalence as a special case. Approximate reachability equivalence is coarser than approximate bisimulation equivalence, just like the hierarchy of the exact ones. Both approximate equivalences satisfy the transitive property, consequently, they can be used in transition system approximation.

Combination Reduction:A SYN-Sequence Selection Strategy for Reachability Testing of Concurrent Programs

Reachability testing is an approach to testing concurrent programs, which can systematically exercise every partially ordered SYN-sequence without constructing the static model. In fact, not all the SYN-sequences need to be tested. This paper proposed a SYN-sequence selection strategy for reachability testing, which can reduce the number of SYN-sequences generated without decreasing the effectiveness of detecting programs＇ errors. We described a simple algorithm to implement the strategy, and then discussed several optimizations to the algorithm. Experiments have been carried out in a case study to verify the efficacy of the strategy.

An Optimized Labeling Scheme for Reachability Queries

Answering reachability queries is one of the fundamental graph operations.Existing approaches either accelerate index construction by constructing an index that covers only partial reachability relationship,which may result in performing cost traversing operation when answering a query;or accelerate query answering by constructing an index covering the complete reachability relationship,which may be inefficient due to comparing the complete node labels.We propose a novel labeling scheme,which covers the complete reachability relationship,to accelerate reachability queries processing.The idea is to decompose the given directed acyclic graph(DAG)G into two subgraphs,G1 and G2.For G1,we propose to use topological labels consisting of two integers to answer all reachability queries.For G2,we construct 2-hop labels as existing methods do to answer queries that cannot be answered by topological labels.The benefits of our method lie in two aspects.On one hand,our method does not need to perform the cost traversing operation when answering queries.On the other hand,our method can quickly answer most queries in constant time without comparing the whole node labels.We confirm the efficiency of our approaches by extensive experimental studies using 20 real datasets.

The Analysis of Pingyao Ancient Town Street Spaces and View Spots Reachability by Space Syntax

The Pingyao ancient town is one of the four largest ancient cities in China. This study analyzes street spaces characteristic and view spots reachability of the Pingyao ancient town using space syntax. Then, it is concluded that the integration and reachability of street spaces are relatively higher in the northern ancient town;the accessibility among street spaces is relatively higher in the northeastern ancient town;and most of the ancient town street spaces are very open. Furthermore, the reachability of 14 view spots and their 4 corresponding street spaces is relatively higher in the 20 view spots and their 9 corresponding street spaces. Finally, some suggestions are presented to the tourism development of Pingyao ancient town based on the above conclusions.

Answering reachability queries with ordered label constraints over labeled graphs

Reachability query plays a vital role in many graph analysis tasks.Previous researches proposed many methods to efficiently answer reachability queries between vertex pairs.Since many real graphs are labeled graph,it highly demands Label-Constrained Reachability(LCR)query inwhich constraint includes a set of labels besides vertex pairs.Recent researches proposed several methods for answering some LCR queries which require appearance of some labels specified in constraints in the path.Besides that constraint may be a label set,query constraint may be ordered labels,namely OLCR(Ordered-Label-Constrained Reachability)queries which retrieve paths matching a sequence of labels.Currently,no solutions are available for OLCR.Here,we propose DHL,a novel bloom filter based indexing technique for answering OLCR queries.DHL can be used to check reachability between vertex pairs.If the answers are not no,then constrained DFS is performed.So,we employ DHL followed by performing constrained DFS to answer OLCR queries.We show that DHL has a bounded false positive rate,and it's powerful in saving indexing time and space.Extensive experiments on 10 real-life graphs and 12 synthetic graphs demonstrate that DHL achieves about 4.8-22.5 times smaller index space and 4.6-114 times less index construction time than two state-of-art techniques for LCR queries,while achieving comparable query response time.The results also show that our algorithm can answer OLCR queries effectively.

Matrix expression and reachability analysis of finite automata

In this paper, we propose a matrix-based approach for finite automata and then study the reachability conditions. Both the deterministic and nondeterministic automata are expressed in matrix forms, and the necessary and sufficient conditions on reachability are given using semitensor product of matrices. Our results show that the matrix expression provides an effective computational way for the reachability analysis of finite automata.

Semi-tensor product of matrices approach to reachability of finite automata with application to language recognition

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）.

REACHABILITY/CONTROLLABILITY OF HIGH ORDER MIX-VALUED LOGICAL NETWORKS

This paper addresses the teachability/controllability of high order mix-valued logical control networks by using the semi-tensor product method, and presents some necessary and sufficient conditions for the reachability/controllability. The high order mix-valued logical network is converted into an algebraic form first, baaed on which the reachability/controllability of the system is then investigated, and several necessary and sufficient conditions are established. The study of several illustrative examples shows that our new method is very effective in dealing with the reachability/controllability of high order mix-valued logical control networks.

An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs

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.

Adding regular expressions to graph reachability and pattern queries

It is increasingly common to find graphs in which edges are of different types, indicating a variety of relation- ships. For such graphs we propose a class of reachability queries and a class of graph patterns, in which an edge is specified with a regular expression of a certain form, ex- pressing the connectivity of a data graph via edges of var- ious types. In addition, we define graph pattern matching based on a revised notion of graph simulation. On graphs in emerging applications such as social networks, we show that these queries are capable of finding more sensible informa- tion than their traditional counterparts. Better still, their in- creased expressive power does not come with extra complex- ity. Indeed, （1） we investigate their containment and mini- mization problems, and show that these fundamental prob- lems are in quadratic time for reachability queries and are in cubic time for pattern queries. （2） We develop an algorithm for answering reachability queries, in quadratic time as for their traditional counterpart. （3） We provide two cubic-time algorithms for evaluating graph pattern queries, as opposed to the NP-completeness of graph pattern matching via subgraph isomorphism. （4） The effectiveness and efficiency of these al- gorithms are experimentally verified using real-life data and synthetic data.

Reduction Method for Reachability Analysis of Petri Nets

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.

Answering Reachability Queries on Incrementally Updated Graphs by Hierarchical Labeling Schema

We proposed a novel solution schema called the Hierarchical Labeling Schema （HLS） to answer reachability queries in directed graphs. Different from many existing approaches that focus on static directed acyclic graphs （DAGs）, our schema focuses on directed cyclic graphs （DCGs） where vertices or arcs could be added to a graph incrementally. Unlike many of the traditional approaches, HLS does not require the graph to be acyclic in constructing its index. Therefore, it could, in fact, be applied to both DAGs and DCGs. When vertices or arcs are added to a graph, the HLS is capable of updating the index incrementally instead of re-computing the index from the scratch each time, making it more efficient than many other approaches in the practice. The basic idea of HLS is to create a tree for each vertex in a graph and link the trees together so that whenever two vertices are given, we can immediately know whether there is a path between them by referring to the appropriate trees. We conducted extensive experiments on both real-world datasets and synthesized datasets. We compared the performance of HLS, in terms of index construction time, query processing time and space consumption, with two state-of-the-art methodologies, the path-tree method and the 3-hop method. We also conducted simulations to model the situation when a graph is updated incrementally. The performance comparison of different algorithms against HLS on static graphs has also been studied. Our results show that HLS is highly competitive in the practice and is particularly useful in the cases where the graphs are updated frequently.

Fast solution to the free return orbit's reachable domain of the manned lunar mission by deep neural network

It is important to calculate the reachable domain(RD)of the manned lunar mission to evaluate whether a lunar landing site could be reached by the spacecraft. In this paper, the RD of free return orbits is quickly evaluated and calculated via the classification and regression neural networks. An efficient databasegeneration method is developed for obtaining eight types of free return orbits and then the RD is defined by the orbit’s inclination and right ascension of ascending node(RAAN) at the perilune. A classify neural network and a regression network are trained respectively. The former is built for classifying the type of the RD, and the latter is built for calculating the inclination and RAAN of the RD. The simulation results show that two neural networks are well trained. The classification model has an accuracy of more than 99% and the mean square error of the regression model is less than 0.01°on the test set. Moreover, a serial strategy is proposed to combine the two surrogate models and a recognition tool is built to evaluate whether a lunar site could be reached. The proposed deep learning method shows the superiority in computation efficiency compared with the traditional double two-body model.

Reachability of Patterned Conditional Pushdown Systems

Conditional pushdown systems (CPDSs) extend pushdown systems by associating each transition rule with a regular language over the stack alphabet. The goal is to model program verification problems that need to examine the run-time call stack of programs. Examples include security property checking of programs with stack inspection, compatibility checking of HTML5 parser specifications, etc. Esparza et al. proved that the reachability problem of CPDSs is EXPTIME-complete, which prevents the existence of an algorithm tractable for all instances in general. Driven by the practical applications of CPDSs, we study the reachability of patterned CPDS (pCPDS) that is a practically important subclass of CPDS, in which each transition rule carries a regular expression obeying certain patterns. First, we present new satura-tion algorithms for solving state and configuration reachability of pCPDSs. The algorithms exhibit the exponential-time complexity in the size of atomic patterns in the worst case. Next, we show that the reachability of pCPDSs carrying sim-ple patterns is solvable in fixed-parameter polynomial time and space. This answers the question on whether there exist tractable reachability analysis algorithms of CPDSs tailored for those practical instances that admit efficient solutions such as stack inspection without exception handling. We have evaluated the proposed approach, and our experiments show that the pattern-driven algorithm steadily scales on pCPDSs with simple patterns.

Navigability and Reachability Index for Emergency Navigation Systems Using Wireless Sensor Networks

Emergency navigation with a large number of sensors can serve as a safety service in emergencies. Recent studies have focused on navigation protocols to safely guide people to exits while helping them avoid hazardous areas. However, those approaches are not applicable in all circumstances. Both the dynamics of the environment and the mobility of users are key challenges for the efficiency and effectiveness of navigation protocols. The concepts of navigability and reachability are used to evaluate three typical navigation approaches. A large number of simulation results show that these two indicators effectively identify the performance levels of navigation protocols in changing environments.

Modeling and reachability analysis of synchronizing transitions bounded Petri net systems based upon semi-tensor product of matrices

The reachability problem of synchronizing transitions bounded Petri net systems （BPNSs） is investigated in this paper by constructing a mathematical model for dynamics of BPNS. Using the semi-tensor product （STP） of matrices, the dynamics of BPNSs, which can be viewed as a combination of several small bounded subnets via synchronizing transitions, are described by an algebraic equation. When the algebraic form for its dynamics is established, we can present a necessary and sufficient condition for the reachability between any marking （or state） and initial marking. Also, we give a corresponding algorithm to calculate all of the transition paths between initial marking and any target marking. Finally, an example is shown to illustrate proposed results. The key advantage of our approach, in which the set of reachable markings of BPNSs can be expressed by the set of reachable markings of subnets such that the big reachability set of BPNSs do not need generate, is partly avoid the state explosion problem of Petri nets （PNs）.