Synthesis of Discrete-Continuous Systems using SMT Solving

Speaker

Ulrich Loup

Title Synthesis of Discrete-Continuous Systems using SMT Solving
When 27.05.2009
Where Lecture Room Informatik 11
Abstract In this talk we address the satisfiability-checking problem for the first-order theory of the reals. We are motivated by the synthesis of hybrid systems with mixed discrete-continuous behavior. The synthesis method we want to apply needs an algorithm to check whether first-order formulas are satisfiable over the reals. The first-order theory of the reals is decidable and corresponding tools are available. On the one hand, these tools are efficient for solving conjunctions of real constraints, but do not scale well for arbitrary Boolean combinations of real constraints, as it occurs in our application domain. On the other hand, there are highly efficient SAT solvers applicable for satisfiability checking of arbitrary propositional formulas. Thus, we can use a combination of both in order to accomplish efficient satisfiability checking of arbitrary Boolean combinations of real constraints: an SMT (SAT modulo theories) solver. We introduce the basic ideas of SAT-solving, and discuss what conditions a theory solver must satisfy to be integrable into an SMT solver. We give an overview of the most efficient decision methods for the first-order theory of the reals and discuss to what extent they fulfill these conditions.