{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:17:42Z","timestamp":1781075862791,"version":"3.54.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319133379","type":"print"},{"value":"9783319133386","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-13338-6_7","type":"book-chapter","created":{"date-parts":[[2014,11,3]],"date-time":"2014-11-03T03:35:45Z","timestamp":1414985745000},"page":"75-91","source":"Crossref","is-referenced-by-count":30,"title":["Synthesizing Finite-State Protocols from Scenarios and Requirements"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Milo","family":"Martin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mukund","family":"Raghothaman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christos","family":"Stergiou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Abhishek","family":"Udupa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"ITU Telecommunication Standardization Sector: ITU-R recommendation Z.120, Message Sequence Charts (MSC 1996) (May 1996)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2008) (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"7_CR3","volume-title":"Computer Networking: A Top-Down Approach","author":"J.F. Kurose","year":"2009","unstructured":"Kurose, J.F., Ross, K.W.: Computer Networking: A Top-Down Approach, 5th edn. Addison-Wesley Publishing Company, USA (2009)","edition":"5"},{"key":"7_CR4","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (2000)"},{"key":"7_CR5","unstructured":"Lynch, N.A.: Distributed algorithms. Morgan Kaufmann (1996)"},{"key":"7_CR6","first-page":"81","volume":"77","author":"P. Ramadge","year":"1989","unstructured":"Ramadge, P., Wonham, W.: The control of discrete event systems. IEEE Transactions on Control Theory\u00a077, 81\u201398 (1989)","journal-title":"IEEE Transactions on Control Theory"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages (1989)","DOI":"10.1145\/75277.75293"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci.\u00a078(3) (2012)","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: 31st Annual Symposium on Foundations of Computer Science, pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"issue":"1","key":"7_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.ipl.2004.01.004","volume":"90","author":"S. Tripakis","year":"2004","unstructured":"Tripakis, S.: Undecidable Problems of Decentralized Observation and Control on Regular Languages. Information Processing Letters\u00a090(1), 21\u201328 (2004)","journal-title":"Information Processing Letters"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: IEEE Symposium on Logic in Computer Science, pp. 321\u2013330 (2005)","DOI":"10.1109\/LICS.2005.53"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Lamouchi, H., Thistle, J.: Effective control synthesis for DES under partial observations. In: 39th IEEE Conference on Decision and Control, pp. 22\u201328 (2000)","DOI":"10.1109\/CDC.2000.912726"},{"issue":"5-6","key":"7_CR13","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B. Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Software Tools for Tchnology Transfer\u00a015(5-6), 519\u2013539 (2013)","journal-title":"Software Tools for Tchnology Transfer"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-78800-3_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Katz","year":"2008","unstructured":"Katz, G., Peled, D.: Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 141\u2013156. Springer, Heidelberg (2008)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-19237-1_13","volume-title":"Hardware and Software: Verification and Testing","author":"G. Katz","year":"2011","unstructured":"Katz, G., Peled, D.: Synthesizing solutions to the leader election problem using model checking and genetic programming. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol.\u00a06405, pp. 117\u2013132. Springer, Heidelberg (2011)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. IEEE Transactions on Software Engineering\u00a029(7) (2003)","DOI":"10.1109\/TSE.2003.1214326"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans. Softw. Eng. 29(2) (2003)","DOI":"10.1109\/TSE.2003.1178048"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2012)","DOI":"10.1145\/2103656.2103680"},{"issue":"7","key":"7_CR19","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/2209249.2209270","volume":"55","author":"D. Harel","year":"2012","unstructured":"Harel, D., Marron, A., Weiss, G.: Behavioral programming. Commun. ACM\u00a055(7), 90\u2013100 (2012)","journal-title":"Commun. ACM"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1) (2001)","DOI":"10.1023\/A:1011227529550"},{"issue":"3","key":"7_CR21","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1109\/TSE.2009.89","volume":"36","author":"B. Bollig","year":"2010","unstructured":"Bollig, B., Katoen, J., Kern, C., Leucker, M.: Learning Communicating Automata from MSCs. IEEE Transactions on Software Engineering\u00a036(3), 390\u2013408 (2010)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Leary, J., Talupur, M., Tuttle, M.R.: Protocol verification using flows: An industrial experience. In: Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 172\u2013179 (November 2009)","DOI":"10.1109\/FMCAD.2009.5351126"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R., Bodik, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Proceedings of the 2005 ACM Conference on Programming Language Design and Implementation (2005)","DOI":"10.1145\/1065010.1065045"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: Transit: specifying protocols with concolic snippets. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, pp. 287\u2013296 (2013)","DOI":"10.1145\/2491956.2462174"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Alur, R., Martin, M.M.K., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. CoRR abs\/1402.7150 (2014)","DOI":"10.1007\/978-3-319-13338-6_7"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-13338-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T04:21:16Z","timestamp":1746505276000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-13338-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319133379","9783319133386"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-13338-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}