Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a manner that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct component specifications that implement a given specification when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. We parametrize the information flow between components by introducing parameters that select whether each variable is visible to a component. The decomposition algorithm identifies which variables can be hidden while preserving realizability and ensuring correct composition, and these are eliminated from component specifications by quantification and conversion of binary decision diagrams to formulas. The resulting specifications describe component viewpoints with full information with respect to the remaining variables, which is essential for tractable algorithmic synthesis of implementations. The specifications are written in TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We define an operator for forming open systems from closed systems, based on a variant of the “while-plus” operator. This operator simplifies the writing of specifications that are realizable without being vacuous. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We show with examples how the method can be applied to obtain contracts that formalize the hierarchical structure of system design.

This paper extends the piggyback algorithm to enlarge the set of liveness properties it can verify. Its extension is motivated by an attempt to express in logic the counterexamples it can detect and relate them to bounded liveness. The original algorithm is based on parallel breadth-first search and piggybacking of accepting states that are deleted after counting a fixed number of transitions. The main improvement is obtained by renewing the counter of transitions when the same accepting states are visited in the negated property automaton. In addition, we describe piggybacking of multiple states in either sets (exact) or Bloom filters (lossy but conservative), and use of local searches that attempt to connect cycles fragmented among processing cores. Finally it is proved that accepting cycle detection is in NC in the size of the product automaton's entire state space, including unreachable states.

This work proposes a motion planning method based on the construction of a roadmap connecting the critical points of a potential field or a distance function. It aims to overcome the limitation of potential field methods due to local minima caused by concave obstacles. The roadmap is incrementally constructed by a two-step procedure. Starting from a minimum, adjacent saddle-points are found using a local saddle-point search method. Then, the new saddle-points are connected to the minima by gradient descent. A numerical continuation algorithm from the computational chemistry literature is used to find saddle-points. It traces the valleys of the potential field, which are gradient extremal paths, defined as the points where the gradient is an eigenvector of the Hessian matrix. The definition of gradient bisectors is also discussed. The presentation conclude simulations in cluttered environments.

We extend Navigation Functions (NF) to worlds of more general geometry and topology. This is achieved without the need for diffeomorphisms, by direct definition in the geometrically complicated configuration space. Every obstacle boundary point should be partially sufficiently curved. This requires that at least one principal normal curvature be sufficient. A normal curvature is termed sufficient when the tangent sphere with diameter the associated curvature radius is a subset of the obstacle. Examples include ellipses with bounded eccentricity, tori, cylinders, one-sheet hyperboloids and others. Our proof establishes the existence of appropriate tuning for this purpose. Direct application to geometrically complicated cases is illustrated through nontrivial simulations.

This paper proposes a method to construct Navigation Functions (NF) from experimental trajectories in an unknown environment. We want to approximate an unknown obstacle function and then use it within an NF. When navigating the same destinations with the experiments, this NF should produce the same trajectories as the experiments. This requirement is equivalent to a partial differential equation (PDE). Solving the PDE yields the unknown obstacle function, expressed with spline basis functions. We apply this new method to anthropomorphic grasping, producing automatic trajectories similar to the observed ones. The grasping experiments were performed for a set of different objects, Principal Component Analysis (PCA) allows reduction of the configuration space dimension, where the learning NF method is then applied.