Encoding strategies for bounded synthesis

reactive systems. The main point of interest is to nd an implementation that fullls
a specication, given in such a logic. While one possibility is to just manually build
the implementation and check its correctness, the more interesting question is whether
we can also do this automatically. Unfortunately, the synthesis of reactive systems is
intractably hard. One approach to improve the complexity is that of constraint-based
bounded synthesis, where the synthesis problem is reduced to solving a constraint system.
The approach also introduces an upper bound on the size of the resulting implementation,
what comes along with an easy possibility for minimization. The eciency of the approach
varies dramatically with the encoding strategy. We will present dierent such encoding
strategies from the bounded synthesis problem of linear temporal logic to the boolean
satisability problem and analyze their assets and drawbacks.
1