CaltechAUTHORS
  A Caltech Library Service

Synthesis from multi-paradigm specifications

Filippidis, Ioannis and Murray, Richard M. and Holzmann, Gerard J. (2015) Synthesis from multi-paradigm specifications. California Institute of Technology , Pasadena, CA. (Unpublished) http://resolver.caltech.edu/CaltechCDSTR:2015.003

[img] PDF (March 9, 2015 draft) - Draft Version
See Usage Policy.

563Kb
[img] PDF (May 11, 2015 updated draft) - Updated Version
See Usage Policy.

608Kb

Use this Persistent URL to link to this item: 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.


Item Type:Report or Paper (Technical Report)
Related URLs:
URLURL TypeDescription
https://github.com/johnyf/openpromelaRelated ItemSoftware implementation
https://github.com/johnyf/promelaRelated ItemSoftware implementation
ORCID:
AuthorORCID
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Contact Email Address:jfilippidis@gmail.com
Additional Information:© 2015 by the authors. This work was supported in part by the TerraSwarm Research Center, one of six centers supported by the STARnet phase of the Focus Center Research Program (FCRP) a Semiconductor Research Corporation program sponsored by MARCO and DARPA. The first author was partially supported by a graduate research fellowship from the Jet Propulsion Laboratory, over the summer of 2014. The authors would like to thank Scott Livingston for providing helpful comments on an early draft of this document.
Group:Control and Dynamical Systems Technical Reports
Funders:
Funding AgencyGrant Number
TerraSwarmUNSPECIFIED
STARnetUNSPECIFIED
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
JPLUNSPECIFIED
Subject Keywords:Reactive synthesis, Generalized Reactivity(1), Linear temporal logic, Infinite games, Promela
Record Number:CaltechCDSTR:2015.003
Persistent URL:http://resolver.caltech.edu/CaltechCDSTR:2015.003
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:54378
Collection:CaltechCDSTR
Deposited By: Ioannis Filippidis
Deposited On:10 Mar 2015 19:12
Last Modified:13 May 2015 21:35

Repository Staff Only: item control page