Browse wiki

From MurrayWiki
Jump to: navigation, search
Synthesis from multi-paradigm specifications
Abstract This work proposes a language for describi …
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.
lugs synthesizer and is written in Python.  +
Authors Ioannis Filippidis, Richard M. Murray and Gerard J. Holzmann  +
Funding The TerraSwarm Research Center +
ID 2015c  +
Source Submitted, 2015 Workshop on Synthesis (SYNT)  +
Tag fmh15-synt  +
Title Synthesis from multi-paradigm specifications +
Type Conference Paper  +
Categories Papers
Modification date
This property is a special property in this wiki.
15 May 2016 05:39:24  +
This property is a special property in this wiki.  +
hide properties that link here 
Synthesis from multi-paradigm specifications + Title


Enter the name of the page to start browsing from.