Please use this identifier to cite or link to this item:
Title: Effective synthesis of asynchronous systems from GR(1) specifications
Authors: Klein, Uri
Piterman, Nir
Pnueli, Amir
First Published: Jan-2012
Presented at: Verification, Model Checking, and Abstract Interpretation 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, 22-24 January 2012
Publisher: Springer Verlag
Citation: Lecture Notes in Computer Science, 2012, 7148, pp. 283-298.
Abstract: We consider automatic synthesis from linear temporal logic specifications for asynchronous systems. We aim the produced reactive systems to be used as software in a multi-threaded environment. We extend previous reduction of asynchronous synthesis to synchronous synthesis to the setting of multiple input and multiple output variables. Much like synthesis for synchronous designs, this solution is not practical as it requires determinization of automata on infinite words and solution of complicated games. We follow advances in synthesis of synchronous designs, which restrict the handled specifications but achieve scalability and efficiency. We propose a heuristic that, in some cases, maintains scalability for asynchronous synthesis. Our heuristic can prove that specifications are realizable and extract designs. This is done by a reduction to synchronous synthesis that is inspired by the theoretical reduction.
DOI Link: 10.1007/978-3-642-27940-9_19
ISSN: 0302-9743
eISSN: 1611-3349
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: © Springer-Verlag Berlin Heidelberg 2012. Deposited with reference to the publisher's archiving policy available on the SHERPA/RoMEO website. The original publication is available at
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
main.pdf364.79 kBUnknownView/Open

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