{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:50:32Z","timestamp":1763459432017,"version":"3.45.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,1,2]],"date-time":"2018-01-02T00:00:00Z","timestamp":1514851200000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"U.S.National Science Foundation","doi-asserted-by":"publisher","award":["#1329759 and #1139138"],"award-info":[{"award-number":["#1329759 and #1139138"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002341","name":"Academy of Finland","doi-asserted-by":"crossref","award":["#139402, #265939, and #277522"],"award-info":[{"award-number":["#139402, #265939, and #277522"]}],"id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"crossref"}]},{"name":"UCBerkeley's iCyPhy Research Center"},{"name":"SARANA project in the SAFIR 2014 programme"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2017,5,31]]},"abstract":"<jats:p>We study the need for complex circular assume-guarantee (AG) rules in formalisms that already provide the simple precongruence rule. We first investigate the question for two popular formalisms: Labeled Transition Systems (LTSs) with weak simulation and Interface Automata (IA) with alternating simulation. We observe that, in LTSs, complex circular AG rules cannot always be avoided, but, in the IA world, the simple precongruence rule is all we need. Based on these findings, we introduce modal IA with cut states, a novel formalism that not only generalizes IA and LTSs but also allows for compositional reasoning without complex AG rules.<\/jats:p>","DOI":"10.1145\/3012280","type":"journal-article","created":{"date-parts":[[2017,1,3]],"date-time":"2017-01-03T08:18:41Z","timestamp":1483431521000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["When Do We Not Need Complex Assume-Guarantee Rules?"],"prefix":"10.1145","volume":"16","author":[{"given":"Antti","family":"Siirtola","sequence":"first","affiliation":[{"name":"University of Oulu, Finland"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[{"name":"Aalto University and UC Berkeley, Berkeley, CA"}]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[{"name":"Aalto University and HIIT, Aalto, Finland"}]}],"member":"320","published-online":{"date-parts":[[2017,1,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"volume-title":"Principles of Model Checking","author":"Baier C.","key":"e_1_2_1_3_1","unstructured":"C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_15"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04298-5_15"},{"key":"e_1_2_1_6_1","volume-title":"A","author":"Chilton Chris","year":"2014","unstructured":"Chris Chilton, Bengt Jonsson, and Marta Kwiatkowska. 2014. Compositional assume-guarantee reasoning for input\/output component theories. Sci. Comput. Program. 91, A (2014), 115--137."},{"key":"e_1_2_1_7_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45449-7_11"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-3532-2_3"},{"key":"e_1_2_1_12_1","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"de Roever Willem-Paul","year":"2001","unstructured":"Willem-Paul de Roever, Frank S. de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers. 2001. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_10"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2004.1428676"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028765"},{"key":"e_1_2_1_17_1","volume-title":"Article 4","author":"L\u00fcttgen Gerald","year":"2013","unstructured":"Gerald L\u00fcttgen and Walter Vogler. 2013. Modal interface automata. Logical Methods in Computer Science 9, 3, Article 4 (2013), 28 pages."},{"key":"e_1_2_1_18_1","first-page":"219","article-title":"An introduction to input\/output automata","volume":"2","author":"Lynch Nancy A.","year":"1989","unstructured":"Nancy A. Lynch and Mark R. Tuttle. 1989. An introduction to input\/output automata. CWI Quarterly 2 (1989), 219--246.","journal-title":"CWI Quarterly"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028738"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1740582.1740584"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656045.2656068"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2362088.2362095"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0"},{"volume-title":"Compositionality: The Significant Difference, Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli (Eds.). LNCS","author":"Shankar Natarajan","key":"e_1_2_1_27_1","unstructured":"Natarajan Shankar. 1998. Lazy compositional verification. In Compositionality: The Significant Difference, Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli (Eds.). LNCS, Vol. 1536. Springer, 541--564."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2014.26"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2015.19"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985342.1985345"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45510-8_3"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3012280","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3012280","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3012280","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:45:55Z","timestamp":1763459155000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3012280"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,2]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,5,31]]}},"alternative-id":["10.1145\/3012280"],"URL":"https:\/\/doi.org\/10.1145\/3012280","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2017,1,2]]},"assertion":[{"value":"2016-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-10-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-01-02","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}