{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:10:58Z","timestamp":1742379058334,"version":"3.40.1"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,1,28]],"date-time":"2012-01-28T00:00:00Z","timestamp":1327708800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2013,3]]},"DOI":"10.1007\/s10626-011-0127-6","type":"journal-article","created":{"date-parts":[[2012,1,27]],"date-time":"2012-01-27T01:16:56Z","timestamp":1327627016000},"page":"27-59","source":"Crossref","is-referenced-by-count":6,"title":["Using logic to solve the submodule construction problem"],"prefix":"10.1007","volume":"23","author":[{"given":"Gregor v.","family":"Bochmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,1,28]]},"reference":[{"issue":"3","key":"127_CR1","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M Abadi","year":"1995","unstructured":"Abadi M, Lamport L (1995) Conjoining specifications. ACM Trans Program Lang Syst 17(3):507\u2013534","journal-title":"ACM Trans Program Lang Syst"},{"key":"127_CR3","unstructured":"Aho AV, Sethi R, Ullman JD (1986) Compilers, principles, techniques and tools. Addison Wesley"},{"issue":"2","key":"127_CR4","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s00165-007-0045-4","volume":"20","author":"P Bhaduri","year":"2008","unstructured":"Bhaduri P, Ramesh S (2008) Interface synthesis and protocol conversion. Form Asp Comput 20(2):205\u2013224","journal-title":"Form Asp Comput"},{"key":"127_CR5","doi-asserted-by":"crossref","unstructured":"Bochmann GV (2002a) Submodule construction and supervisory control: a generalization. In: Proc of int conf on implementation and applications of automata (invited paper). Springer Lecture Notes","DOI":"10.1007\/3-540-36390-4_3"},{"key":"127_CR6","doi-asserted-by":"crossref","unstructured":"Bochmann GV (2002b) Submodule construction for specifications with input assumptions and output guarantees. In: Proc FORTE\u201902 (22st IFIP WG 6.1 international conference on formal techniques for networked and distributed systems). Chapman & Hall","DOI":"10.1007\/3-540-36135-9_2"},{"key":"127_CR7","volume-title":"Proc IFIP int conf on formal techniques for distributed systems, LNCS 5522","author":"GV Bochmann","year":"2009","unstructured":"Bochmann GV (2009) Using first-order logic to reason about submodule construction. In: Proc IFIP int conf on formal techniques for distributed systems, LNCS 5522. Springer, Lisbon, Portugal"},{"key":"127_CR8","unstructured":"Bochmann GV, Merlin PM (1980) On the construction of communication protocols. In: ICCC, pp\u00a0371\u2013378 (reprinted in Sunshine C (ed) (1981) Communication protocol modeling, Artech House Publ.; Russian translation: Problems of Intern. Center for Science and Techn. Information, Moscow, 1981, no. 2, pp 146\u2013155. See also Merlin P, Bochmann G V (1983) On the construction of submodule specifications and communication protocols. ACM Trans Program Lang Syst 5(1):1\u201325)"},{"issue":"2","key":"127_CR9","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1109\/9.272327","volume":"39","author":"BA Brandin","year":"1994","unstructured":"Brandin BA, Wonham WM (1994) Supervisory control of timed discrete-event systems. IEEE Trans Automat Contr 39(2):329\u2013342","journal-title":"IEEE Trans Automat Contr"},{"key":"127_CR10","unstructured":"Broy M (1995) Advanced component interface specification. In: Proc TPPP\u201994. Lecture notes in CS 907, pp 369\u2013392"},{"key":"127_CR11","doi-asserted-by":"crossref","unstructured":"Buffalov S, El-Fakih K, Yevtushenko N, Bochmann GV (2003) Progressive solutions to a parallel automata equation. In: Proc FORTE conf (IFIP), Berlin, LNCS 2767, Springer, pp 367\u2013382","DOI":"10.1007\/978-3-540-39979-7_24"},{"key":"127_CR12","doi-asserted-by":"crossref","unstructured":"Daou B, Bochmann GV (2005) Submodule construction for extended state machine models. In: Proc IFIP int\u2019l conf on formal techniques for networked and distributed systems - FORTE 2005, Taiwan, Springer LNCS 3731, pp 396\u2013410","DOI":"10.1007\/11562436_29"},{"key":"127_CR13","unstructured":"De Luca A, Henzinger TA (2001) Interface automata. In: Proc 8th European software engineering conf held jointly with 9th ACM SIGSOFT FSE 2001, pp 109\u2013120"},{"key":"127_CR14","unstructured":"Drissi J, Bochmann GV (1999) Submodule construction tool. In: Mohammadian M (ed) Proc int conf on computational intelligence for modelling, control and automation, Vienne, IOS Press, pp 319\u2013324"},{"key":"127_CR15","unstructured":"Drissi J, Bochmann GV (2000) Submodule construction for systems of timed I\/O automata. Technical report (see also Drissi J, PhD thesis, University of Montreal, in French)"},{"issue":"1999","key":"127_CR16","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1016\/S0950-5849(99)00014-2","volume":"41","author":"E Haghverdi","year":"1999","unstructured":"Haghverdi E, Ural H (1999) Submodule construction from concurrent system specifications. Inform Software Tech (Elsevier) 41(1999):499\u2013506","journal-title":"Inform Software Tech (Elsevier)"},{"key":"127_CR17","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"127_CR18","unstructured":"Kelekar SGH (1994) Synthesis of protocols and protocol converters using the submodule construction approach. In: Danthine A, et al (eds) Proc PSTV, XIII"},{"key":"127_CR19","unstructured":"Kim T, Villa T, Brayton R, Sangiovanni-Vincentelli A (1997) Synthesis of FSMs: functional optimization. Kluwer Academic Publishers"},{"issue":"3","key":"127_CR20","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1023\/A:1008258331497","volume":"7","author":"R Kumar","year":"1997","unstructured":"Kumar R, Nelvagar S, Marcus SI (1997) A discrete event systems approach for protocol conversion. Discret Event Dyn Syst 7(3):295\u2013315. doi: 10.1023\/A:1008258331497","journal-title":"Discret Event Dyn Syst"},{"key":"127_CR21","unstructured":"Larsen KG, Xinxin L (1990) Equation solving using modal transition systems. In: Proc IEEE symp on logic in computer science, pp 108\u2013117"},{"issue":"3","key":"127_CR22","first-page":"219","volume":"2","author":"NA Lynch","year":"1989","unstructured":"Lynch NA, Tuttle MR (1989) An introduction to input\/output automata. CWI Quarterly 2(3):219\u2013246","journal-title":"CWI Quarterly"},{"key":"127_CR23","first-page":"229","volume-title":"STACS 95, annual symp. on theoretical aspects of computer science","author":"O Maler","year":"1995","unstructured":"Maler O, Pnueli A, Sifakis J (1995) On the synthesis of discrete controllers for timed systems. In: STACS 95, annual symp. on theoretical aspects of computer science, Berlin, Springer, pp 229\u2013242"},{"issue":"4","key":"127_CR24","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1991","unstructured":"Misra J, Chandy KM (1991) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417\u2013426","journal-title":"IEEE Trans Softw Eng"},{"issue":"2","key":"127_CR25","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0304-3975(89)90128-X","volume":"68","author":"J Parrow","year":"1989","unstructured":"Parrow J (1989) Submodule construction as equation solving in CCS. Theor Comp Sci 68(2):175\u2013202","journal-title":"Theor Comp Sci"},{"key":"127_CR26","volume-title":"Proc of IFIP FORTE\/PSTV\u201998 conf","author":"A Petrenko","year":"1998","unstructured":"Petrenko A, Yevtushenko N (1998) Solving asynchronous equations. In: Proc of IFIP FORTE\/PSTV\u201998 conf, Paris, Chapman-Hall"},{"key":"127_CR27","doi-asserted-by":"crossref","first-page":"1236","DOI":"10.1016\/S0140-3664(96)01157-7","volume":"19","author":"A Petrenko","year":"1996","unstructured":"Petrenko A, Yevtushenko N, Bochmann GV, Dssouli R (1996) Testing in context: framework and test derivation. Computer Communications Journal, Special Issue on Protocol Engineering 19:1236\u20131249","journal-title":"Computer Communications Journal, Special Issue on Protocol Engineering"},{"key":"127_CR28","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/BF01245634","volume":"3","author":"H Qin","year":"1991","unstructured":"Qin H, Lewis P (1991) Factorisation of finite state machines under strong and observational equivalences. J Form Asp Comput 3(2):284\u2013307. doi: 10.1007\/BF01245634","journal-title":"J Form Asp Comput"},{"issue":"1","key":"127_CR29","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJG Ramadge","year":"1989","unstructured":"Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81\u201398","journal-title":"Proc IEEE"},{"key":"127_CR30","unstructured":"Tao ZP, Bochmann GV, Dssouli R (1995) A model and an algorithm of subsystem construction. In: Proceedings of the eighth international conference on parallel and distributed computing systems, 21\u201323 Sept 1995. Orlando, Florida, USA, pp 619\u2013622"},{"key":"127_CR31","unstructured":"Tao Z, Bochmann GV, Dssouli R (1997) A formal method for synthesizing optimized protocol converters and its application to mobile data networks. Publisher: Baltzer, ACM Press, Netherlands. Mob Netw Appl 2(3):259\u2013269"},{"issue":"4","key":"127_CR32","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/BF01439153","volume":"5","author":"JG Thistle","year":"1995","unstructured":"Thistle JG (1995) On control of systems modelled as deterministic Rabin automata. Discret Event Dyn Syst 5(4):357\u2013381. doi: 10.1007\/BF01439153","journal-title":"Discret Event Dyn Syst"},{"key":"127_CR33","doi-asserted-by":"crossref","unstructured":"Tretmans J (1996) Test generation with inputs, outputs and quiescence. In: Proc 2nd international workshop on tools and algorithms for construction and analysis of systems (TACAS), Springer, pp 127\u2013146","DOI":"10.1007\/3-540-61042-1_42"},{"key":"127_CR34","unstructured":"Yevtushenko N, Villa T, Brayon R, Petrenko A, Sangiovanni-Vincentelli A (2000) Synthesis by language equation solving (exended abstract). In: Proc of annual intern workshop on logic synthesis, 2000, 11\u201314, complete paper in conference on Computer-Aided Design (ICCAD \u201901), 2001, pp 103; see also Solving equations in logic synthesis. Technical Report, Tomsk State University, Tomck 1999, 27 p (in Russian) or Sequential synthesis by language equation solving. http:\/\/www.cs.berkeley.edu\/~bodik\/teaching\/cs294\/papers\/language.pdf"},{"issue":"1","key":"127_CR35","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/s10626-007-0031-2","volume":"18","author":"N Yevtushenko","year":"2008","unstructured":"Yevtushenko N, Villa T, Brayton R, Petrenko A, Vincentelli AS (2008) Compositionally progressive solutions of synchronous FSM equations. Discret Event Dyn Syst 18(1):51\u201389","journal-title":"Discret Event Dyn Syst"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-011-0127-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-011-0127-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-011-0127-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T09:10:21Z","timestamp":1742375421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-011-0127-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,28]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["127"],"URL":"https:\/\/doi.org\/10.1007\/s10626-011-0127-6","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"type":"print","value":"0924-6703"},{"type":"electronic","value":"1573-7594"}],"subject":[],"published":{"date-parts":[[2012,1,28]]}}}