Reachability and optimal control for linear hybrid automata: a quantifier elimination approach

This paper considers an optimal control problem for linear hybrid automata (LHA). First, we present a controller synthesis algorithm based on reachability analysis. The algorithm computes the maximal initial set from which the controller drives the system to a given target set. It is shown that, using quantifier elimination (QE), an under-approximation of the maximal reachable set can be derived. Next, a weighted time-optimal control problem is solved by transforming it into a constrained optimization problem whose constraints are a set of inequalities with quantifiers. Quantifier elimination (QE) techniques are employed in order to derive the quantifier free inequalities that are shown to be linear. Thus, the optimal cost is obtained using linear programming. For any state belonging to the maximal initial set the optimal switching times and the optimal continuous control inputs are computed. These are used in order to derive a hybrid controller which is optimal with respect to the cost function. Our results are applied to an air traffic management example which is of practical interest.     

An incremental algorithm for DLO quantifier elimination via constraint propagation

The first-order logical theory of dense linear order has long been known to admit quantifier elimination. This paper develops an explicit algorithm that yields an equivalent quantifier free form of its input formula. This algorithm performs existential quantifier elimination via constraint propagation. The result is computed incrementally using functional programming techniques. This approach may be of interest in implementing query languages for constraint databases.     

Time-optimal control for discrete-time hybrid automata

In this paper, the problem of time-optimal control for hybrid systems with discrete-time dynamics is considered. The hybrid controller steers all trajectories starting from a maximal set to a given target set in minimum time. We derive an algorithm that computes this maximal winning set. Also, algorithms for the computation of level sets associated with the value function rather than the value function itself are presented. We show that by solving the reachability problem for the discrete time hybrid automata we obtain the time optimal solution as well. The control synthesis is subject to hard constraints on both control inputs and states. For linear discrete-time dynamics, linear programming and quantifier elimination techniques are employed for the backward reachability analysis. Emphasis is given on the computation of operators for non-convex sets using an extended convex hull approach. A two-tank example is considered in order to demonstrate the techniques of the paper.     

Quantifier elimination in automatic loop parallelization

We present an application of quantifier elimination techniques in the automatic parallelization of nested loop programs. The technical goal is to simplify affine inequalities whose coefficients may be unevaluated symbolic constants. The values of these so-called structure parameters are determined at run time and reflect the problem size. Our purpose here is to make the research community of quantifier elimination, in a tutorial style, aware of our application domain–loop parallelization–and to highlight the role of quantifier elimination, as opposed to alternative techniques, in this domain. Technically, we focus on the elimination method of Weispfenning.     

Linear Quantifier Elimination

This paper presents verified quantifier elimination procedures for dense linear orders (two of them novel), for real and for integer linear arithmetic. All procedures are defined and verified in the theorem prover Isabelle/HOL, are executable and can be applied to HOL formulae themselves (by reflection). The formalization of the different theories is highly modular.     

Linear Problems in Valued Fields

A first-order formula over a valued field is called linear if it contains no products or reciprocals of quantified variables. We give quantifier elimination procedures based on test term ideas for linear formulas in the following classes of valued fields: discretely valued fields, discretely valued fields with a Z -group as the value group over a language containing predicates stating divisibility in the value group, and non-discretely valued fields. From the existence of the elimination procedures, it follows that the corresponding decision problems are in an alternating single exponential time-space (Berman) complexity class. We exhibit the substructure completeness of the considered classes of valued fields w.r.t. linear formulas.     

Quantifier-free encoding of invariants for hybrid systems

Hybrid systems are a clean modeling framework for embedded systems, which feature integrated discrete and continuous dynamics. A well-known source of complexity comes from the time invariants, which represent an implicit quantification of a constraint over all time points of a continuous transition. Emerging techniques based on Satisfiability Modulo Theory (SMT) have been found promising for the verification and validation of hybrid systems because they combine discrete reasoning with solvers for first-order theories. However, these techniques are efficient for quantifier-free theories and the current approaches have so far either ignored time invariants or have been limited to hybrid systems with linear constraints. In this paper, we propose a new method that encodes a class of hybrid systems into transition systems with quantifier-free formulas. The method does not rely on expensive quantifier elimination procedures. Rather, it exploits the sequential nature of the transition system to split the continuous evolution enforcing the invariants on the discrete time points. This way, we can encode all hybrid systems whose invariants can be expressed in terms of polynomial constraints. This pushes the application of SMT-based techniques beyond the standard linear case.     

Out of order quantifier elimination for Standard Quantified Linear Programs

In this paper, we present an out of order quantifier elimination algorithm for a class of Quantified Linear Programs (QLPs) called Standard Quantified Linear Programs (SQLPs). QLPs in general and SQLPs in particular are extremely useful constraint logic programming structures that find wide applicability in the modeling of real-time schedulability specifications; see Subramani [Subramani, K., 2005a. A comprehensive framework for specifying clairvoyance, constraints and periodicity in real-time scheduling. The Computer Journal 48 (3), 259–272]. Consequently any algorithmic advance in their solution has a strong practical impact. Prior to this work, the only known approaches to the solution of QLPs involved sequential variable elimination; see Subramani [Subramani, K., 2003b. An analysis of quantified linear programs. In: Calude, C.S. et al. (Eds.), Proceedings of the 4th International Conference on Discrete Mathematics and Theoretical Computer Science. DMTCS. In: Lecture Notes in Computer Science, vol. 2731. Springer-Verlag, pp. 265–277]. In the sequential approach, the innermost quantified variable is eliminated first, followed by the variable which then becomes the innermost quantified variable and so on, until we are left with a single variable from which the satisfiability of the original formula is easily deduced. This approach is applicable in both discrete and continuous domains; however, it is to be noted that the logic demanding the sequential approach requires that the variables are discrete-valued. To the best of our knowledge, the necessity for sequential elimination over continuous-valued variables has not been investigated in the literature. The techniques used in the development of our elimination algorithm may find applications in domains such as classical logic and finite model theory. The final aspect of our research concerns the structure-preserving nature of the algorithm that we introduce here; in general, it is not known whether discrete domains admit such elimination procedures.     

Subsumption and indexing in constraint query languages with linear arithmetic constraints

Bottom-up evaluation of a program-query pair in a constraint query language (CQL) starts with the facts in the database and repeatedly applies the rules of the program, in iterations, to compute new facts, until we have reached a fixpoint. Checking if a fixpoint has been reached amounts to checking if any new facts were computed in an iteration. Such a check also enhances efficiency in that subsumed facts can be discarded, and not be used to make any further derivations in subsequent iterations, if we use Semi-naive evaluation. We show that the problem of subsumption in CQLs with linear arithmetic constraints is co-NP complete, and present a deterministic algorithm, based on the divide and conquer strategy, for this problem. We also identify polynomial-time sufficient conditions for subsumption and non-subsumption in CQLs with linear arithmetic constraints. We adapt indexing strategies from spatial databases for efficiently indexing facts in such a CQL: such indexing is crucial for performance in the presence of large databases. Based on a recent algorithm by C. Lassez and J.-L. Lassez for quantifier elimination, we present an incremental version of the algorithm to check for subsumption in CQLs with linear arithmetic constraints.This work was supported by a David and Lucile Packard Foundation Fellowship in Science and Engineering, a Presidential Young Investigator Award, with matching grants from the Digital Equipment Corporation, Tandem and Xerox, and NSF Grant No. IRI-9011563.     

Reduction and Quantifier Elimination Techniques for Program Validation

We study the automatic verification of programs with infinite or parameterized state space. This paper presents methods allowing the transformation of some second-order formulas expressing Hoare triples into equivalent formulas expressed in a weaker but decidable logic. Two techniques are considered: quantifier elimination and reduction to a finite domain. We illustrate these techniques on the validation of memory coherency protocols expressed in Unity.     

碰撞问题中的量词消去算法的并行化研究

机器人技术中的碰撞问题可以被表示成量词消去问题，但由于有些碰撞问题的复杂性使得这些问题在单个微机上求解需要花费的时间很长或者根本就解不出来。本文提出了基于分布Maple系统下量词消去算法的并行化．并针对分布Maple系统的特点以及算法的特点，通过实例分析，给出了两种并行策略，以达到在Maple软件环境下提高处理器利用率，提高量词消去算法的效率的目的。     

Quantifier elimination by dependency sequents

We consider the problem of existential quantifier elimination for Boolean CNF formulas. We present a new method for solving this problem called derivation of dependency-sequents (DDS). A dependency-sequent (D-sequent) is used to record that a set of variables is redundant under a partial assignment. We introduce the join operation that produces new D-sequents from existing ones. We show that DDS is compositional, i.e., if our input formula is a conjunction of independent formulas, DDS automatically recognizes and exploits this information. We introduce an algorithm based on DDS and present experimental results demonstrating its potential.     

Guaranteed set-point computation with application to the control of a sailboat

The problem of characterizing in a guaranteed way the set of all feasible set-points of a control problem is known to be difficult. In the present work, the problem to be solved involves non-linear equality constraints with variables affected by logical quantifiers. This problem is not solvable by current symbolic methods like quantifier elimination, which is commonly used for solving this class of problems. We propose the utilization of guaranteed set-computation techniques based on interval analysis, in particular a solver referred to as Quantified Set Inversion (QSI). As an application example, the problem of simultaneously controlling the speed and the orientation of a sailboat is presented. For this purpose, the combination of QSI solver and feedback linearization techniques is employed.     

Propagating systems of dense linear integer constraints

In interval propagation approaches to solving nonlinear constraints over reals it is common to build stronger propagators from systems of linear equations. This, as far as we are aware, is not pursued for integer finite domain propagation. In this paper we show how we use interval Gauss–Jordan elimination to build stronger propagators for an integer propagation solver. In a similar fashion we present an interval Fourier elimination preconditioning technique to generate redundant linear constraints from a system of linear inequalities. We show how to convert the resulting interval propagators into integer propagators. This allows us to use existing integer solvers. We give experiments that show how these preconditioning techniques can improve propagation performance on dense systems.     

Generation of injective and reversible modular mappings

A modular mapping consists of a linear transformation followed by modulo operations. It is characterized by a transformation matrix and a vector of moduli, called the modulus vector. Modular mappings are useful to derive parallel versions of algorithms with commutative operations and algorithms intended for execution on processor arrays with toroidal networks. In order to preserve algorithm correctness, modular mappings must be injective. Results of previous work characterize injective modular mappings of rectangular index sets. This paper provides a technique to generate modular mappings that satisfy these injective conditions and extends the results to general index sets. For an n-dimensional rectangular index set, the technique has O(n/sup 2/n!) complexity. To facilitate generation of efficient code, modular mappings must also be reversible (i.e., have easily described inverses). An O(n/sup 2/) method is provided to generate reversible modular mappings. This method reduces the search space by fixing entries of the modulus vector while attempting to minimize the number of entries to exclude few solutions. For general index sets defined by linear inequalities, injectivity can be checked by formulating and solving a set of linear inequalities. A modified Fourier-Motzkin elimination is proposed to solve these inequalities. To generate an injective modular mapping of an index set defined by linear inequalities, this paper proposes a technique that attempts to minimize the values of the entries of the modulus vector. Several examples are provided to illustrate the application of the above mentioned methods, including the case of BLAS routines.     

Simple CAD Construction and its Applications

This paper presents a method for the simplification of truth-invariant cylindrical algebraic decompositions (CADs). Examples are given that demonstrate the usefulness of the method in speeding up the solution formula construction phase of the CAD-based quantifier elimination algorithm. Applications of the method to the construction of truth-invariant CADs for very large quantifier-free formulas and quantifier elimination of non-prenex formulas are also discussed.     

Smashing peacocks further: drawing quasi-trees from biconnected components

We extend the popular force-directed approach to network (or graph) layout to allow separation constraints, which enforce a minimum horizontal or vertical separation between selected pairs of nodes. This simple class of linear constraints is expressive enough to satisfy a wide variety of application-specific layout requirements, including: layout of directed graphs to better show flow; layout with non-overlapping node labels; and layout of graphs with grouped nodes (called clusters). In the stress majorization force-directed layout process, separation constraints can be treated as a quadratic programming problem. We give an incremental algorithm based on gradient projection for efficiently solving this problem. The algorithm is considerably faster than using generic constraint optimization techniques and is comparable in speed to unconstrained stress majorization. We demonstrate the utility of our technique with sample data from a number of practical applications including gene-activation networks, terrorist networks and visualization of high-dimensional data     

An Approximation Framework for Solvers and Decision Procedures

We consider the problem of automatically and efficiently computing models of constraints, in the presence of complex background theories such as floating-point arithmetic. Constructing models, or proving that a constraint is unsatisfiable, has various applications, for instance for automatic generation of test inputs. It is well-known that a naïve encoding of constraints into simpler theories (for instance, bit-vectors or propositional logic) often leads to a drastic increase in size, or that it is unsatisfactory in terms of the resulting space and runtime demands. We define a framework for systematic application of approximations in order to improve performance. Our method is more general than previous techniques in the sense that approximations that are neither under- nor over-approximations can be used, and it shows promising performance on practically relevant benchmark problems.     

改进的蒙哥马利算法及其模乘法器实现

模乘运算的速度决定了公钥加密系统和众多通信系统的系统性能。通过分析Walter等学者对蒙哥马利算法的研究成果,得到运算精简基2-MMM算法,实现基于运算精简算法的线性脉动阵列模乘法器。在验证改进算法正确性后,对模乘法器进行功能仿真和综合。用TSMC 0.18 μm标准单元库综合,可以工作在200 MHz时钟下,等效单元为42 k门,完成1 024 bit模乘法运算需