Applications of Quantified Constraint Solving over the Reals
Bibliography

Stefan Ratschan

January 30, 2008

Quantified constraints over the reals appear in numerous contexts. Usually existential quantification occurs when some parameter can be chosen by the user of a system, and univeral quantification when the exact value of a parameter is either unknown, or when it occurs in infinitely many, similar versions.

The following is a list of application areas and publications that contain applications for solving quantified constraints over the reals. The list is certainly not complete, but grows as the author encounters new items. Contributions are very welcome!

Electrical Engineering/Electronics:
[95][91]
Stability:
[74][93][75][94][55][54][76]
Control:
[1][64][63][38][62][80][8][5][48][4][26][89][92][90][88][81][37][97][36][82][102][6][87][56], survey [35], reachability [71][72][70][7], embedded control systems [99], hybrid systems [42][44][47][98][91][41], projection of system output function [51], computation of control invariant sets [21], optimal control [83]
Computational Geometry/Motion Planning/Collision Detection:
[96][62][52][101][10]
Constraint Databases:
[69][22][84][13][2][14][43][68]
Theorem Proving in Real Geometry:
[33][32]
Several Different:
[34][100][77][62]
Use of Predicate Language for Modeling Engineering Problems:
[39][17]
Other:
camera motion: [15], constraint logic programming: [53], mechanical engineering: [58][57], mathematics: [73] (from [65]), [23][66], biology: [27][47][85][24], interpolation: [49], scheduling [45], automated theorem proving [16][60][59], optimization: [3], termination of rewrite systems [28][31], flight control [46], program analysis [29][30][50][9], hybrid systems [86], injectivity test [19] (see Lagrange/Delanoue/Jaulin papers), computer assisted proofs [11], parameter estimation [18][20][67]

Acknowledgments

Thanks to Hirokazu Anai for contributing references.

References

 [1]
C. Abdallah, P. Dorato, W. Yang, R. Liska, and S. Steinberg. Applications of quantifier elimination theory to control system design. In 4th IEEE Mediterranean Symposium on Control and Automation, Crete, Greece, 1996.
 [2]
F. Afrati, S. S. Cosmadakis, S. Grumbach, and G. M. Kuper. Linear vs. polynomial constraints in database query languages. In Proc. PPCP'94, 1994.
 [3]
H. Anai. On solving semidefinite programming by quantifier elimination. In Proc. of American Control Conference, Philadelphia, pages 2814-2818, 1998.
 [4]
H. Anai. Algebraic approach to analysis of discrete-time polynomial systems. In Proc. of European Control Conference, 1999.
 [5]
H. Anai and S. Hara. Fixed-structure robust controller synthesis based on sign definite condition by a special quantifier elimination. In Proceedings of American Control Conference 2000, pages 1312-1316, 2000.
 [6]
H. Anai, S. Hara, and K. Yokoyama. Sum of roots with positive real parts. In ISSAC '05: Proceedings of the 2005 international symposium on Symbolic and algebraic computation, pages 21-28, New York, NY, USA, 2005. ACM Press.
 [7]
H. Anai and V. Weispfenning. Reach set computation using real quantifier elimination. In M. D. Benedetto and A. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control : 4th International Workshop, HSCC 2001, volume 2034 of LNCS. Springer, 2001.
 [8]
B. D. O. Anderson, N. K. Bose, and E. I. Jury. Output feedback stabilization and related problems -- solution via decision methods. IEEE Trans. Automatic Control, AC-20:53-66, 1975.
 [9]
M. G. Armin Groeslinger and C. Lengauer. Quantifier elimination in automatic loop parallelization. Journal of Symbolic Computation, 41(11):1206-1221, 2006.
 [10]
D. S. Arnon. Geometric reasoning with logic and algebra. Artificial Intelligence, 37:37-60, 1988.
 [11]
B. Bánhelyi, T. Csendes, and B. M. Garay. Optimization and the Miranda approach in detecting horseshoe-type chaos by computer. Int. J. Bifurcation and Chaos, 17(3):735-748, 2007.
 [12]
B. Barmish and Z. Shi. Robust stability of a class of polynomials with coefficients depending multilinearly on perturbations. IEEE Trans. Autom. Control, AC-35:1040-1043, 1990.
 [13]
S. Basu. New results on quantifier elimination over real closed fields and applications to constraint databases. Journal of the ACM, 46(4):537-555, 1999.
 [14]
M. Baudinet, J. Chomicki, and P. Wolper. Constraint- generating dependencies. In G. Gottlob and M. Vardi, editors, Database Theory -ICDT'95, 5th International Conference, volume 893 of LNCS, Prague, Czech Republic, 1995. Springer- Verlag.
 [15]
F. Benhamou and F. Goualard. Universally quantified interval constraints. In Proc. of the Sixth Intl. Conf. on Principles and Practice of Constraint Programming (CP'2000), number 1894 in LNCS, Singapore, 2000. Springer Verlag.
 [16]
N. S. Bjørner, M. E. Stickel, and T. E. Uribe. A practical integration of first-order reasoning and decision procedures. In CADE-97, volume 1249, pages 101-115, 1997.
 [17]
J. Bowen and D. Bahler. Full first- order logic in knowledge representation: A constraint- based approach. Technical Report TR-93-03, Department of Computer Science, University College, Cork, Ireland, 1993.
 [18]
I. Braems, F. Berthier, L. Jaulin, M. Kieffer, and É. Walter. Guaranteed estimation of electrochemical parameters by set inversion using interval analysis. Journal of Electroanalytical Chemistry, 495:1-9, 2000.
 [19]
I. Braems, L. Jaulin, M. Kieffer, and E. Walter. Guaranteed numerical alternatives to structural identifiability testing. In Proceedings of the 40th IEEE Conference on Decision and Control, pages 3122-3127, 2001.
 [20]
I. Braems, N. Ramdani, A. Boudenne, L. Jaulin, L. Ibos, E. Walter, and Y. Candau. New set-membership techniques for parameter estimation in presence of model uncertainty. In Proc. of the 5th Internation Conference on Inverse Problems in Engineering: Theory and Practice, 2005.
 [21]
J. M. Bravo, D. Limon, T. Alamo, and E. Camacho. On the computation of invariant sets for constraint nonlinear systems-an interval arithmetic approach. Automatica, 41:1583-1589, 2005.
 [22]
A. Brodsky. Constraint databases: Promising technology or just intellectual exercise? ACM Computing Surveys, 28(4), 1996.
 [23]
C. Brown. Simple CAD construction and its applications. Journal of Symbolic Computation, 31(5):521-547, 2001.
 [24]
C. W. Brown, M. E. Kahoui, D. Novotni, and A. Weber. Algorithmic methods for investigating equilibria in epidemic modeling. Journal of Symbolic Computation, 41:1157-1173, 2006.
 [25]
B. F. Caviness and J. R. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Wien, 1998.
 [26]
C. Champetier and J. F. Magni. Pole assignment by output feedback using cylindrical algebraic decomposition. Internation Journal of Control, 48(5):2107-2120, 1988.
 [27]
C. Chauvin, M. Müller, and A. Weber. An application of quantifier elimination to mathematical biology. In Computer Algebra in Science and Engineering, pages 287-296. World Scientific, 1994.
 [28]
G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation, 12:299-328, 1991. Also in [25].
 [29]
M. Colon, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In Computer-Aided Verification (CAV 2003), volume 2725 of LNCS, pages 420-432. Springer, 2003.
 [30]
P. Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In R. Cousot, editor, VMCAI'05, number 3385 in LNCS, pages 1-24. Springer, 2005.
 [31]
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69-116, 1987.
 [32]
A. Dolzmann. Solving geometric problems with real quantifier elimination. In X.-S. Gao, D. Wang, and L. Yang, editors, Automated Deduction in Geometry, pages 14-29. Springer, 1999.
 [33]
A. Dolzmann, T. Sturm, and V. Weispfenning. A new approach for automatic theorem proving in real geometry. Journal of Automated Reasoning, 21(3):357-380, 1998.
 [34]
A. Dolzmann, T. Sturm, and V. Weispfenning. Real quantifier elimination in practice. In B. H. Matzat, G.-M. Greuel, and G. Hiss, editors, Algorithmic Algebra and Number Theory, pages 221-248. Springer, 1998.
 [35]
P. Dorato. Quantified multivariate polynomial inequalities. IEEE Control Systems Magazine, 20(5):48-58, October 2000.
 [36]
P. Dorato, D. Famularo, C. T. Abdallah, and W. Wang. Robust nonlinear feedback design via quantifier elimination theory. International Journal of Robust and Nonlinear Control, 9:817-822, 1999.
 [37]
P. Dorato and I. Sakamaki. Symbolic quantifier elimination for robust feedback design. In Proceedings of the 4th IFAC Symposium on Robust Control Design, 2003.
 [38]
P. Dorato, W. Yang, and C. Abdallah. Robust multi-objective feedback design by quantifier elimination. Journal of Symbolic Computation, 24:153-159, 1997.
 [39]
B. Faltings and K. Sun. FAMING: Supporting innovative mechanism shape design. Computer-Aided Design, 28(3):207-216, 1996.
 [40]
G. Fiorio, S. Malan, M. Milanese, and M. Taragna. Robust performance design of fixed structure controllers with uncertain parameters. In Proceedings of the 32nd IEEE Conf. Decision and Control, pages 3029-3031, 1993.
 [41]
I. A. Fotiou, A. G. Beccuti, G. Papafotiou, and M. Morari. Optimal control of piece-wise polynomial hybrid systems using cylindrical algebraic decomposition. In J. Hespanha and A. Tiwari, editors, HSCC'06, volume 3927 of LNCS. Springer, 2006.
 [42]
M. Fränzle. Analysis of hybrid systems: An ounce of realism can save an infinity of states. In J. Flum and M. Rodriguez-Artalejo, editors, Computer Science Logic (CSL'99), number 1683 in LNCS. Springer, 1999.
 [43]
V. Gaede and O. Günther. Constraint-based query optimization and processing. In Proc. 1st Intl. Database Workshop on Constraint Database Systems (CDB'95), 1995.
 [44]
Y. Gao, J. Lygeros, M. Quincampoix, and N. Seube. Approximate stabilisation of uncertain hybrid systems. In Maler and Pnueli [79], pages 203-215.
 [45]
R. Gerber, W. Pugh, and M. Saksena. Parametric dispatching of hard real-time tasks. IEEE Transactions on Computers, 44(3):471-479, 1995.
 [46]
A. Geser and C. Muñoz. A geometric approach to strategic conflict detection and resolution. In Proceedings of the 21st Digital Avionics Systems Conference (DASC 2002), 2002.
 [47]
R. Ghosh, A. Tiwari, and C. Tomlin. Automated symbolic reachability analysis; with application to delta-notch signaling automata. In Maler and Pnueli [79].
 [48]
S. T. Glad. An algebraic approach to bang-bang control. In Proc. 3rd European Contr. Conf., pages 2892-2895, Rome, Italy, 1995.
 [49]
L. Gonzalez-Vega. Applying quantifier elimination to the Birkhoff interpolation problem. Journal of Symbolic Computation, 22(1):83-103, 1996.
 [50]
A. Größlinger, M. Griebl, and C. Lengauer. Introducing non-linear parameters to the polyhedron model. In M. Gerndt and E. Kereku, editors, Proc. 11th Workshop on Compilers for Parallel Computers (CPC 2004), Research Report Series, pages 1-12. LRR-TUM, Technische Universität München, July 2004.
 [51]
P. Herrero i Viñas. Quantified Real Constraint Solving Using Modal Intervals. PhD thesis, Universitat de Girona, 2006.
 [52]
H. Hong. Collision problems by an improved CAD- based quantifier elimination algorithm. Technical Report 91-05, RISC- Linz, 1991.
 [53]
H. Hong. Non-linear constraints solving over real numbers in constraint logic programming. Technical Report 92-08, RISC-Linz, 1992.
 [54]
H. Hong, R. Liska, and S. Steinberg. Logic, quantifiers, computer algebra and stability. SIAM News, 30(6):10-,13, 1997.
 [55]
H. Hong, R. Liska, and S. Steinberg. Testing stability by quantifier elimination. Journal of Symbolic Computation, 24(2):161-187, 1997.
 [56]
N. Hyodo, M. Hong, H. Yanami, S. Hara, and H. Anai. Solving and visualizing nonlinear parametric constraints in control based on quantifier elimination. Applicable Algebra in Engineering, Communication and Computing, 18:497-512, 2007.
 [57]
N. I. Ioakimidis. Quantifier elimination in applied mechanics problems with cylindrical algebraic decomposition. International Journal of Solids and Structures, 34(30):4037-4070, 1997.
 [58]
N. I. Ioakimidis. REDLOG-aided derivation of feasibility conditions in applied mechanics and engineering problems under simple inequality constraints. Journal of Mechanical Engineering (Strojnícky Casopis), 50(1):58-69, 1999.
 [59]
P. Janicic and A. Bundy. A general setting for combining and integrating decision procedures into theorem provers. Journal of Automated Reasoning, 2001.
 [60]
P. Janicic, A. Bundy, and I. Green. A framework for the flexible integration of a class of decision procedures in theorem provers. In CADE-16, number 1632 in LNAI, pages 127-141. Springer, 1999.
 [61]
L. Jaulin, I. Braems, and É. Walter. Interval methods for nonlinear identification and robust control. In 41st IEEE Conference on Decision and Control, 2002.
 [62]
L. Jaulin and É. Walter. Guaranteed tuning, with application to robust control and motion planning. Automatica, 32(8):1217-1221, 1996.
 [63]
M. Jirstrand. Nonlinear control system design by quantifier elimination. Journal of Symbolic Computation, 24(2):137-152, 1997.
 [64]
M. Jirstrand. Algebraic Methods for Inequality Constraints in Control. PhD thesis, Linköping University, Department of Electrical Engineering, Division of Automatic Control, 1998. No. 527.
 [65]
W. Kahan. Problem no. 9: An ellipse problem. SIGSAM Bulletin of the ACM, 9(35):11, 1975.
 [66]
M. E. Kahoui and A. Weber. Deciding Hopf bifurcations by quantifier elimination in a software-component architecture. Journal of Symbolic Computation, 30(2):161-179, 2000.
 [67]
M. Kieffer and E. Walter. Interval analysis for guaranteed non-linear parameter and state estimation. Mathematical & Computer Modelling of Dynamical Systems, 11(2):171-181, 2005.
 [68]
M. Koubarakis. Foundations of indefinite constraint databases. In Proc. PPCP'94, 1995.
 [69]
G. Kuper, L. Libkin, and J. Paredaens, editors. Constraint Databases. Springer, 2000.
 [70]
G. Lafferriere, G. J. Pappas, and S. Yovine. Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computation, 32(3):231-253, 2001.
 [71]
G. Lafferriere, G. S. Pappas, and S. Yovine. A new class of decidable hybrid systems. In Hybrid Systems: Computation and Control, volume 1569 of LNCS, pages 137-151. Springer, 1999.
 [72]
G. Lafferriere, G. S. Pappas, and S. Yovine. Reachability computation for linear hybrid systems. In Proceedings of the 14th IFAC World Congress, volume E, pages 7-12, Beijin, China, 1999.
 [73]
D. Lazard. Quantifier elimination: Optimal solutions for two classical examples. Journal of Symbolic Computation, 5(1,2):261-266, 1988.
 [74]
R. Liska and S. Steinberg. Applying quantifier elimination to stability analysis of difference schemes. Computer Journal, 36(5):497-593, 1993.
 [75]
R. Liska and S. Steinberg. Solving stability problems using quantifier elimination. In R. Jeltsch and M. Mansour, editors, Stability Theory, Proceedings of Conference on Centennial Hurwitz on Stability Theory, pages 205-210, Basel, 1996. Birkhäuser Verlag. International Series of Numerical Mathematics (ISNM) Vol. 121.
 [76]
R. Liska and P. Váchal. Quantifier elimination supported proofs in numerical treatment of fluid flows. Applicable Algebra in Engineering, Communication and Computing, 18(6):575-582, 2007.
 [77]
R. Loos and V. Weispfenning. Applying linear quantifier elimination. The Computer Journal, 36(5):450-462, 1993.
 [78]
S. Malan, M. Milanese, and M. Taragna. Robust analysis and design of control systems using interval arithmetic. Automatica, 33(7):1363-1372, 1997.
 [79]
O. Maler and A. Pnueli, editors. Hybrid Systems: Computation and Control (HSCC), volume 2623 of LNCS. Springer, 2003.
 [80]
D. Nesic and I. M. Y. Mareels. Dead beat controllability of polynomial systems: Symbolic computation approaches. IEEE Transactions on Automatic Control, 43(2):162-175, 1998.
 [81]
D. Nesic and I. M. Y. Mareels. Stability of implicit and explicit polynomial systems: Symbolic computation approaches. Europ. J. Contr., 5:32-43, 1999.
 [82]
T. V. Nguyen, T. Mori, Y. Kuroe, and Y. Mori. Qe approach to common lyapunov function problem. Journal of Japan Society for Symbolic and Algebraic Computation, 10:52-62, 2003.
 [83]
Y. Pang and M. P. Spathopoulos. Reachability and optimal control for linear hybrid automata: A quantifier elimination approach. International Journal of Control, 2006. to appear.
 [84]
J. Paredaens, J. van den Bussche, and D. van Gucht. First-order queries on finite structures over the reals. SIAM Journal on Computing, 27(6):1747-1763, 1998.
 [85]
C. Piazza, M. Antoniotti, V. Mysore, A. Policriti, F. Winkler, and B. Mishra. Algorithmic algebraic model checking i: Challenges from systems biology. In 17th International Conference on Computer Aided Verification, 2005.
 [86]
S. Prajna. Barrier certificates for nonlinear model validation. In Proceedings of the IEEE Conference on Decision and Control (CDC), Maui, HI, 2003.
 [87]
S. Prajna and A. Papachristodoulou. A tutorial on sum of squares techniques for systems analysis. In Proc. ACC 2005, 2005.
 [88]
S. Prakash, J. Vanualailai, and T. Soma. Obtaining approximate regions of asymptotic stability by computer algebra: A case study. S. Pac. J. Nat. Sci, 20:56-61, 2002.
 [89]
S. Ratschan and L. Jaulin. Solving composed first-order constraints from discrete-time robust control. In Proceedings of the Sixth Annual Workshop of the ERCIM Working Group on Constraints, 2001. http://arXiv.org/html/cs/0110012
 [90]
S. Ratschan and J. Vehí. Robust pole clustering of parametric uncertain systems using interval methods. In P. Colaneri, editor, Robust Control Design 2003 -- Proceedings of the 4th IFAC Symposium. Elsevier Science, 2004.
 [91]
M. Senesky, G. Eirea, and T. J. Koo. Hybrid modelling and control of power electronics. In Maler and Pnueli [79].
 [92]
Y. Smagina. Robust modal P and PI regulator synthesis for a plant with interval parameters in the state space. In Proc. of the American Control Conference, 2000.
 [93]
S. Steinberg and R. Liska. Stability analysis by quantifier elimination. In G. Jacob, N. Ousous, and S. Steinberg, editors, Proceedings SC 93, International IMACS Symposium on Symbolic Computation, New Trends and Developments, pages 62-67, 1993. Lille, France, June 14 - 17, 1993.
 [94]
S. Steinberg and R. Liska. Stability analysis by quantifier elimination. Mathematics and Computers in Simulation, 42(4-6):629-638, 1996.
 [95]
T. Sturm. Reasoning over networks by symbolic methods. Applicable Algebra in Engineering Communication and Computing, 10(1):79-96, September 1999.
 [96]
T. Sturm and V. Weispfenning. Computational geometry problems in REDLOG. In D. Wang, editor, Automated Deduction in Geometry, volume 1360 of LNAI, pages 58-86, Springer-Verlag, 1998.
 [97]
B. Tibken and E. Hofer. Application of quantifier elimination to controller design for bilinear systems. In M. Hamza, editor, Proc. IASTED International Conference Control and Applications CA 2000, pages 102-107, 2000.
 [98]
A. Tiwari and G. Khanna. Series of abstractions for hybrid automata. In C. J. Tomlin and M. R. Greenstreet, editors, Hybrid Systems: Computation and Control, number 2289 in LNCS, 2002.
 [99]
A. Tiwari, N. Shankar, and J. Rushby. Invisible formal methods for embedded control systems. Proc. of the IEEE, 2002. to appear.
 [100]
V. Weispfenning. Simulation and optimization by quantifier elimination. Journal of Symbolic Computation, 24(2), 1997.
 [101]
V. Weispfenning. Semilinear motion planning with REDLOG. Applicable Algebra in Engineering, Communication, and Computing, 12(6):455-475, 2001.
 [102]
J.-Q. Ying, L. Xu, and M. Kawamata. Robust stability and stabilization of n-d systems. In CD Proceedings of MTNS, 2002.

Examples

A collection of examples from the above papers. I am thankful for any contribution!