{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T04:31:37Z","timestamp":1785213097491,"version":"3.55.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":21,"publisher":"Springer-Verlag","isbn-type":[{"value":"3540544771","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0023737","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T06:01:03Z","timestamp":1132380063000},"page":"233-242","source":"Crossref","is-referenced-by-count":56,"title":["Memory efficient algorithms for the verification of temporal properties"],"prefix":"10.1007","author":[{"given":"C.","family":"Courcoubetis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Wolper","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M.","family":"Yannakakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2","key":"25_CR1","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1145\/78942.78948","volume":"12","author":"S. Aggarwal","year":"1990","unstructured":"S. Aggarwal, C. Courcoubetis, and P. Wolper. Adding liveness properties to coupled finite-state machines. ACM Transactions on Programming Languages and Systems, 12(2):303\u2013339, 1990.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"25_CR2","unstructured":"Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley, Reading, 1974."},{"key":"25_CR3","unstructured":"Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. Data Structures and Algorithms. Addison Wesley, Reading, 1982."},{"issue":"2","key":"25_CR4","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, January 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and O. Gr\u00fcmberg. Avoiding the state explosion problem in temporal logic model-checking algorithms. In Proc. 6th ACM Symposium on Principles of Distributed Computing, pages 294\u2013303, Vancouver, British Columbia, August 1987.","DOI":"10.1145\/41840.41865"},{"key":"25_CR6","unstructured":"R. Grotz, C. Jard, and C. Lassudrie. Attacking a complex distributed systems from different sides: an experience with complementary validation tools. In Proc. 4th Work. Protocol Specification, Testing, and Verification, pages 3\u201317. North-Holland, 1984."},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"B.T. Hailpern. Tools for verifying network protocols. In K. Apt, editor, Logic and Models of Concurrent Systems, NATO ISI Series, pages 57\u201376. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_3"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"G. Holzmann. An improved protocol reachability analysis technique. Software Practice and Experience, pages 137\u2013161, February 1988.","DOI":"10.1002\/spe.4380180203"},{"key":"25_CR9","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-52148-8_16","volume":"407","author":"C. Jard","year":"1989","unstructured":"C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, volume 407, pages 189\u2013196, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag.","journal-title":"Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble"},{"key":"25_CR10","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/S0065-2458(08)60533-1","volume":"29","author":"M.T. Liu","year":"1989","unstructured":"M.T. Liu. Protocol engineering. Advances in Computing, 29:79\u2013195, 1989.","journal-title":"Advances in Computing"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97\u2013107, New Orleans, January 1985.","DOI":"10.1145\/318593.318622"},{"key":"25_CR12","first-page":"337","volume":"137","author":"J.P. Quielle","year":"1981","unstructured":"J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in cesar. In Proc. 5th Int'l Symp. on Programming, volume 137, pages 337\u2013351. Springer-Verlag, Lecture Notes in Computer Science, 1981.","journal-title":"Proc. 5th Int'l Symp. on Programming"},{"key":"25_CR13","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1146\/annurev.cs.02.060187.001451","volume":"2","author":"H. Rudin","year":"1987","unstructured":"H. Rudin. Network protocols and tools to help produce them. Annual Review of Computer Science, 2:291\u2013316, 1987.","journal-title":"Annual Review of Computer Science"},{"key":"25_CR14","doi-asserted-by":"crossref","first-page":"630","DOI":"10.1109\/TC.1982.1676060","volume":"C-312","author":"H. Rudin","year":"1982","unstructured":"H. Rudin and C.H. West. A validation technique for tightly-coupled protocols. IEEE Transactions on Computers, C-312:630\u2013636, 1982.","journal-title":"IEEE Transactions on Computers"},{"key":"25_CR15","unstructured":"C.A. Sunshine. Experience with automated protocol verification. In Proceedings of the International Conference on Communication, pages 1306\u20131310, 1983."},{"key":"25_CR16","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-51803-7_27","volume":"398","author":"M. Vardi","year":"1989","unstructured":"M. Vardi. Unified verification theory. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 202\u2013212. Lecture Notes in Computer Science, Springer-Verlag, 1989.","journal-title":"Proc. Temporal Logic in Specification"},{"key":"25_CR17","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. Symp. on Logic in Computer Science, pages 322\u2013331, Cambridge, june 1986."},{"key":"25_CR18","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computation paths. IBM Research Report RJ6209, 1988."},{"key":"25_CR19","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1147\/rd.224.0393","volume":"22","author":"C.H. West","year":"1978","unstructured":"C.H. West. Generalized technique for communication protocol validation. IBM J. of Res. and Devel., 22:393\u2013404, 1978.","journal-title":"IBM J. of Res. and Devel."},{"key":"25_CR20","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-51803-7_23","volume":"398","author":"P. Wolper","year":"1989","unstructured":"P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 75\u2013123. Lecture Notes in Computer Science, Springer-Verlag, 1989.","journal-title":"Proc. Temporal Logic in Specification"},{"key":"25_CR21","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1147\/rd.221.0060","volume":"22","author":"C.H. West","year":"1978","unstructured":"C.H. West and P. Zafiropulo. Automated validation of a communication protocol: the ccitt x.21 recommendation. IBM Journal of Research and Development, 22:60\u201371, 1978.","journal-title":"IBM Journal of Research and Development"}],"container-title":["Lecture Notes in Computer Science","Computer-Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0023737.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:50:22Z","timestamp":1607550622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0023737"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540544771"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0023737","relation":{},"subject":[]}}