One of the most fundamental problems in computer science is the reachability problem: Given a directed graph and two vertices s and t, can sreach t via a path? We revisit existing techniques and ...combine them with new approaches to support a large portion of reachability queries in constant time using a linear-sized reachability index. Our new algorithm O’Reach can be easily combined with previously developed solutions for the problem or run standalone.In a detailed experimental study, we compare a variety of algorithms with respect to their index-building and query times as well as their memory footprint on a diverse set of instances. Our experiments indicate that the query performance often depends strongly not only on the type of graph but also on the result, i.e., reachable or unreachable. Furthermore, we show that previous algorithms are significantly sped up when combined with our new approach in almost all scenarios. Surprisingly, due to cache effects, a higher investment in space doesn’t necessarily pay off: Reachability queries can often be answered even faster than single memory accesses in a precomputed full reachability matrix.
This article introduces a new class of sets, called constrained zonotopes, that can be used to enclose sets of interest for estimation and control. The numerical representation of these sets is ...sufficient to describe arbitrary convex polytopes when the complexity of the representation is not limited. At the same time, this representation permits the computation of exact projections, intersections, and Minkowski sums using very simple identities. Efficient and accurate methods for computing an enclosure of one constrained zonotope by another of lower complexity are provided. The advantages and disadvantages of these sets are discussed in comparison to ellipsoids, parallelotopes, zonotopes, and convex polytopes in halfspace and vertex representations. Moreover, extensive numerical comparisons demonstrate significant advantages over other classes of sets in the context of set-based state estimation and fault detection.
This work presents a method of efficiently computing inner and outer approximations of forward reachable sets for nonlinear control systems with changed dynamics and control authority, given an a ...priori computed reachable set for the nominal system. The method functions by shrinking or inflating a precomputed reachable set based on prior knowledge of the system's trajectory deviation growth dynamics, depending on whether an inner approximation or outer approximation is desired. These dynamics determine an upper bound on the minimal deviation between two trajectories emanating from the same point that are generated by control inputs from the nominal and diminished set of control inputs, respectively. The dynamics depend on the given Hausdorff distance bound between the nominal set of admissible controls and the possibly unknown impaired space of admissible controls. Because of its computational efficiency compared to direct computation of the off-nominal reachable set, this procedure can be applied to on-board fault-tolerant path planning and failure recovery. In addition, the proposed algorithm does not require convexity of the reachable sets unlike our previous work, thereby making it suitable for general use. We raise a number of implementational considerations for our algorithm, and we present three illustrative examples, namely an application to the heading dynamics of a ship, a lower triangular dynamical system, and a system of coupled linear subsystems.
We propose a novel formulation for approximating reachable sets through a minimum discounted reward optimal control problem. The formulation yields a continuous solution that can be obtained by ...solving a Hamilton-Jacobi equation. Furthermore, the numerical approximation to this solution is the unique fixed-point to a contraction mapping. This allows for more efficient solution methods that are not applicable under traditional formulations for solving reachable sets. Lastly, this formulation provides a link between reinforcement learning and learning reachable sets for systems with unknown dynamics, allowing algorithms from the former to be applied to the latter. We use two benchmark examples, double integrator, and pursuit-evasion games, to show the correctness of the formulation as well as its strengths in comparison to previous work.
To solve some scheduling problems of batch processes based on timed Petri net models, timed extended reachability graphs (TERGs) and approximated TERGs can be used. Such graphs abstract temporal ...specifications and represent parts of timed languages. By exploring the feasible trajectories in a TERG, optimal schedules can be obtained with respect to the makespans of batch processes that are modeled by timed Petri nets. Nevertheless, the rapid growth of the number of states in a TERG makes the problem intractable for large systems. In this paper, we improve the existing clustering TERG approach, and we make it suitable for large sized batch processes. We also enlarge a systematic approach to model batch processes with timed Petri nets. Finally, a comprehensive example of scheduling problem is studied for an archetypal chemical production plant in order to illustrate the efficiency of the proposed approach.
•The scheduling problem of batch chemical processes is formalized with timed Petri net models.•The timed extended reachability graph of the model is combined with a hierarchical clustering algorithm to develop a new time graph with a reduced size, namely ClusTERG.•The approximation error of this ClusTERG is far less than other approximations.•Such an approach is used to obtain near-optimal schedules of a batch process.
Subcubic certificates for CFL reachability Chistikov, Dmitry; Majumdar, Rupak; Schepper, Philipp
Proceedings of ACM on programming languages,
01/2022, Volume:
6, Issue:
POPL
Journal Article
Peer reviewed
Open access
Many problems in interprocedural program analysis can be modeled as the context-free language (CFL) reachability problem on graphs and can be solved in cubic time. Despite years of efforts, there are ...no known truly sub-cubic algorithms for this problem. We study the related
certification
task: given an instance of CFL reachability, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that, in both scenarios, there exist succinct certificates (
O
(
n
2
) in the size of the problem) and these certificates can be checked in subcubic (matrix multiplication) time. The certificates are based on grammar-based compression of paths (for reachability) and on invariants represented as matrix inequalities (for non-reachability). Thus, CFL reachability lies in nondeterministic and co-nondeterministic
subcubic
time.
A natural question is whether faster algorithms for CFL reachability will lead to faster algorithms for combinatorial problems such as Boolean satisfiability (SAT). As a consequence of our certification results, we show that there cannot be a fine-grained reduction from SAT to CFL reachability for a conditional lower bound stronger than
n
ω
, unless the nondeterministic strong exponential time hypothesis (NSETH) fails. In a nutshell, reductions from SAT are unlikely to explain the cubic bottleneck for CFL reachability.
Our results extend to related subcubic equivalent problems: pushdown reachability and 2NPDA recognition; as well as to all-pairs CFL reachability. For example, we describe succinct certificates for pushdown non-reachability (inductive invariants) and observe that they can be checked in matrix multiplication time. We also extract a new hardest 2NPDA language, capturing the “hard core” of all these problems.
This paper investigates interval estimation methods for discrete-time linear time-invariant systems. We propose a novel interval estimation method by integrating robust observer design with ...reachability analysis. By introducing H ∞ design into interval estimation, the proposed method is effective in improving the accuracy of interval estimation. Moreover, the comparisons and relationships between the existing methods and the proposed method are discussed in detail. Finally, simulation results are presented to demonstrate the effectiveness of the proposed method.
This article explores reach set computations for perturbed delay differential equations (DDEs). The perturbed DDEs of interest in this article is a class of DDEs whose dynamics are subject to ...perturbations, and their solutions feature the local homeomorphism property with respect to initial states. Membership in this class of perturbed DDEs is determined by conducting sensitivity analysis of solution mappings with respect to initial states to impose a bound constraint on the time-lag term. The homeomorphism property of solutions to such class of perturbed DDEs enables us to construct over- and underapproximations of reach sets by performing reachability analysis on just the boundaries of their permitted initial sets, thereby permitting an extension of reach set computation methods for ordinary differential equations to perturbed DDEs. Three examples demonstrate the performance of our approach.
PDF
