{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:41:25Z","timestamp":1754484085492},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540551799"},{"type":"electronic","value":"9783540467632"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55179-4_7","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T04:53:23Z","timestamp":1330232003000},"page":"59-69","source":"Crossref","is-referenced-by-count":5,"title":["Automatic temporal verification of buffer systems"],"prefix":"10.1007","author":[{"given":"A. Prasad","family":"Sistla","sequence":"first","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"7_CR1","unstructured":"Y. Afek, H. Attyia, A. Fekete, M. Fischer, N. Lynch, Y. Mansour, D.-W. Wang, and L. Zuck. Reliable communication using unreliable channel, to appear in JACM."},{"key":"7_CR2","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"K. A. Bartlett","year":"1969","unstructured":"K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communication of the ACM, 12:260\u2013261, 1969.","journal-title":"Communication of the ACM"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. Transactions on Programming Languages and Systems, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"7_CR4","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design: A Fundation. (A draft), 1986."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and C. L. Lei. Modalities for model checking: Branching time strikes back. In Proc. 12th ACM Symp. on Principles of Programming Languages, pages 84\u201396, 1985.","DOI":"10.1145\/318593.318620"},{"issue":"2","key":"7_CR6","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM TOPLAS, 5(2):190\u2013222, 1983.","journal-title":"ACM TOPLAS"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specifications. In Proc. 12th ACM Symp. on Principles of Programming Languages, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 137\u2013151, 1987.","DOI":"10.1145\/41840.41852"},{"issue":"3","key":"7_CR9","first-page":"219","volume":"2","author":"N. A. Lynch","year":"1989","unstructured":"N.A. Lynch and M. R. Tuttle. An introduction to input\/output automata. CWI Quarterly, 2(3):219\u2013246, 1989.","journal-title":"CWI Quarterly"},{"issue":"3","key":"7_CR10","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. TOPLAS, 4(3):455\u2013495, 1982.","journal-title":"TOPLAS"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The Temporal Logic of programs. In Proc. 18th IEEE Symp. on Foundation of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1\/2","key":"7_CR12","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1016\/S0019-9958(84)80043-1","volume":"63","author":"A. P. Sistla","year":"1984","unstructured":"A. P. Sistla, E. M. Clarke, N. Francez, and A. R. Meyer. Can message buffers be axiomatized in linear temporal logic? Information and Control, 63(1\/2):88\u2013112, 1984.","journal-title":"Information and Control"},{"key":"7_CR13","unstructured":"A. P. Sistla and L. D. Zuck. Reasoning in a restricted temporal logic. submitted for publication, parts appeared in [SZ87], 1990."},{"key":"7_CR14","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proc. 1st IEEE Symp. on Logics in Computer Science, 1986."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55179-4_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:58:04Z","timestamp":1605628684000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55179-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551799","9783540467632"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-55179-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}