Murray: htdb2wiki: creating page for 2015c_fmh15-synt.html

2016-05-15T05:39:24Z

htdb2wiki: creating page for 2015c_fmh15-synt.html

New page

{{HTDB paper
| authors = Ioannis Filippidis, Richard M. Murray and Gerard J. Holzmann
| title = Synthesis from multi-paradigm specifications
| source = Submitted, 2015 Workshop on Synthesis (SYNT)
| year = 2015
| type = Conference Paper
| funding = TerraSwarm
| url = http://resolver.caltech.edu/CaltechCDSTR:2015.003
| abstract =
This work proposes a language for describing reactive synthesis problems that integrates imperative and declarative elements. The semantics is defined in terms of two-player turn-based infinite games with full information. Currently, synthesis tools accept linear temporal logic (LTL) as input, but this description is less structured and does not facilitate the expression of sequential constraints. This motivates the use of a structured programming language to specify synthesis problems. Transition systems and guarded commands serve as imperative constructs, expressed in a syntax based on that of the modeling language Promela. The syntax allows defining which player controls data and control flow, and separating a program into assumptions and guarantees. These notions are necessary for input to game solvers. The integration of imperative and declarative paradigms allows using the paradigm that is most appropriate for expressing each requirement. The declarative part is expressed in the LTL fragment of generalized reactivity(1), which admits efficient synthesis algorithms. The implementation translates Promela to input for the Slugs synthesizer and is written in Python.
| flags =
| filetype = link
| tag = fmh15-synt
| id = 2015c
}}

Synthesis from multi-paradigm specifications - Revision history

Murray: htdb2wiki: creating page for 2015c_fmh15-synt.html