Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/10278
Title: Synthesis of Reactive(1) designs
Authors: Bloem, Roderick
Jobstmann, Barbara
Piterman, Nir
Pnueli, Amir
Sa'Ar, Yaniv
First Published: 18-Aug-2011
Publisher: Elsevier
Citation: Journal of Computer and System Sciences, 2012, 78 (3), pp. 911-938.
Abstract: We address the problem of automatically synthesizing digital designs from linear-time specifications. We consider various classes of specifications that can be synthesized with effort quadratic in the number of states of the reactive system, where we measure effort in symbolic steps. The synthesis algorithm is based on a novel type of game called General Reactivity of rank 1 (GR(1)), with a winning condition of the form (⃞⃟p1⋀...⋀⃞⃟pm)➙(⃞⃟q1⋀...⋀⃞⃟qn), where each pi and qi is a Boolean combination of atomic propositions. We show symbolic algorithms to solve this game, to build a winning strategy and several ways to optimize the winning strategy and to extract a system from it. We also show how to use GR(1) games to solve the synthesis of LTL specifications in many interesting cases. As empirical evidence to the generality and efficiency of our approach we include a significant case study. We describe the formal specifications and the synthesis process applied to a bus arbiter, which is a realistic industrial hardware specification of modest size.
DOI Link: 10.1016/j.jcss.2011.08.007
ISSN: 0022-0000
eISSN: 1090-2724
Links: http://www.sciencedirect.com/science/article/pii/S0022000011000869
http://hdl.handle.net/2381/10278
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: Copyright © 2011 Elsevier Inc. Deposited with reference to the publisher's archiving policy available on the SHERPA/RoMEO website. NOTICE: this is the author’s version of a work that was accepted for publication in Journal of Computer and System Sciences. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Journal of Computer and System Sciences, 2012, 78 (3), pp. 911-938. DOI# 10.1016/j.jcss.2011.08.007
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
GROne.pdf525.2 kBUnknownView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.