{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:40:25Z","timestamp":1759333225409},"reference-count":42,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.326.14","type":"journal-article","created":{"date-parts":[[2020,9,20]],"date-time":"2020-09-20T06:06:25Z","timestamp":1600581985000},"page":"216-233","source":"Crossref","is-referenced-by-count":3,"title":["The Quotient in Preorder Theories"],"prefix":"10.4204","volume":"326","author":[{"given":"\u00cd\u00f1igo X.","family":"\u00cdncer Romeo","sequence":"first","affiliation":[{"name":"University of California, Berkeley"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"Mangeruca","sequence":"additional","affiliation":[{"name":"Raytheon Technologies Research Center,  Rome, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tiziano","family":"Villa","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Verona, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[{"name":"University of California, Berkeley"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"2720","published-online":{"date-parts":[[2020,9,20]]},"reference":[{"issue":"10","key":"S1S-tcad2000","doi-asserted-by":"publisher","first-page":"1149","DOI":"10.1109\/43.875301","article-title":"Sequential synthesis using S1S","volume":"19","author":"Aziz","year":"2000","journal-title":"IEEE Transactions on Computer-Aided Design"},{"issue":"4","key":"barrett-deds98","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1023\/A:1008301317459","article-title":"Bisimulation, the Supervisory Control Problem and Strong Model Matching for Finite State Machines","volume":"8","author":"Barrett","year":"1998","journal-title":"Discrete Event Dynamic Systems: Theory & Applications"},{"key":"benes2013","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-40184-8_7","article-title":"Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"Bene\u0161","year":"2013"},{"key":"multViewpoint","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-92188-2_9","article-title":"Multiple Viewpoint Contract-Based Specification and Design","volume-title":"Formal Methods for Components and Objects","author":"Benveniste","year":"2007"},{"key":"BenvenisteContractBook","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","article-title":"Contracts for System Design","volume":"12","author":"Benveniste","year":"2018","journal-title":"Foundations and Trends^89.5-.3em in Electronic Design Automation"},{"issue":"2","key":"bhaduri08","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s00165-007-0045-4","article-title":"Interface synthesis and protocol conversion","volume":"20","author":"Bhaduri","year":"2008","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"bochmann-deds2013","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s10626-011-0127-6","article-title":"Using logic to solve the submodule construction problem","volume":"23","author":"Bochmann","year":"2013","journal-title":"Discrete Event Dynamic Systems"},{"issue":"2","key":"bouyer2011","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/s10849-010-9127-4","article-title":"Timed Modal Logics for Real-Time Systems - Specification, Verification and Control","volume":"20","author":"Bouyer","year":"2011","journal-title":"Journal of Logic, Language and Information"},{"key":"burch-comb-cycle","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1109\/ICCAD.1993.580149","article-title":"Modelling hierarchical combinational circuits","volume-title":"The Proceedings of the International Conference on Computer-Aided Design","author":"Burch","year":"1993"},{"key":"cassez2000","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/10722167_29","article-title":"Model-Checking for Hybrid Systems by Quotienting and Constraints Solving","volume-title":"Computer Aided Verification","author":"Cassez","year":"2000"},{"key":"Castagnetti:SEFM-2015","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-662-49224-6_23","article-title":"Automated Synthesis of Protocol Converters with BALM-II","volume-title":"Software Engineering and Formal Methods. SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART. York, UK, September 7-8, 2015","author":"Castagnetti","year":"2015"},{"issue":"8","key":"cerny-marin77","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1109\/TC.1977.1674912","article-title":"An approach to unified methodology of combinational switching circuits","volume":"vol. C-26","author":"Cerny","year":"1977","journal-title":"IEEE Transactions on Computers"},{"key":"verhoeff-mpc1989","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-51305-1_10","article-title":"Networks of communicating processes and their \\voidb@x (de-)composition","volume-title":"Mathematics of Program Construction","volume":"375","author":"Chen","year":"1989"},{"key":"dealfaro-interface03","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-39910-0_12","article-title":"Game Models for Open Systems","volume-title":"Verification: Theory and Practice","volume":"2772","author":"De Alfaro","year":"2003"},{"issue":"5","key":"deAlfaro2001","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/503209.503226","article-title":"Interface Automata","volume":"26","author":"De Alfaro","year":"2001","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"11","key":"mm-tac01","doi-asserted-by":"publisher","first-page":"1726","DOI":"10.1109\/9.964683","article-title":"Model Matching for Finite State Machines","volume":"46","author":"Di Benedetto","year":"2001","journal-title":"IEEE Transactions on Automatic Control"},{"key":"iwls10:ch2","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-1-4615-0817-5_2","article-title":"Multi-Level Logic Optimization","volume-title":"Logic Synthesis and Verification","author":"Fujita","year":"2001"},{"issue":"3","key":"green-tcomm-1986","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1109\/32.4655","article-title":"Protocol Conversion","volume":"34","author":"Green","year":"1986","journal-title":"IEEE Transactions on Communications"},{"issue":"8","key":"haghverdi99","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1016\/S0950-5849(99)00014-2","article-title":"Submodule construction from concurrent system specifications","volume":"41","author":"Haghverdi","year":"1999","journal-title":"Information and Software Technology"},{"key":"hallal-conv2000","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1109\/ICECS.2000.912975","article-title":"Design of divergence-free protocol converters using supervisory control techniques","volume-title":"7th IEEE International Conference on Electronics, Circuits and Systems, ICECS 2000","volume":"2","author":"Hallal","year":"2000"},{"key":"iwls10:ch9","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-1-4615-0817-5_2","article-title":"Optimization of Synchronous Circuits","volume-title":"Logic Synthesis and Verification","author":"Hassoun","year":"2001"},{"key":"ullman-automata2","doi-asserted-by":"publisher","DOI":"10.1145\/568438.568455","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft","year":"2001"},{"key":"fsm1-book","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2622-0","volume-title":"Synthesis of FSMs: Functional Optimization","author":"Kam","year":"1997"},{"key":"kim72","doi-asserted-by":"publisher","first-page":"1440","DOI":"10.1109\/T-C.1972.223521","article-title":"The simplification of sequential machines with input restrictions","author":"Kim","year":"1972","journal-title":"IRE Transactions on Electronic Computers"},{"issue":"3","key":"kumar-conv97","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1023\/A:1008258331497","article-title":"A discrete event systems approach for protocol conversion","volume":"7","author":"Kumar","year":"1997","journal-title":"Discrete Event Dynamic Systems: Theory & Applications"},{"key":"kurshan-asynch99","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/3-540-60045-0_61","article-title":"Modelling asynchrony with a synchronous model","volume":"vol. 15","author":"Kurshan","year":"1999","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"lam-tse-1988","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1109\/32.4655","article-title":"Protocol Conversion","volume":"14","author":"Lam","year":"1988","journal-title":"IEEE Trans. Softw. Eng."},{"key":"larsen-xinxin1990","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1109\/LICS.1990.113738","article-title":"Equation solving using modal transition systems","volume-title":"Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e","author":"Larsen","year":"1990"},{"issue":"3","key":"lynch-cwi89","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1.1.83.7751","article-title":"An introduction to Input\/Output automata","volume":"2","author":"Lynch","year":"1989","journal-title":"CWI-Quarterly"},{"key":"mallon99","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1109\/ASYNC.1999.761537","article-title":"Analysis and Applications of the XDI Model","volume-title":"International Symposium on Advanced Research in Asynchronous Circuits and Systems","author":"Mallon","year":"1999"},{"issue":"1","key":"boch83","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/357195.357196","article-title":"On the Construction of Submodule Specifications and Communication Protocols","volume":"5","author":"Merlin","year":"1983","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"negu-concur00","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-44618-4_16","article-title":"Process spaces","volume-title":"Proceedings of CONCUR 2000, 11th International Conference on Concurrency Theory","volume":"1877","author":"Negulescu","year":"2000"},{"key":"DBLP:conf\/iccad\/PasseroneAHS02","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1145\/774572.774592","article-title":"Convertibility verification and converter synthesis: two faces of the same coin","volume-title":"ICCAD","author":"Passerone","year":"2002"},{"key":"contractMerging","doi-asserted-by":"publisher","DOI":"10.1145\/3358216","article-title":"Coherent Extension, Composition, and Merging Operators in Contract Models for System Design","volume":"18","author":"Passerone","year":"2019","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"DBLP:conf\/dac\/PasseroneRS98","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/277044.277047","article-title":"Automatic Synthesis of Interfaces Between Incompatible Protocols","volume-title":"DAC","author":"Passerone","year":"1998"},{"key":"raclet2011modal","doi-asserted-by":"publisher","first-page":"119","DOI":"10.3233\/FI-2011-416","article-title":"A modal interface theory for component-based design","volume":"108","author":"Raclet","year":"2011","journal-title":"Fundamenta Informaticae"},{"key":"agquotient","series-title":"MEMOCODE \u201918","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556872","article-title":"Quotient for Assume-Guarantee Contracts","volume-title":"16th ACM-IEEE International Conference on Formal Methods and Models for System Design","author":"\u00cdncer Romeo","year":"2018"},{"key":"iwls10:ch3","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-1-4615-0817-5_2","article-title":"Flexibility in Logic","volume-title":"Logic Synthesis and Verification","author":"Sentovich","year":"2001"},{"issue":"11","key":"ucp-ieeeproc2015","doi-asserted-by":"publisher","first-page":"2152","DOI":"10.1109\/JPROC.2015.2450937","article-title":"Component-Based Design by Solving Language Equations","volume":"103","author":"Villa","year":"2015","journal-title":"Proceedings of the IEEE"},{"key":"villa12","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68759-9","volume-title":"The Unknown Component Problem: Theory and Applications","author":"Villa","year":"2012"},{"key":"fujita-aspdac2007","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1109\/ASPDAC.2007.357999","article-title":"Protocol Transducer Synthesis using Divide and Conquer approach","volume-title":"Design Automation Conference, 2007. ASP-DAC '07. Asia and South Pacific","author":"Watanabe","year":"2007"},{"key":"fsmeq1-iwls2004","first-page":"409","article-title":"Composition Operators in Language Equations","volume-title":"International Workshop on Logic and Synthesis","author":"Yevtushenko","year":"2004"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2020,9,25]],"date-time":"2020-09-25T00:32:14Z","timestamp":1600993934000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2009.10886v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,20]]},"references-count":42,"URL":"https:\/\/doi.org\/10.4204\/eptcs.326.14","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,20]]}}}