{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:34:59Z","timestamp":1791459299200,"version":"4.3.4"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,2,1]],"date-time":"2013-02-01T00:00:00Z","timestamp":1359676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"FSE 2010 in Santa Fe, New Mexico"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2013,2]]},"abstract":"<jats:p>We present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behavior models. Our approach works for an expressive subset of liveness properties, distinguishes between controlled and monitored actions, and differentiates system goals from environment assumptions. We show that assumptions must be modeled carefully in order to avoid synthesizing anomalous behavior models. We characterize nonanomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline.<\/jats:p>","DOI":"10.1145\/2430536.2430543","type":"journal-article","created":{"date-parts":[[2013,3,5]],"date-time":"2013-03-05T15:28:36Z","timestamp":1362497316000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":52,"title":["Synthesizing nonanomalous event-based controllers for liveness goals"],"prefix":"10.1145","volume":"22","author":[{"given":"Nicol\u00e1s","family":"D'ippolito","sequence":"first","affiliation":[{"name":"Imperial College London, London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor","family":"Braberman","sequence":"additional","affiliation":[{"name":"Universidad de Buenos Aires"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[{"name":"Leicester University, Leicester"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebasti\u00e1n","family":"Uchitel","sequence":"additional","affiliation":[{"name":"Universidad de Buenos Aires and Imperial College London, London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,3,4]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Ed. Lecture Notes in Computer Science Series","volume":"2742","author":"Armoni R."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the IFAC Symposium on System Structure and Control.","author":"Asarin E."},{"key":"e_1_2_1_3_1","unstructured":"Autili M. Inverardi P. Tivoli M. and Garlan D. 2004. Synthesis of \u201ccorrect\u201d adaptors for protocol enhancement in component-based systems. In Specification and Verification of Component-Based Systems. ACM 79.  Autili M. Inverardi P. Tivoli M. and Garlan D. 2004. Synthesis of \u201ccorrect\u201d adaptors for protocol enhancement in component-based systems. In Specification and Verification of Component-Based Systems. ACM 79."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/196244.196575"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV '97)","author":"Beer I."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008779610539"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the IJCAI'01 Workshop on Planning under Uncertainty and Incomplete Information.","author":"Bertoli P."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595719"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe (DATE '07)","author":"Bloem R."},{"key":"e_1_2_1_10_1","unstructured":"Bontemps Y. Schobbens P.-Y. and L\u00f6ding C. 2004. Synthesis of open reactive systems from scenario-based specifications. Fundamenta Informaticae - Application of Concurrency to System Design (ACSD'03). 62 139--169.   Bontemps Y. Schobbens P.-Y. and L\u00f6ding C. 2004. Synthesis of open reactive systems from scenario-based specifications. Fundamenta Informaticae - Application of Concurrency to System Design (ACSD'03). 62 139--169."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Buchi J. and Landweber L. 1969. Solving sequential conditions by finite-state strategies. Trans. AMS. 295--311.  Buchi J. and Landweber L. 1969. Solving sequential conditions by finite-state strategies. Trans. AMS. 295--311.","DOI":"10.1090\/S0002-9947-1969-0280205-0"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_14"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 10th International Conference on Fundamental Approaches to Software Engineering (FASE'07)","author":"Chechik M."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03)","author":"Cobleigh J. M."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02144-2_22"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181800"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.78"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882305"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985823"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_10"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703420675"},{"key":"e_1_2_1_24_1","unstructured":"Gat E. Bonnasso R. P. Murphy R. and Press A. 1997. On three-layer architectures. In Artificial Intelligence and Mobile Robots. AAAI Press 195--210.   Gat E. Bonnasso R. P. Murphy R. and Press A. 1997. On three-layer architectures. In Artificial Intelligence and Mobile Robots. AAAI Press 195--210."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940106"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/647868.737106"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_11"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Gurfinkel A. and Chechik M. 2004. How vacuous is vacuous&quest; In Tools and Algorithms for the Construction and Analysis of Systems 451--466.  Gurfinkel A. and Chechik M. 2004. How vacuous is vacuous&quest; In Tools and Algorithms for the Construction and Analysis of Systems 451--466.","DOI":"10.1007\/978-3-540-24730-2_34"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02161-9_6"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 1st International Conference on Autonomic Computing. IEEE Computer Society","author":"Huang A.-C."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294904.1294908"},{"key":"e_1_2_1_33_1","unstructured":"Jackson M. 1995a. Software Requirements&Specifications: A Lexicon of Practice Principles and Prejudices. ACM Press\/Addison-Wesley Publishing Co. New York.   Jackson M. 1995a. Software Requirements&Specifications: A Lexicon of Practice Principles and Prejudices. ACM Press\/Addison-Wesley Publishing Co. New York."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/225014.225041"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/646514.695804"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1030033.1030074"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.01.006"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOSE.2007.19"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2005.66"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the 5th IEEE International Symposium on Requirements Engineering. IEEE Computer Society Washington, DC.","author":"Lamsweerde A. V.","year":"2001"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-008-0027-7"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/581339.581353"},{"key":"e_1_2_1_47_1","volume-title":"Formal Development of Reactive Systems - Case Study Production Cell. Lecture Notes in Computer Science Series","volume":"891","author":"Lewerentz C."},{"key":"e_1_2_1_48_1","first-page":"219","article-title":"An introduction to input\/output automata","volume":"2","author":"Lynch N.","year":"1989","journal-title":"CWI Quart."},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS). Lecture Notes in Computer Science","volume":"95","author":"Maler O."},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag New York Inc. New York.   Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag New York Inc. New York.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)96871-J"},{"key":"e_1_2_1_52_1","volume-title":"Eds. Lecture Notes in Computer Science Series","volume":"3192","author":"Pistore M."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_24"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"key":"e_1_2_1_57_1","volume-title":"Artificial Intelligence: A Modern Approach","author":"Russell S.","year":"1995"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the 5th International Conference on Automated Technology for Verification and Analysis (ATVA'07)","author":"Schewe S."},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science Series","volume":"4905","author":"Sohail S."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292316.1292318"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.107"},{"key":"e_1_2_1_62_1","unstructured":"van Lamsweerde A. 2009. Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley.   van Lamsweerde A. 2009. Requirements Engineering - From System Goals to UML Models to Software Specifications. Wiley."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.879820"},{"key":"e_1_2_1_64_1","volume-title":"Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE","author":"Young M.","year":"2005"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/237432.237434"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2430536.2430543","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2430536.2430543","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:23Z","timestamp":1750221323000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2430536.2430543"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2]]},"references-count":65,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["10.1145\/2430536.2430543"],"URL":"https:\/\/doi.org\/10.1145\/2430536.2430543","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,2]]},"assertion":[{"value":"2011-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-03-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}