Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Madhusudan, Parthasarathy http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-32479
URL:

Synthesizing Reactive Programs

pdf-format:


Abstract

Current theoretical solutions to the classical Church's synthesis problem are focused on synthesizing transition systems and not programs. Programs are compact and often the true aim in many synthesis problems, while the transition systems that correspond to them are often large and not very useful as synthesized artefacts. Consequently, current practical techniques first synthesize a transition system, and then extract a more compact representation from it. We reformulate the synthesis of reactive systems directly in terms of program synthesis, and develop a theory to show that the problem of synthesizing programs over a fixed set of Boolean variables in a simple imperative programming language is decidable for regular omega-specifications. We also present results for synthesizing programs with recursion against both regular specifications as well as visibly-pushdown language specifications. Finally, we show applications to program repair, and conclude with open problems in synthesizing distributed programs.

BibTeX - Entry

@InProceedings{madhusudan:LIPIcs:2011:3247,
  author =	{Parthasarathy Madhusudan},
  title =	{{Synthesizing Reactive Programs}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{428--442},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3247},
  URN =		{urn:nbn:de:0030-drops-32479},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.CSL.2011.428},
  annote =	{Keywords: program synthesis, boolean programs, automata theory, temporal logics}
}

Keywords: program synthesis, boolean programs, automata theory, temporal logics
Seminar: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue date: 2011
Date of publication: 2011


DROPS-Home | Fulltext Search | Imprint Published by LZI