@inproceedings{pnueli_synthesis_1989,
	address = {New York, NY, USA},
	series = {{POPL} '89},
	title = {On the synthesis of a reactive module},
	isbn = {978-0-89791-294-5},
	url = {https://doi.org/10.1145/75277.75293},
	doi = {10.1145/75277.75293},
	abstract = {We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(x, y) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm for constructing the program whenever it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees in time exponential in the number of pairs, but only polynomial in the number of states. This leads to a synthesis algorithm whose complexity is double exponential in the length of the given specification.},
	urldate = {2022-12-23},
	booktitle = {Proceedings of the 16th {ACM} {SIGPLAN}-{SIGACT} symposium on {Principles} of programming languages},
	publisher = {Association for Computing Machinery},
	author = {Pnueli, A. and Rosner, R.},
	month = jan,
	year = {1989},
	pages = {179--190},
}

{"_id":"a9bc8Q9DMkYbRHLFt","bibbaseid":"pnueli-rosner-onthesynthesisofareactivemodule-1989","author_short":["Pnueli, A.","Rosner, R."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"New York, NY, USA","series":"POPL '89","title":"On the synthesis of a reactive module","isbn":"978-0-89791-294-5","url":"https://doi.org/10.1145/75277.75293","doi":"10.1145/75277.75293","abstract":"We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(x, y) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm for constructing the program whenever it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees in time exponential in the number of pairs, but only polynomial in the number of states. This leads to a synthesis algorithm whose complexity is double exponential in the length of the given specification.","urldate":"2022-12-23","booktitle":"Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","publisher":"Association for Computing Machinery","author":[{"propositions":[],"lastnames":["Pnueli"],"firstnames":["A."],"suffixes":[]},{"propositions":[],"lastnames":["Rosner"],"firstnames":["R."],"suffixes":[]}],"month":"January","year":"1989","pages":"179–190","bibtex":"@inproceedings{pnueli_synthesis_1989,\n\taddress = {New York, NY, USA},\n\tseries = {{POPL} '89},\n\ttitle = {On the synthesis of a reactive module},\n\tisbn = {978-0-89791-294-5},\n\turl = {https://doi.org/10.1145/75277.75293},\n\tdoi = {10.1145/75277.75293},\n\tabstract = {We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(x, y) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm for constructing the program whenever it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees in time exponential in the number of pairs, but only polynomial in the number of states. This leads to a synthesis algorithm whose complexity is double exponential in the length of the given specification.},\n\turldate = {2022-12-23},\n\tbooktitle = {Proceedings of the 16th {ACM} {SIGPLAN}-{SIGACT} symposium on {Principles} of programming languages},\n\tpublisher = {Association for Computing Machinery},\n\tauthor = {Pnueli, A. and Rosner, R.},\n\tmonth = jan,\n\tyear = {1989},\n\tpages = {179--190},\n}\n\n\n\n\n\n\n\n","author_short":["Pnueli, A.","Rosner, R."],"key":"pnueli_synthesis_1989","id":"pnueli_synthesis_1989","bibbaseid":"pnueli-rosner-onthesynthesisofareactivemodule-1989","role":"author","urls":{"Paper":"https://doi.org/10.1145/75277.75293"},"metadata":{"authorlinks":{}},"downloads":0,"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/alukina","dataSources":["Cfgnp5s4HQSBd8tAf"],"keywords":[],"search_terms":["synthesis","reactive","module","pnueli","rosner"],"title":"On the synthesis of a reactive module","year":1989}