Efficient SAT-based techniques for parameter synthesis and optimization

Alberto Griggio

Many application domains can be described in terms of parameterized systems, where parameters are variables whose value is invariant over time, but is only partially constrained. A key challenge in this context is the estimation of the parameter valuations that guarantee the correct behavior of the system. Manual estimation of these values is time consuming and does not find optimal solutions for specific design problems. Therefore, a fundamental problem is to automatically synthesize the maximal region of parameter valuations for which the system satisfies some properties, or to find the best/most appropriate valuation with respect to a given cost function.

In this talk, we present a technique for parameter synthesis and optimization that exploits the efficiency of state-of-the art model checking algorithms based on SAT (and SMT) solvers. We will start from a general solution for parameter synthesis, applicable in various settings, and then show how to improve the effectiveness of our procedure by exploiting domain knowledge. In particular, we show how to use some assumptions of monotonicity, arising naturally in many important applications, in order to speed up the convergence towards the desired solutions. We demonstrate the usefulness of our technique with a set of case studies taken from the domains of diagnosability and safety analysis.