Tags:formal methods, program synthesis and reactive synthesis

Abstract:

Model Refinement is a novel approach to reactive program synthesis that iteratively refines an over-approximating model of a desired system behavior by eliminating undesired behaviors. In contrast to many current automata based approaches to reactive synthesis, it does not require a finite state space or user supplied templates. Instead it symbolically computes the required invariant by solving a system of definite constraints.. The original work on model refinement, however, assumed that both the assumptions on the environment (in an Assume-Guarantee setting) and the constraints on the system variables necessary to guarantee the required behavior were fixed and known. Sometimes, though, the designer of a system has some intended behavior and wishes to know what the minimal assumptions are on the environment under which the system can guarantee the required behavior; or to know what the constraints are on the system variables under known environment assumptions. In other words, we wish to solve a parametric model refinement problem. Our contribution in this paper is to show how such a problem can be solved when the constraints are assumed to be an interval of the form m\ldots n.

Inferring Environment Assumptions in Model Refinement