A Caltech Library Service

A multi-paradigm language for reactive synthesis

Filippidis, Ioannis and Murray, Richard M. and Holzmann, Gerard J. (2016) A multi-paradigm language for reactive synthesis. Electronic Proceedings in Theoretical Computer Science (EPTCS), 202 . pp. 73-97. ISSN 2075-2180.

[img] PDF - Published Version
See Usage Policy.


Use this Persistent URL to link to this item:


This paper 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, extended with past LTL. The implementation translates Promela to input for the Slugs synthesizer and is written in Python. The AMBA AHB bus case study is revisited and synthesized efficiently, identifying the need to reorder binary decision diagrams during strategy construction, in order to prevent the exponential blowup observed in previous work.

Item Type:Article
Related URLs:
URLURL TypeDescription
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Additional Information:© 2015 I. Filippidis, R.M. Murray, G.J. Holzmann. The authors would like to thank Scott Livingston for providing helpful feedback. This work was supported by STARnet, 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.
Funding AgencyGrant Number
Semiconductor Research CorporationUNSPECIFIED
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Record Number:CaltechAUTHORS:20190410-120619515
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:94629
Deposited By: George Porter
Deposited On:11 Apr 2019 17:40
Last Modified:03 Oct 2019 21:05

Repository Staff Only: item control page