{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T16:30:30Z","timestamp":1774801830230,"version":"3.50.1"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0225610 (ITR)0720882 (CSR-EHS: PRET)0931843 (ActionWebs)"],"award-info":[{"award-number":["CCR-0225610 (ITR)0720882 (CSR-EHS: PRET)0931843 (ActionWebs)"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["MURI FA9550-06-0312AFTRUST FA9550-06-1-0244"],"award-info":[{"award-number":["MURI FA9550-06-0312AFTRUST FA9550-06-1-0244"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000183","name":"Army Research Office","doi-asserted-by":"publisher","award":["ARO W911NF-07-2-0019"],"award-info":[{"award-number":["ARO W911NF-07-2-0019"]}],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11402-N23 (RiSE)"],"award-info":[{"award-number":["S11402-N23 (RiSE)"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2011,7]]},"abstract":"<jats:p>Compositional theories are crucial when designing large and complex systems from smaller components. In this work we propose such a theory for synchronous concurrent systems. Our approach follows so-called interface theories, which use game-theoretic interpretations of composition and refinement. These are appropriate for systems with distinct inputs and outputs, and explicit conditions on inputs that must be enforced during composition. Our interfaces model systems that execute in an infinite sequence of synchronous rounds. At each round, a contract must be satisfied. The contract is simply a relation specifying the set of valid input\/output pairs. Interfaces can be composed by parallel, serial or feedback composition. A refinement relation between interfaces is defined, and shown to have two main properties: (1) it is preserved by composition, and (2) it is equivalent to substitutability, namely, the ability to replace an interface by another one in any context. Shared refinement and abstraction operators, corresponding to greatest lower and least upper bounds with respect to refinement, are also defined. Input-complete interfaces, that impose no restrictions on inputs, and deterministic interfaces, that produce a unique output for any legal input, are discussed as special cases, and an interesting duality between the two classes is exposed. A number of illustrative examples are provided, as well as algorithms to compute compositions, check refinement, and so on, for finite-state interfaces.<\/jats:p>","DOI":"10.1145\/1985342.1985345","type":"journal-article","created":{"date-parts":[[2011,7,21]],"date-time":"2011-07-21T13:27:09Z","timestamp":1311254829000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":55,"title":["A Theory of Synchronous Relational Interfaces"],"prefix":"10.1145","volume":"33","author":[{"given":"Stavros","family":"Tripakis","sequence":"first","affiliation":[{"name":"University of California, Berkeley"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ben","family":"Lickly","sequence":"additional","affiliation":[{"name":"University of California, Berkeley"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[{"name":"Institute of Science and Technology, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edward A.","family":"Lee","sequence":"additional","affiliation":[{"name":"University of California, Berkeley"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,7]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR\u201998)","volume":"1466","author":"Alur R.","unstructured":"Alur , R. , Henzinger , T. , Kupferman , O. , and Vardi , M . 1998. Alternating refinement relations . In Proceedings of the International Conference on Concurrency Theory (CONCUR\u201998) . Lecture Notes in Computer Science , vol. 1466 . Springer. Alur, R., Henzinger, T., Kupferman, O., and Vardi, M. 1998. Alternating refinement relations. In Proceedings of the International Conference on Concurrency Theory (CONCUR\u201998). Lecture Notes in Computer Science, vol. 1466. Springer."},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Back R.-J. and Wright J. 1998. Refinement Calculus. Springer. Back R.-J. and Wright J. 1998. Refinement Calculus. Springer.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800057.808665"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"e_1_2_2_9_1","unstructured":"Berry G. 1999. The constructive semantics of Pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org\/. Berry G. 1999. The constructive semantics of Pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org\/."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/268999.269004"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Broy M. and St\u00f8len K. 2001. Specification and Development of Interactive Systems: Focus on Streams Interfaces and Refinement. Springer. Broy M. and St\u00f8len K. 2001. Specification and Development of Interactive Systems: Focus on Streams Interfaces and Refinement. Springer.","DOI":"10.1007\/978-1-4613-0091-5"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734413"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/196092.195325"},{"key":"e_1_2_2_15_1","first-page":"192","article-title":"Game models for open systems. In Verification: Theory and Practice, N. Dershowitz Ed","volume":"2772","author":"de Alfaro L.","year":"2004","unstructured":"de Alfaro , L. 2004 . Game models for open systems. In Verification: Theory and Practice, N. Dershowitz Ed ., Lecture Notes in Computer Science Series , vol. 2772 , Spring er, 192 -- 213 . de Alfaro, L. 2004. Game models for open systems. In Verification: Theory and Practice, N. Dershowitz Ed., Lecture Notes in Computer Science Series, vol. 2772, Springer, 192--213.","journal-title":"Lecture Notes in Computer Science Series"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the International Workshop on Embedded Software (EMSOFT\u201901)","volume":"2211","author":"de Alfaro L.","unstructured":"de Alfaro , L. and Henzinger , T . 2001b. Interface theories for component-based design . In Proceedings of the International Workshop on Embedded Software (EMSOFT\u201901) . Lecture Notes in Computer Science , vol. 2211 , Springer. de Alfaro, L. and Henzinger, T. 2001b. Interface theories for component-based design. In Proceedings of the International Workshop on Embedded Software (EMSOFT\u201901). Lecture Notes in Computer Science, vol. 2211, Springer."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-005-7006-5"},{"key":"e_1_2_2_19_1","volume-title":"Proceedings of the 18th International Conference on Software Engineering (ICSE\u201996)","author":"Dhara K.","unstructured":"Dhara , K. and Leavens , G . 1996. Forcing behavioral subtyping through specification inheritance . In Proceedings of the 18th International Conference on Software Engineering (ICSE\u201996) . IEEE Computer Society, 258--267. Dhara, K. and Leavens, G. 1996. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 18th International Conference on Software Engineering (ICSE\u201996). IEEE Computer Society, 258--267."},{"key":"e_1_2_2_20_1","volume-title":"Notes on structured programming","author":"Dijkstra E.","unstructured":"Dijkstra , E. 1972. Notes on structured programming . In Structured Programming, O. Dahl, E. Dijkstra, and C. Hoare Eds., Academic Press , London, UK , 1--82. Dijkstra, E. 1972. Notes on structured programming. In Structured Programming, O. Dahl, E. Dijkstra, and C. Hoare Eds., Academic Press, London, UK, 1--82."},{"key":"e_1_2_2_21_1","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits","author":"Dill D.","unstructured":"Dill , D. 1987. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits . MIT Press, Cambridge , MA. Dill, D. 1987. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, Cambridge, MA."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450070"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.2.317"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/151155"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3532.315103"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2007.364"},{"key":"e_1_2_2_29_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification. Lecture Notes in Computer Science","volume":"1427","author":"Henzinger T.","unstructured":"Henzinger , T. , Qadeer , S. , and Rajamani , S . 1998. You assume, we guarantee: Methodology and case studies . In Proceedings of the International Conference on Computer-Aided Verification. Lecture Notes in Computer Science , vol. 1427 , Springer-Verlag. Henzinger, T., Qadeer, S., and Rajamani, S. 1998. You assume, we guarantee: Methodology and case studies. In Proceedings of the International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1427, Springer-Verlag."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_31_1","volume-title":"Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages. Prentice-Hall, Inc., Upper Saddle River, NJ, 141--155","author":"Hoare C. A. R.","year":"1985","unstructured":"Hoare , C. A. R. 1985 . Programs are predicates . In Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages. Prentice-Hall, Inc., Upper Saddle River, NJ, 141--155 . Hoare, C. A. R. 1985. Programs are predicates. In Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages. Prentice-Hall, Inc., Upper Saddle River, NJ, 141--155."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/174662.174665"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80932-0"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/185087.185117"},{"key":"e_1_2_2_36_1","unstructured":"Leavens G. and Cheon Y. 2006. Design by contract with JML. http:\/\/www.jmlspecs.org\/jmldbc.pdf. Leavens G. and Cheon Y. 2006. Design by contract with JML. http:\/\/www.jmlspecs.org\/jmldbc.pdf."},{"key":"e_1_2_2_37_1","volume-title":"EECS Department","author":"Lee E.","unstructured":"Lee , E. 2008. Cyber physical systems: Design challenges. Tech. rep. UCBIEECS-2008-8 , EECS Department , University of California , Berkeley. Lee, E. 2008. Cyber physical systems: Design challenges. Tech. rep. UCBIEECS-2008-8, EECS Department, University of California, Berkeley."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.736561"},{"key":"e_1_2_2_39_1","volume-title":"Proceedings of the International Workshop on Embedded Software (EMSOFT\u201901)","author":"Lee E.","unstructured":"Lee , E. and Xiong , Y . 2001. System-level types for component-based design . In Proceedings of the International Workshop on Embedded Software (EMSOFT\u201901) . Springer, 237--253. Lee, E. and Xiong, Y. 2001. System-level types for component-based design. In Proceedings of the International Workshop on Embedded Software (EMSOFT\u201901). Springer, 237--253."},{"key":"e_1_2_2_40_1","series-title":"Lecture Notes in Computer Science Series","volume-title":"Abstract Software Specifications","author":"Liskov B.","unstructured":"Liskov , B. 1979. Modular program construction using abstractions . In Abstract Software Specifications . Lecture Notes in Computer Science Series , vol. 86 ., Springer , 354--389. Liskov, B. 1979. Modular program construction using abstractions. In Abstract Software Specifications. Lecture Notes in Computer Science Series, vol. 86., Springer, 354--389."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403736"},{"key":"e_1_2_2_43_1","first-page":"219","article-title":"An introduction to input\/output automata","volume":"2","author":"Lynch N.","year":"1989","unstructured":"Lynch , N. and Tuttle , M. 1989 . An introduction to input\/output automata . CWI Quart. 2 , 219 -- 246 . Lynch, N. and Tuttle, M. 1989. An introduction to input\/output automata. CWI Quart. 2, 219--246.","journal-title":"CWI Quart."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.293952"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733598"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646372"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/167962.167976"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/358161.358168"},{"key":"e_1_2_2_52_1","volume-title":"Types and Programming Languages","author":"Pierce B.","unstructured":"Pierce , B. 2002. Types and Programming Languages . MIT Press . Pierce, B. 2002. Types and Programming Languages. MIT Press."},{"key":"e_1_2_2_53_1","doi-asserted-by":"crossref","unstructured":"Raclet J.-B. Badouel E. Benveniste A. Caillaud B. Legay A. and Passerone R. 2010. A modal interface theory for component-based design. http:\/\/www.irisa.fr\/distribcom\/benveniste\/pub\/Fundamenta2010.htm1. Raclet J.-B. Badouel E. Benveniste A. Caillaud B. Legay A. and Passerone R. 2010. A modal interface theory for component-based design. http:\/\/www.irisa.fr\/distribcom\/benveniste\/pub\/Fundamenta2010.htm1.","DOI":"10.3233\/FI-2011-416"},{"key":"e_1_2_2_54_1","unstructured":"Ravindran K. and Yang G. 2010. Personal communication. Ravindran K. and Yang G. 2010. Personal communication."},{"key":"e_1_2_2_55_1","volume-title":"Proceedings of the 2nd NASA Formal Methods Symposium (NFM\u201910)","author":"Roy P.","unstructured":"Roy , P. and Shankar , N . 2010. An expressive type system for Simulink . In Proceedings of the 2nd NASA Formal Methods Symposium (NFM\u201910) . 149--160. Roy, P. and Shankar, N. 2010. An expressive type system for Simulink. In Proceedings of the 2nd NASA Formal Methods Symposium (NFM\u201910). 149--160."},{"key":"e_1_2_2_56_1","volume-title":"Compositionality: The Significant Difference","author":"Shankar N.","unstructured":"Shankar , N. 1998. Lazy compositional verification . In Compositionality: The Significant Difference . Springer , 541--564. Shankar, N. 1998. Lazy compositional verification. In Compositionality: The Significant Difference. Springer, 541--564."},{"key":"e_1_2_2_57_1","volume-title":"The Z Notation: A Reference Manual","author":"Spivey J. M.","unstructured":"Spivey , J. M. 1989. The Z Notation: A Reference Manual . Prentice-Hall, Inc. , Upper Saddle River, NJ. Spivey, J. M. 1989. The Z Notation: A Reference Manual. Prentice-Hall, Inc., Upper Saddle River, NJ."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/646823.706907"},{"key":"e_1_2_2_59_1","volume-title":"Mathematical Logic","author":"Tourlakis G.","unstructured":"Tourlakis , G. 2008. Mathematical Logic . Wiley . Tourlakis, G. 2008. Mathematical Logic. Wiley."},{"key":"e_1_2_2_60_1","doi-asserted-by":"crossref","unstructured":"Tripakis S. Lickly B. Henzinger T. and Lee E. 2009a. On relational interfaces. Tech. rep. UCBIEECS-2009-60 EECS Department University of California Berkeley. Tripakis S. Lickly B. Henzinger T. and Lee E. 2009a. On relational interfaces. Tech. rep. UCBIEECS-2009-60 EECS Department University of California Berkeley.","DOI":"10.1145\/1629335.1629346"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629335.1629346"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/362575.362577"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347382"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1985342.1985345","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1985342.1985345","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:59:55Z","timestamp":1750244395000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1985342.1985345"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":63,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,7]]}},"alternative-id":["10.1145\/1985342.1985345"],"URL":"https:\/\/doi.org\/10.1145\/1985342.1985345","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7]]},"assertion":[{"value":"2010-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}