Search

Contrary to state feedback control, the design of static output feedback is quite challenging even for linear time- invariant state-space systems. In this paper we consider the eigenvalue placement from an algebraic point of view. Not all eigenvalues necessarily have to be placed, i.e., we consider a partial eigenvalue placement. In addition, the stability of the remaining dynamics must be ensured. We also exploit degrees of freedom in the controller design of multivariable systems in order to minimize suitable matrix norms of the feedback gain. The required computations are carried out using methods from algebraic geometry such as Grobner bases and quantifier elimination.

The Duffing system and the nonlinear pendulum are a comparatively simple dynamical systems that can generate complex dynamics such as subharmonics, intermittency and chaos. Both system has been used to model a variety of technical systems, where nonlinear oscillations occur. The dynamics can usually not be computed analytically but only simulated numerically. In this paper we provide a method to compute analytically exact bounds on the trajectories of the excited Duffing system and the nonlinear pendulum. These computations are carried out using quantifier elimination.

Lyapunov’s second method is the most commonly used stability test for nonlinear systems. While Lyapunov’s approach requires that the time-derivative of an energy-like function is strictly positive or negative, the generalisation by LaSalle allows the sign to become zero. With the latter theorem convergence to an invariant set contained in the zero-set of the time-derivative can be shown. In this contribution we propose a method to compute such an invariant set for polynomial systems using algebraic geometry. This is done by extending the concept of Lie derivatives on polynomial ideals. The proposed method is illustrated on some simple examples.

In this contribution we investigate local and global observability of multi-variable polynomial systems. Nonlinear observability is based on the concept of indistinguishability, for which we examine the observability map regarding to injectivity. To carry out the analysis we use a computation technique called quantifier elimination. Our approach can be applied even if the observability analysis requires more components of the observability map than the dimension of the state space. The observability analysis is illustrated on several example systems.

Advances in the field of Machine Learning and Deep Neural Networks (DNNs) has enabled rapid development of sophisticated and autonomous systems. However, the inherent complexity to rigorously assure the safe operation of such systems hinders their real-world adoption in safety-critical domains such as aerospace and medical devices. Hence, there is a surge in interest to explore the use of advanced mathematical techniques such as formal methods to address this challenge. In fact, the initial results of such efforts are promising. Along these lines, we propose the use of quantifier elimination (QE) - a formal method technique, as a complimentary technique to the state-of-the-art static analysis and verification procedures. Using an airborne collision avoidance DNN as a case example, we illustrate the use of QE to formulate the precise range forward propagation through a network as well as analyze its robustness. We discuss the initial results of this ongoing work and explore the future possibilities of extending this approach and/or integrating it with other approaches to perform advanced safety assurance of DNNs.

Assuring passivity of a closed loop control system is an important issue for the synthesis of the systems. In the present study, a new approach is proposed in order to determine the controller and system parameter spaces that guarantee the passivity of a given nonlinear input affine MIMO system. The utilized parameter space mapping is solving the classical passivity conditions by quantifier elimination. Therefore, the proposed method ensures the passivity of a system with respect to whole classes of function candidates as storage functions, instead of testing the passivity with respect to a single particular storage function. By using the proposed method, the overall computational complexity can be reduced significantly (in comparison to Lyapunov based approaches) by subdividing systems into subsystems and examine their passivity individually. Three benchmark case studies are discussed at the end of the present study in order to verify the effectiveness and correctness of the proposed method.

Cylindrical Algebraic Decomposition (CAD) is a key tool in computational algebraic geometry, particularly for quantifier elimination over real-closed fields. However, it can be expensive, with worst case complexity doubly exponential in the size of the input. Hence it is important to formulate the problem in the best manner for the CAD algorithm. One possibility is to precondition the input polynomials using Groebner Basis (GB) theory. Previous experiments have shown that while this can often be very beneficial to the CAD algorithm, for some problems it can significantly worsen the CAD performance.In the present paper we investigate whether machine learning, specifically a support vector machine (SVM), may be used to identify those CAD problems which benefit from GB preconditioning. We run experiments with over 1000 problems (many times larger than previous studies) and find that the machine learned choice does better than the human-made heuristic.

© 2016 IEEE. A method based on a quantifier elimination algorithm is suggested for obtaining explicit model predictive control (MPC) laws for linear time invariant systems with quadratic objective and polytopic constraints. The structure of the control problem considered allows Weispfenning's 'quantifier elimination by virtual substitution' algorithm to be used. This is applicable to first order formulas in which quantified variables appear at most quadratically. It has much better practical computational complexity than general quantifier elimination algorithms, such as cylindrical algebraic decomposition. We show how this explicit MPC solution, together with Weispfenning's algorithm, can be used to check recursive feasibility of the system, for both nominal and disturbed systems. Extension to cases beyond linear MPC using Weispfenning's algorithm is part of future work.

The controller design problem to stabilize a linear time-invariant state-space system by static state feedback has been solved decades ago. Combining the static state feedback with a state observer one obtains a dynamic output feedback control law. Contrary to that, the design problem of static output feedback stabilization is significantly more challenging. In this paper, we discuss the existence and the computation of stabilizing static output feedback control gains. Our approach allows additional specifications regarding the eigenvalues of the closed-loop system.

We present our work on integration of quantifier elimination (QE) technique with model checking and compositional verification. We begin by showing how quantifier elimination problems arise in these applications. In a k-induction based model checking approach, the verification problems of the base and inductive steps can be reduced to the QE problems in which all the variables are existentially quantified. It follows that a k-induction based model checker can be extended with QE tools to provide back-end solver options. Our implementation of integrating the QE tool Redlog with the model-checker JKind showed the successful resolution of a non-linear computation (emanating from a fuzzy logic operation) that the SMT-solver supported JKind was unable to resolve. Thus the QE tool provides a parallel option to the model-checker. The integrations of the QE tool Redlog with the model-checker JKind has been completed by us, and relies on writing the SMT-to-Redlog translator. On the other hand, in compositional verification, the goal is to prove a system level assume-guarantee style contract from the given component level contracts. The existing compositional verification tool AGREE tries to sequentially prove that each component’s assumption is satisfied by the system assumption and other components’ guarantees, following which the conjunction of all component contracts and system assumption is used to verify the system guarantee. In contrast, we propose a QE-based approach to derive, in a single step, the strongest system contract, from which any postulated system contract can be verified by performing a simple implication verification from the former to the later. We show how the compositional reasoner AGREE can be strengthened through its integration with the QE tool Redlog. We implemented our above approaches in a new prototype tool called ReLIC (Reduced Logic Inference for Composition) and demonstrated it through an illustrative example.

The generalization of the classical nonlinear stability theory on systems with control inputs or disturbances naturally leads to the concept of input-to-state stability (ISS). Determining the ISS property for a given system is generally non-trivial, especially if it involves unknown or design parameters. To this end, in the present paper we present an algebraic method based on automated quantifier elimination (QE) procedures. Thereby we invoke parametrized ISS-Lyapunov functions. As a result, we obtain boundaries in the space of the unknown parameters, guaranteeing the ISS property. The proposed procedure is illustrated by three numerical examples.

The static state feedback controller design, which achieves a desired behavior of the closed loop system, was solved in linear control theory decades ago. This is not true for static output feedback controller design, which is still an open problem. Here an approach is presented which handles the existence and design problem using quantifier elimination methods. Our approach allows the formal verification of arbitrary eigenvalue placement and enables the construction of controllers which lead to specified dynamic behavior. The design method is illustrated on examples known from literature.

A computational approach of feasible regions for parameter-dependent Lyapunov functions for linear systems based on real-root-classification (RRC) is proposed in this paper. We refer to such Lyapunov functions as feasible if there exists a parameter set that guarantees the existence of a Lyapunov function. In this sense, the stability of parameter-dependent linear ordinary differential equations (ODEs) and differential algebraic equations (DAEs) is considered. To this end, the existence condition of Lyapunov functions is given in form of an algebraic condition by means of a quantifier elimination (QE) formulation. We apply RRC to solve the QE problem to obtain algebraic necessary and sufficient existence conditions. Several numerical examples demonstrate that this approach produces non-conservative stability regions in the parameter space.

Boolean functional synthesis allows the automated construction of Boolean functions from declarative specifications. BDD-based techniques for this problem can be very efficient when the specification can be compactly represented by a BDD, but this is not always possible. In model checking, a way around this problem has been found by using factored representations, where formulas are represented as a conjunction of subformulas, each encoded individually as a BDD. We show how techniques and heuristics for quantifier elimination on factored formulas can also be lifted to perform synthesis, and show that this approach allows the synthesis of many problem instances that are intractable when represented by a single BDD. We compare our approach to other tools for Boolean synthesis that are not BDD-based. Our empirical evaluation shows that, while no approach dominates across the board, our tool outperforms other tools on several problem instances.

Explicit Runge Kutta (ERK) methods are well known for numerical solutions of initial value problems. Since the stability function of any ERK scheme is a polynomial, these methods cannot be A-stable. However, the size and shape of the their stability regions can matter. By careful selection of the parameters of the m-stage method that appear in the coefficients of the stability polynomial, one can influence the shape and size of stability region and can aim to optimize it in some sense. Hong et al. in their seminal paper in 1997 [8] showed how real quantifier elimination (RQE) can be used for the investigation of stability problems of dynamical systems. They also showed some examples which were too difficult for their RQE program called QEPCAD. Following their setting and Seip et al. work [15], we investigate the maximal largest possible disk and half-disk that can be inscribed in the stability region of an ERK method and for a whole class of stability regions associated to the class of m-stage pth order methods by RQE. The main tool for the investigation is Mathematica’s RQE implementation. We obtain exact optimal radii for the family of m-stage pth-order methods, when p = m - 1 or p = m-2 (m ≤ 5). We also show that the maximal radius for the particular Dormand-Prince 7-stage 5th-order method can be computed in a few seconds.

We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely restricted to handling linear arithmetic operations and properties, or are non-compositional. We use Constrained Horn Clauses (CHCs) to represent the verification conditions where the memory operations are modeled using the extensional theory of arrays (ARR). First, we describe an exponential time quantifier elimination (QE) algorithm for ARR which can introduce new quantifiers of the index and value sorts. Second, we adapt the QE algorithm to efficiently obtain under-approximations using models, resulting in a polynomial time Model Based Projection (MBP) algorithm. Third, we integrate the MBP algorithm into the framework of compositional reasoning of procedural programs using may and must summaries recently proposed by us. Our solutions to the CHCs are currently restricted to quantifier-free formulas. Finally, we describe our practical experience over SV-COMP'15 benchmarks using an implementation in the tool SPACER., Comment: 8 pages, FMCAD 2015

We investigate the quantifier alternation hierarchy of first-order logic over finite words. To do so, we rely on the separation problem. For each level in the hierarchy, this problem takes two regular languages as input and asks whether there exists a formula of the level that accepts all words in the first language and no word in the second one. Usually, obtaining an algorithm that solves this problem requires a deep understanding of the level under investigation. We present such an algorithm for the level a#x03A3; 3 (formulas having at most 2 alternations beginning with an existential block). We also obtain as a corollary that one can decide whether a regular language is definable by a a#x03A3; 4 formula (formulas having at most 3 alternations beginning with an existential block).

This paper presents a method to establish overshoot suppression control based on estimation on the final tracking error and its feedback compensation. Overshoot is one of important issues in industrial control to avoid unsafe situations such as overflow, crash, and so on. We analyze the overshoot amount caused by control input and show a strategy for its suppression. To apply the strategy, we show a control scheme composed of prediction and feedback compensation with novel feedback gain design method based on quantifier elimination. Illustrative examples are given to show the effectiveness of the proposing method.

We report on our on-going efforts to apply real quantifier elimination to the (semi-)automatic complexity analysis of numerical algorithms. In particular, we describe a case study on the square root problem: given a real number x and an error bound, find a real interval such that it contains √x and its width is less than or equal to e. A typical numerical algorithm starts with an initial interval and repeatedly updates it by applying a “refinement map” on it until it becomes narrow enough. In this paper, the complexity analysis amounts to find the smallest maximum number of loop iterations of the algorithm. Hence, the algorithm must be correct, terminating and optimal. It can be formulated as a quantifier elimination problem over real numbers. Hence, in principle, the complexity analysis can be carried out automatically. However, the computational requirement is huge, making the automatic analysis practically impossible with the current general real quantifier elimination software. We overcame the difficulty by (1) carefully reducing a complicated quantified formula into several simpler ones and (2) automatically eliminating the quantifiers from the resulting ones using the state-of-the-art quantifier elimination software. As the result, we were able to compute semi-automatically the complexity of a class of optimal contracting maps.

This paper presents a simple solution to an offline multi-rate predictive control problem with constraints by using quantifier elimination approach. One of advantages of the proposing method is the easiness of implementation as PID control. Time domain input to output modeling is applied in order to avoid huge memory cost which is pointed out in state space based offline MPC methods. We give admissible tracking error at future time points as a control specification. We can test the existence of a control law which satisfies the control specification by a visualized logical formula.

We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied. Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC.We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.

We consider the problem of existential quantifier elimination for Boolean formulas in conjunctive normal form. Recently we presented a new method for solving this problem based on the machinery of Dependency sequents (D-sequents). The essence of this method is to add to the quantified formula implied clauses until all the clauses with quantified variables become redundant. A D-sequent is a record of the fact that a set of quantified variables is redundant in some subspace. In this paper, we introduce a quantifier elimination algorithm based on a new type of D-sequents called clause D-sequents that express redundancy of clauses rather than variables. Clause D-sequents significantly extend our ability to introduce and algorithmically exploit redundancy, as our experimental results show.

We present a method for synthesising action models that result in a given post-condition when executed on any Kripke model. Action models represent social actions that affect the knowledge or beliefs of agents in multi-agent systems. In the consideration of action model synthesis, we introduce an extension of the action model logic of Baltag, Moss and Solecki [3] with an action model quantifier, ∃φ which stands for “there is an action model that results in the post-condition φ”. We show that this quantifier is equivalent to the refinement quantifier of van Ditmarsch and French [10], and provide a sound and complete axiomatisation for the resulting logic, along with decidability and expressivity results.

General problems of the interval circuit analysis theory are considered. Quantifier interpretation of the interval circuit parameters in the analysis and diagnosis problems is analysed. The rules of the applied interval problems are formalised. As applied to various problem definition of the circuit analysis and diagnosis two kind of the interval variable are introduced, which are associated with universal quantifier and existential quantifier. The quantifier description of the problem solution set is considered. Formal solution set, united solution set, tolerable solution set, controllable solution set are considered. The example is given.

We define always eventually region stability and then formulate the absolute always eventually region stability problem as the problem of finding a class of plants that a generic proportional-integral (PI) controller can always eventually stabilize. We use real quantifier elimination methods to solve the absolute always eventually region stability problem. The class of plants found in our solution includes nonlinear and switched plant models. Our analysis reveals that if a PI controller satisfies two assumptions of the form: (a) the proportional gain K p and the integral gain K i satisfy an inequality, and (b) the integral of the error term in the controller is saturated, then such a PI controller can be used to establish always eventually region stability for any plant that suitably responds to the control input. Such a result is useful for compositionally verifying a system consisting of a plant and a controller.

A hybrid computational method between sum of squares (SOS) and quantifier elimination (QE) is discussed for a problem of nonlinear gain analysis. A computational procedure is proposed to be applied to nonlinear polynomial systems. The procedure takes two major parts: the first part is searching a structure in the gain functions while the second part reveals all the gain functions in the structure. These tasks are assigned to the SOS and QE approaches, respectively. In order to find an accurate system performance, the gain functions are optimized in the procedure. The proposed analysis procedure is illustrated for a few systems.

Interval Logics are often very expressive logics for which decision and model-checking algorithms are hard or even impossible to achieve, and this also applies for Duration Calculus, which adds the notion of accumulated duration to the Interval Temporal Logic introduced by Moszkowski et al. In this ongoing work, we report on our experiences with implementing the model-checking algorithm introduce by Franzle and Hansen, which reduces model checking to checking formulas of Presburger arithmetic. The model-checking algorithm generates Presburger formulas that may have sizes being exponential in the chop depth of the Duration Calculus formulas, so it is not clear whether this is a feasible approach. The decision procedure is partitioned into a front end with reductions including "cheap", equation-based quantifier eliminations, and a general quantifier-elimination procedure, where we have experimented with an implementation based on Cooper's algorithm and with the SMT solver Z3. The formula reductions are facilitated using a new 'guarded normal form'. Applying the front end before a general quantifier elimination procedure gave significant improvements for most of the experiments.

This paper is concerned with symbolic computation in analysis and synthesis for multi-agent dynamical systems, where all the agents share a common linear time-invariant (LTI) system h(s). Such a system can be represented by the LTI system with generalized frequency variable φ(s) :=1/h(s). There are a very few results on the analysis and synthesis except stability test, since the system is large and more complex than the standard LTI system. Actually, most of the problems are nonconvex in general, and hence numerical computations do not work so well. Instead, appropriate use of symbolic computations may help to solve the problems. This paper treat two types of analysis problems on robustness of the system, namely H ∞ -norm computation and D-stability test, and show that symbolic computation including quantifier elimination (QE) method effectively works for solving the problems.

It is an important task to obtain a nonlinear gain function of dynamical systems by computational methods. A numerical approach, sum of squares (SOS), has been proposed so far, but there is no clue to find a minimum one. In this paper, a procedure is proposed to analyze nonlinear gain functions of a class of dynamical systems by combination use of symbolic and numeric methods. The role of SOS is to search for a structure of a gain function quickly and then quantifier elimination (QE) covers all possible functions in the structure to find a minimum function. An illustrative example shows the effectiveness of the proposed analysis procedure.

One of the major interests of finite model theory is to separate the expressive power of different logics or fragments of logics. In this paper, we define a variant of Ehrenfeucht-Fra\"iss\' e games that characterizes quantifier classes over finite structures and prove that the fragments of first-order logic based on quantifier structures form a strict hierarchy in terms of their expressiveness over finite structures.

This paper presents a new approach to generate inequalities invariants of hybrid system based on template and quantifier elimination. The main idea is to introduce a candidate parametric invariant as template and then reduce the verification condition into a quantifier elimination problem. The challenge is to deal with the continuous consecution condition of hybrid system because of the existence of differential equation. From the preliminary experiment results, we demonstrate the feasibility of our approach.

In the logical query of relational database, the Derivation of Relations predicate Methods is the theoretical foundation, but SQL is The standard computer query language, which concrete the logical query of software. Special emphasis, for Complex universal quantifier, it's just in the theory of Theoretic. The Research on the Derivation of Relations predicate Methods for Complex universal quantifier, in practical case, which will be realized by SQL.

Craig and deductive interpolation properties are investigated for uninorm based fuzzy logics. In particular, it is shown that for a restricted language, the only extensions of monoidal t-norm logic with Craig interpolation are classical logic, Godel logic, and three-valued Godel logic. Quantifier elimination in an appropriate language and the amalgamation, deductive interpolation and Craig interpolation properties are established for the logics based on idempotent residuated uninorms with an involutive negation.

As one of mathematical representations of discrete distributed systems, Petri net has been widely used to model, analyze and simulate concurrent and distributed systems. The algebraic invariant is a powerful technique for the verification of Petri net. In this paper, we present a new and simple technique to construct the invariant of Petri net based on its properties. This technique can generate the invariant without computing DNF formula or Gro¨bner bases or using quantifier elimination, thereby circumventing difficulties in recent approaches. From the preliminary experiment results, the performance of this technique is significant.

Recently, the trend of control engineering changes from classical control theory to modern control theory, and also analogue to digital with times. But, even now parameter adjustment in generator excitation control has been often carried out by the classical loop-shaping method using a Bode diagram. Modern control theory has seldom been used in practice due to the facts that the experience of using such design methods is insufficient and there are no introduction results in actual design situations. However, the classical loop-shaping method has some drawbacks, e.g., sensitivity adjustment procedure by a Bode diagram is complicated and cumbersome. In this paper we employ a loop-shaping method using Hinfin norm constraints, which is achieved via a parameter space approach accomplished by symbolic method called quantifier elimination (QE) and apply it to design PI control type AVR of the excitation control. The method allows us to determine appropriate parameter values of PI controller for visually in a parameter space. We report some simulation results for the PI control type AVR design and inspect the performance.

Affine size-change analysis has been used for calculating precise polynomial bounds on the run times, and stack depths of affine size-change terminating programs. Such polynomial costs may be discovered by a characterization as a problem in quantifier elimination. In this paper we extend this work to cover a class of exponential cost programs. The tool described allows the calculation of run-time and stack-depth costs for some classes of exponential-cost programs, again by using quantifier elimination. The technique is automated, and uses the reduce computer algebra system.

In this paper we consider the problem of computing sets of observable states for discrete-time, piecewise affine systems. When the maximal set of observable states is full-dimensional, we provide an algorithm for reconstructing it up to a zero measure set. The core of the method is a quantifier elimination procedure that, in view of basic results on piecewise linear algebra, can be performed via the projection of polytopes on subspaces. We also provide a necessary condition on the minimal length of the observability horizon in order to expect a full-dimensional set of observable states. Numerical experiments highlight that the new procedure is considerably faster than the one proposed in (Ferrari-Trecate and Gati, 2004).

Recently there has been an increasing interest in the application of computer algebra to control system analysis and design. Control system design is to find out feasible parameters to be designed for which a target system satisfies given control design specifications. Many important control system design problems are regarded as parametric and non-convex optimization problems. We have been developing a MATLAB toolbox for robust control via a parameter space approach based on symbolic-numeric computation. First we explain how we can practically solve such control system design problems by using algebraic methods, quantifier elimination. Then we show an effective visualization of the results i.e. the feasible regions of design parameters in a parameter space. All these results are implemented as the MATLAB toolbox for parametric robust control. We also demonstrate our MATLAB toolbox by using actual control design problems.

Air traffic management system is responsible for a safe and orderly flow of air traffic, thus preventing collisions between aircraft both in the air and on the ground. This paper shows that an air traffic management problem can be transferred into a weighted time-optimal problem for hybrid system. In particular, it is shown that the problem can be transformed into a constrained optimization problem whose constraints are a set of inequalities with quantifiers. Quantifier elimination (QE) techniques are employed in order to derive quantifier free inequalities. The optimal cost is obtained using linear programming

We describe an efficient approach for SAT-based quantifier elimination that significantly improves the performance of pre-image and fixed-point computation in SAT-based unbounded symbolic model checking (UMC). The proposed method captures a larger set of new states per SAT-based enumeration step during quantifier elimination, in comparison to previous approaches. The novelty of our approach is in the use of circuit-based cofactoring to capture a large set of states, and in the use of a functional hashing based simplified circuit graph to represent the captured states. We also propose a number of heuristics to further enlarge the state set represented per enumeration, thereby reducing the number of enumeration steps. We have implemented our techniques in a SAT-based UMC framework where we show the effectiveness of SAT-based existential quantification on public benchmarks, and on a number of large industry designs that were hard to model check using purely BDD-based techniques. We show several orders of improvement in time and space using our approach over previous CNF-based approaches. We also present controlled experiments to demonstrate the role of several heuristics proposed in the paper. Importantly, we were able to prove using our method the correctness of a safety property in an industry design that could not be proved using other known approaches.

In this paper, we study classes of discrete time hybrid systems for which the classical algorithm for computing the maximal controlled invariant set and the least restrictive controller is computable and guaranteed to terminate in a finite number of iterations. We show how the algorithm can be encoded using quantifier elimination, which leads to a semi-decidability result for definable hybrid systems. For discrete time linear systems with linear constraints that are either controllable or nilpotent and have bounded disturbances, we show that the controlled invariance algorithm terminates in a number of iterations which is at most the dimension of the state space. Both in the hybrid and in the linear case, our results are much more general than the corresponding ones for continuous time systems. Finally we show that for linear systems with ellipsoidal constraints, an approximated solution can be obtained using robust convex programming. We provide an example showing that our algorithm gives better estimations than other ellipsoidal methods and is more efficient than the exact method for linear constraints.

We study 0-1 laws for extensions of first-order logic by Lindstrom quantifiers. We state sufficient conditions on a quantifier Q expressing a graph property, for the logic FO[Q]-the extension of first-order logic by means of the quantifier Q-to have a 0-1 law. We use these conditions to show, in particular, that FO[Rig], where Rig is the quantifier expressing rigidity, has a 0-1 law. We also show that FO[Ham], where Ham is the quantifier expressing Hamiltonicity, does not have a 0-1 law. Blass and Harary pose the question whether there is a logic which is powerful enough to express Hamiltonicity or rigidity and which has a 0-1 law. It is a consequence of our results that there is no such regular logic (in the sense of abstract model theory) in the case of Hamiltonicity, but there is one in the case of rigidity. We also consider sequences of vectorized quantifiers, and show that the extensions of first-order logic obtained by adding such sequences generated by quantifiers that are closed under substructures have 0-1 laws.

For multi-objective design and robust control synthesis problems, the methods based on quantifier elimination (QE) have been proposed. QE based methods are really suitable for such problems but, in general, they have a drawback on computational complexity. We propose an efficient symbolic method for a parameter space approach based on sign definite condition by a special quantifier elimination using a Sturm-Habicht sequence. Then we examine its feasibility, in particular, for multi-objective control using a low degree fixed-structure controller by showing the several experimental results.

In this paper, we focus on the discrete-time polynomial systems and present the modified algorithms for testing observability and accessibility based on the methods by D. Nesic. Our method uses not only quantifier elimination but also Grobner basis and real root counting techniques for decision problems needed in checking the properties and incorporates the strategy to improve efficiency in testing equivalence of ideals. Moreover, we show that invertibility of the systems can be checked by using Grobner basis technique and hence backward accessibility and transitivity can be tested in the similar way in finite time step.

A systematic scheme that leads to a set of inequalities involving the free variables, whose satisfaction will be necessary and sufficient for global positivity or nonnegativity of any specified polynomial with literal coefficients, is developed.

This paper deals with the application of computerized quantifier elimination (QE) methods for robust multiobjective feedback design, when design objectives are specified in the frequency domain. The class of design problems considered here has no analytical solutions, so that computerized solutions are of interest, even for relatively simple problems. However, due to the computational complexity of pure QE algorithms, a combined QE discretization approach is proposed and illustrated with an example.

This paper presents an experimental/theoretical study of methods to identify and control a repetitively-pulsed high power microwave source. A neural network was used to model the system and quantifier elimination (QE) theory is used to search for suitable operating conditions.

The role of quantifier elimination procedures in the tackling of multidimensional digital filter stability test based on the generalization of Sturm's theorem appeared for the first time as a journal publication in 1974. That was followed in 1975 by a discursive documentation on the use of such methods to tackle output feedback stabilization and other control problems. Recent progress in software for symbol manipulations via serial as well as parallel processing encourage investigations into wider adoption of quantifier elimination theory based methods in problems involving higher number of free variables. This paper review the past and present status before giving future directions for research that incorporate the conflicting factors of accuracy of solution and computational cost for implementing for algorithms developed using particularly cylindrical algebraic decomposition.