Synthesizing reactive programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 ω-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.

Original languageEnglish (US)
Title of host publicationComputer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011
Pages428-442
Number of pages15
DOIs
StatePublished - Dec 1 2011
Event25th International Workshop on Computer Science Logic, CSL 2011/20th Annual Conference of the European Association for Computer Science Logic, EACSL - Bergen, Norway
Duration: Sep 12 2011Sep 15 2011

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume12
ISSN (Print)1868-8969

Other

Other25th International Workshop on Computer Science Logic, CSL 2011/20th Annual Conference of the European Association for Computer Science Logic, EACSL
CountryNorway
CityBergen
Period9/12/119/15/11

Keywords

  • Automata theory
  • Boolean programs
  • Program synthesis
  • Temporal logics

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Synthesizing reactive programs'. Together they form a unique fingerprint.

Cite this