{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:13:44Z","timestamp":1725664424793},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540592938"},{"type":"electronic","value":"9783540492337"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59293-8_200","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:11:42Z","timestamp":1330276302000},"page":"262-276","source":"Crossref","is-referenced-by-count":8,"title":["Assumption\/guarantee specifications in linear-time temporal logic (extended abstract)"],"prefix":"10.1007","author":[{"given":"Bengt","family":"Jonsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yih-Kuen","family":"Tsay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82:253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"17_CR2","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73\u2013132, January 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. Conjoining specifications. Technical Report 118, SRC DEC, 1993. Part of the paper appears in PODC '94 as \u201cOpen Systems in TLA\u201d.","DOI":"10.1145\/197917.197960"},{"issue":"1","key":"17_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(93)90151-I","volume":"114","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and G.D. Plotkin. A logical view of composition. Theoretical Computer Science, 114(1):3\u201330, June 1993.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"17_CR5","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"24","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters, 24(4):181\u2013185, October 1985.","journal-title":"Information Processing Letters"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"H. Barringer and R. Kuiper. Hierarchical development of concurrent systems in a temporal logic framework. In Seminar on Concurrency, LNCS 197, pages 35\u201361. Springer-Verlag, 1984.","DOI":"10.1007\/3-540-15670-4_2"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"P. Collette. Application of the composition principle to Unity-like specifications. In TAPSOFT '93, LNCS 668, pages 230\u2013242. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56610-4_67"},{"key":"17_CR8","unstructured":"P. Collette. Design of Compositional Proof Systems Based on Assumption-Guarantee Specifications \u2014 Application to UNITY. PhD thesis, Universit\u00e9 Catholique de Louvain, June 1994."},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"P. Gr\u00f8nning, T.Q. Nielsen, and H.H. L\u00f8vengreen. Refinement and composition of transition-based rely-guarantee specifications with auxiliary variables. In FST&TCS, LNCS 472, pages 332\u2013348. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-53487-3_55"},{"issue":"4","key":"17_CR10","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596\u2013619, October 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"B. Jonsson and Y.-K. Tsay. Assumption\/guarantee specifications in linear-time temporal logic. Technical Report DoCS 95\/58, Department of Computer Systems, Uppsala University, January 1995.","DOI":"10.1007\/3-540-59293-8_200"},{"key":"17_CR12","first-page":"657","volume-title":"Information Processing 83","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. What good is temporal logic? In R.E.A. Mason, editor, Information Processing 83, pages 657\u2013668. IFIP, North-Holland, 1983."},{"issue":"3","key":"17_CR13","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"4","key":"17_CR15","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(4):417\u2013426, July 1981.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"17_CR16","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1982","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1982.","journal-title":"Theoretical Computer Science"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"A. Pnueli. System specification and refinement in temporal logic. In FST&TCS, LNCS 652, pages 1\u201338. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-56287-7_92"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Q. Xu, A. Cau, and P. Collette. On unifying assumption-commitment style proof rules for concurrency. In CONCUR '94, LNCS 836, pages 267\u2013282. Springer-Verlag, 1994.","DOI":"10.1007\/978-3-540-48654-1_22"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '95: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59293-8_200.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:26:31Z","timestamp":1605648391000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59293-8_200"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540592938","9783540492337"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-59293-8_200","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}