Quantified Constraint Solving in Control Engineering

The main objective of the proposed project is to develop theories, algorithms and software for solving quantified constraints that arise in control engineering. Here a quantified constraint is a first-order formula over the reals. This means that it contains quantifiers ("for all", "there is"), connectives ("and", "or", "not"), predicate symbols (e.g., =, <), function symbols (e.g., +, -, *, sin), rational constants and variables ranging over the real numbers. Within this project we require that a given quantified constraint models a significant application in control engineering. This has several consequences: In practice, constants are often not exactly known, so it is important to deal with approximate input constants, for example in the form of floating-point intervals. Moreover, one should be able to compute approximate solutions, especially in the case when exact solutions are too hard to compute. Furthermore, specific applications result in a specific structure of the occurring quantified constraints. This structure can and should be exploited for efficiency reasons.