Synthesis for Regular Specifications over Unbounded Domains

paper ps   
Synthesis from declarative specifications is an ambitious automated method for obtaining systems that are correct by construction. Previous work includes synthesis of reactive finite-state systems from linear temporal logic and its fragments. Further recent work focuses on a different application area by doing functional synthesis over unbounded domains, using a modified Presburger arithmetic quantifier elimination algorithm. We present new algorithms for functional synthesis over unbounded domains based on automata-theoretic methods, with advantages in the expressive power and in the efficiency of synthesized code. Our approach synthesizes functions that meet given regular specifications defined over unbounded sequences of input and output bits. Thanks to the translation from weak monadic second-order logic to automata, this approach supports full Presburger arithmetic as well as bitwise operations on arbitrary length integers. The presence of quantifiers enables finding solutions that optimize a given criterion. Unlike synthesis of reactive systems, our notion of realizability allows functions that require examining the entire input to compute the output. Regardless of the complexity of the specification, our algorithm synthesizes linear-time functions that read the input and directly produce the output. We also describe a technique to synthesize functions with bounded lookahead when possible, which is appropriate for streaming implementations. We implemented our synthesis algorithm and show that it synthesizes efficient functions on a number of examples.

Citation

Jad Hamza, Barbara Jobstmann, and Viktor Kuncak. Synthesis for regular specifications over unbounded domains. In FMCAD, 2010.

BibTex Entry

@inproceedings{HamzaETAL10SynthesisforRegularSpecificationsoverUnboundedDomains,
  author = {Jad Hamza and Barbara Jobstmann and Viktor Kuncak},
  title = {Synthesis for Regular Specifications over Unbounded Domains},
  booktitle = {FMCAD},
  abstract = {Synthesis from declarative specifications is an
ambitious automated method for obtaining systems that are correct by construction.
Previous work includes synthesis of reactive finite-state
systems from linear temporal logic and its fragments.
Further recent work focuses on a different application area
by doing functional synthesis over unbounded domains, using
a modified Presburger arithmetic quantifier elimination
algorithm.  We present new algorithms for functional
synthesis over unbounded domains based on automata-theoretic
methods, with advantages in the expressive power and in the
efficiency of synthesized code.
Our approach synthesizes functions that meet given regular
specifications defined over unbounded sequences of input and
output bits.  Thanks to the translation from weak monadic
second-order logic to automata, this approach supports full
Presburger arithmetic as well as bitwise operations on
arbitrary length integers. The presence of quantifiers
enables finding solutions that optimize a given criterion.
Unlike synthesis of reactive systems, our notion of
realizability allows functions that require examining the
entire input to compute the output.  Regardless of the
complexity of the specification, our algorithm synthesizes
linear-time functions that read the input and directly
produce the output. We also describe a technique to
synthesize functions with bounded lookahead when possible,
which is appropriate for streaming implementations.  We
implemented our synthesis algorithm and show that it
synthesizes efficient functions on a number of examples.
},
  year = 2010
}