{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:45:19Z","timestamp":1725727519481},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642391750"},{"type":"electronic","value":"9783642391767"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39176-7_4","type":"book-chapter","created":{"date-parts":[[2013,5,30]],"date-time":"2013-05-30T08:58:44Z","timestamp":1369904324000},"page":"43-60","source":"Crossref","is-referenced-by-count":3,"title":["A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software"],"prefix":"10.1007","author":[{"given":"Vadim","family":"Alimguzhin","sequence":"first","affiliation":[]},{"given":"Federico","family":"Mari","sequence":"additional","affiliation":[]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[]},{"given":"Ivano","family":"Salvo","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11813040_1","volume-title":"FM 2006: Formal Methods","author":"T.A. Henzinger","year":"2006","unstructured":"Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 1\u201315. Springer, Heidelberg (2006)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-642-14295-6_20","volume-title":"Computer Aided Verification","author":"F. Mari","year":"2010","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Synthesis of quantized feedback control software for discrete time linear hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 180\u2013195. Springer, Heidelberg (2010)"},{"key":"4_CR3","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Model based synthesis of control software from system level formal specifications. ACM Trans. on Soft. Eng. and Meth. (to appear)"},{"key":"4_CR4","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Quantized feedback control software synthesis from system level formal specifications. CoRR abs\/1107.5638v1 (2011)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-48983-5_22","volume-title":"Hybrid Systems: Computation and Control","author":"C.J. Tomlin","year":"1999","unstructured":"Tomlin, C.J., Lygeros, J., Sastry, S.S.: Computing controllers for nonlinear hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569, pp. 238\u2013255. Springer, Heidelberg (1999)"},{"key":"4_CR6","unstructured":"Dean, J., Ghemawat, S.: Mapreduce: Simplified data processing on large clusters. In: OSDI, pp. 137\u2013150 (2004)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Lin, J., Dyer, C.: Data-Intensive Text Processing with MapReduce. Synthesis Lectures on Human Language Technologies. Morgan & Claypool Publishers (2010)","DOI":"10.2200\/S00274ED1V01Y201006HLT007"},{"key":"4_CR8","unstructured":"Pacheco, P.: Parallel Programming with MPI. Morgan Kaufmann (1997)"},{"issue":"2","key":"4_CR9","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1109\/TPEL.2009.2028732","volume":"25","author":"M. Rodriguez","year":"2010","unstructured":"Rodriguez, M., Fernandez-Miaja, P., Rodriguez, A., Sebastian, J.: A multiple-input digitally controlled buck converter for envelope tracking applications in radiofrequency power amplifiers. IEEE Trans. on Pow. El.\u00a025(2), 369\u2013381 (2010)","journal-title":"IEEE Trans. on Pow. El."},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/9.273337","volume":"39","author":"G. Kreisselmeier","year":"1994","unstructured":"Kreisselmeier, G., Birkh\u00f6lzer, T.: Numerical nonlinear regulator design. IEEE Trans. on Automatic Control\u00a039(1), 33\u201346 (1994)","journal-title":"IEEE Trans. on Automatic Control"},{"issue":"8","key":"4_CR11","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. on Computers"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: Automatic control software synthesis for quantized discrete time hybrid systems. In: CDC, pp. 6120\u20136125. IEEE (2012)","DOI":"10.1109\/CDC.2012.6426260"},{"issue":"1","key":"4_CR13","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/63.484413","volume":"11","author":"W.C. So","year":"1996","unstructured":"So, W.C., Tse, C., Lee, Y.S.: Development of a fuzzy logic controller for dc\/dc converters: design, computer simulation, and experimental evaluation. IEEE Trans. on Power Electronics\u00a011(1), 24\u201332 (1996)","journal-title":"IEEE Trans. on Power Electronics"},{"key":"4_CR14","unstructured":"Kim, W., Gupta, M.S., Wei, G.Y., Brooks, D.M.: Enabling on-chip switching regulators for multi-core processors using current staggering. In: ASGI (2007)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: On model based synthesis of embedded control software. In: EMSOFT (2012)","DOI":"10.1145\/2380356.2380398"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-24743-2_9","volume-title":"Hybrid Systems: Computation and Control","author":"A. Bemporad","year":"2004","unstructured":"Bemporad, A., Giorgetti, N.: A SAT-based hybrid solver for optimal control of hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 126\u2013141. Springer, Heidelberg (2004)"},{"key":"4_CR17","series-title":"LNEE","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-79142-3_10","volume-title":"Informatics in Control Automation and Robotics","author":"G. Penna Della","year":"2008","unstructured":"Della Penna, G., Magazzeni, D., Tofani, A., Intrigila, B., Melatti, I., Tronci, E.: Automated Generation of Optimal Controllers through Model Checking Techniques. In: Cetto, J.A., Ferrier, J.-L., Costa dias Pereira, J.M., Filipe, J. (eds.) Informatics in Control Automation and Robotics. LNEE, vol.\u00a015, pp. 107\u2013119. Springer, Heidelberg (2008)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Della Penna, G., Magazzeni, D., Mercorio, F., Intrigila, B.: UPMurphi: A tool for universal planning on pddl+ problems. In: ICAPS (2009)","DOI":"10.1609\/icaps.v19i1.13352"},{"issue":"4","key":"4_CR19","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.sysconle.2011.02.002","volume":"60","author":"M.J. Mazo","year":"2011","unstructured":"Mazo, M.J., Tabuada, P.: Symbolic approximate time-optimal control. Systems & Control Letters\u00a060(4), 256\u2013263 (2011)","journal-title":"Systems & Control Letters"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Jha, S., Seshia, S.A., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: EMSOFT, pp. 107\u2013116. ACM (2011)","DOI":"10.1145\/2038642.2038660"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal: Status & developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 456\u2013459. Springer, Heidelberg (1997)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-00602-9_7","volume-title":"Hybrid Systems: Computation and Control","author":"F. Cassez","year":"2009","unstructured":"Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic synthesis of robust and optimal controllers \u2013 an industrial case study. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol.\u00a05469, pp. 90\u2013104. Springer, Heidelberg (2009)"},{"issue":"1","key":"4_CR23","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/s10009-008-0094-x","volume":"11","author":"I. Melatti","year":"2009","unstructured":"Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G.: Parallel and distributed model checking in eddy. Int. J. Softw. Tools Technol. Transf.\u00a011(1), 13\u201325 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Legay, A.: Distributed parametric and statistical model checking. In: PDMC, pp. 30\u201342 (2011)","DOI":"10.4204\/EPTCS.72.4"},{"key":"4_CR25","first-page":"4","volume-title":"PDMC. PDMC-HIBI 2010","author":"J. Barnat","year":"2010","unstructured":"Barnat, J., Brim, L., Ceska, M., Rockai, P.: Divine: Parallel distributed model checker. In: PDMC. PDMC-HIBI 2010, pp. 4\u20137. IEEE Computer Society, Washington, DC (2010)"},{"issue":"6","key":"4_CR26","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1109\/87.726531","volume":"6","author":"W. Schubert","year":"1998","unstructured":"Schubert, W., Stengel, R.: Parallel synthesis of robust control systems. IEEE Trans. on Contr. Sys. Techn.\u00a06(6), 701\u2013706 (1998)","journal-title":"IEEE Trans. on Contr. Sys. Techn."},{"key":"4_CR27","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/1975482.1975486","volume-title":"Proceedings of the 7th FPGAworld Conference, FPGAworld 2010","author":"M. Jurikovi\u010d","year":"2010","unstructured":"Jurikovi\u010d, M., \u010ci\u010d\u00e1k, P., Jelemensk\u00e1, K.: Parallel controller design and synthesis. In: Proceedings of the 7th FPGAworld Conference, FPGAworld 2010, pp. 35\u201340. ACM, New York (2010)"},{"issue":"8","key":"4_CR28","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/0141-9331(94)90092-2","volume":"18","author":"J. Pardey","year":"1994","unstructured":"Pardey, J., Amroun, A., Bolton, M., Adamski, M.: Parallel controller synthesis for programmable logic devices. Microprocessors and Microsystems\u00a018(8), 451\u2013457 (1994)","journal-title":"Microprocessors and Microsystems"},{"key":"4_CR29","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Linear constraints as a modeling language for discrete time hybrid systems. In: ICSEA. IARIA (2012)"},{"issue":"3&4","key":"4_CR30","first-page":"212","volume":"5","author":"F. Mari","year":"2012","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Synthesizing control software from boolean relations. Int. J. on Advances in SW\u00a05(3&4), 212\u2013223 (2012)","journal-title":"Int. J. on Advances in SW"},{"key":"4_CR31","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Control software visualization. In: INFOCOMP. IARIA (2012)"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-32943-2_19","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"F. Mari","year":"2012","unstructured":"Mari, F., Melatti, I., Salvo, I., Tronci, E.: Undecidability of quantized state feedback control for discrete time linear hybrid systems. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol.\u00a07521, pp. 243\u2013258. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39176-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,2]],"date-time":"2023-07-02T00:42:53Z","timestamp":1688258573000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39176-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642391750","9783642391767"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39176-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}