{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:24:37Z","timestamp":1770337477781,"version":"3.49.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[1992,10,1]],"date-time":"1992-10-01T00:00:00Z","timestamp":717897600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1992,10]]},"DOI":"10.1007\/bf00121128","type":"journal-article","created":{"date-parts":[[2004,10,31]],"date-time":"2004-10-31T04:38:59Z","timestamp":1099197539000},"page":"275-288","source":"Crossref","is-referenced-by-count":271,"title":["Memory-efficient algorithms for the verification of temporal properties"],"prefix":"10.1007","volume":"1","author":[{"given":"C.","family":"Courcoubetis","sequence":"first","affiliation":[]},{"given":"M.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"P.","family":"Wolper","sequence":"additional","affiliation":[]},{"given":"M.","family":"Yannakakis","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","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 Journal of Research and Development, 22:393?404 (1978).","journal-title":"IBM Journal of Research and Development"},{"key":"CR2","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?195 (1989).","journal-title":"Advances in Computing"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"191","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:191?316 (1987).","journal-title":"Annual Review of Computer Science"},{"key":"CR4","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?71 (1978).","journal-title":"IBM Journal of Research and Development"},{"key":"CR5","doi-asserted-by":"crossref","first-page":"630","DOI":"10.1109\/TC.1982.1676060","volume":"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?636 (1982).","journal-title":"IEEE Transactions on Computers"},{"key":"CR6","unstructured":"C.A. Sunshine. Experience with automated protocol verification. In Proceedings of the International Conference on Communication, Boston, June 1983, pp. 1306?1310."},{"key":"CR7","series-title":"NATO ISI Series","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-3-642-82453-1_3","volume-title":"Logic and Models of Concurrent Systems","author":"B.T. Hailpern","year":"1985","unstructured":"B.T. Hailpern. Tools for verifying network protocols. In Logic and Models of Concurrent Systems, NATO ISI Series, K. Apt (ed.). Springer-Verlag, New York, 1985, pp. 57?76."},{"key":"CR8","first-page":"3","volume-title":"Proceedings of the 4th Workshop of Protocol Specification, Testing, and Verification","author":"R. Grotz","year":"1984","unstructured":"R. Grotz, C. Jard, and C. Lassudrie. Attacking a complex distributed systems for different sides: an experience with complementary validation tools. In Proceedings of the 4th Workshop of Protocol Specification, Testing, and Verification. North-Holland, Amsterdam, 1984, 3?17."},{"issue":"2","key":"CR9","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?263 (January 1986).","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and O. Gr\u00fcmberg. Avoiding the state explosion problem in temporal logic modelchecking algorithms. In Proceedings of the 6th ACM Symposium on Principles of Distributed Computing. Vancouver, British Columbia, August 1987, pp. 294?303.","DOI":"10.1145\/41840.41865"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pneuli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages. New Orleans, January 1985, pp. 97?107.","DOI":"10.1145\/318593.318622"},{"key":"CR12","series-title":"Lecture Notes in Computer Science","first-page":"337","volume-title":"Proceedings of the 5th International Symposium on Programming","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. In Proceedings of the 5th International Symposium on Programming, volume 137, in Lecture Notes in Computer Science. Springer Verlag, New York, 1981, pp. 337?351."},{"key":"CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-51803-7_27","volume-title":"Proceedings of Temporal Logic in Specification","author":"M. Vardi","year":"1989","unstructured":"M. Vardi. Unified verification theory. In Proceedings of Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pneuli (ed.), volume 398 in Lecture Notes in Computer Science. Springer-Verlag, New York, 1989, pp. 202?212."},{"key":"CR14","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of a Symposium on Logic in Computer Science, Cambridge, June 1986, pp. 322?331."},{"key":"CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-51803-7_23","volume-title":"Proceedings of Temporal Logic in Specification","author":"P. Wolper","year":"1989","unstructured":"P. Wolper. On the relation of programs and computations to models of temporal logic. In Proceedings of Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli (eds.), volume 398 in Lecture Notes in Computer Science. Springer-Verlag, New York, 1989, pp. 75?123."},{"issue":"no. 2","key":"CR16","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1002\/spe.4380180203","volume":"18","author":"G. Holzmann","year":"1988","unstructured":"G. Holzmann. An improved protocol reachability analysis technique. Software Practice and Experience, vol. 18, no. 2, 137?161 (February 1988).","journal-title":"Software Practice and Experience"},{"key":"CR17","series-title":"Lecture Notes in Computer Science","first-page":"189","volume-title":"Automatic Verification Methods for Finite State Systems, Proceedings of a International Workshop, Grenoble","author":"C. Jard","year":"1989","unstructured":"C. Jard and T. J\u00e9ron. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proceedings of a International Workshop, Grenoble, volume 407 in Lecture Notes in Computer Science, Grenoble, June 1989. Springer-Verlag, New York, 1989, pp. 189?96."},{"key":"CR18","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computation paths. IBM Research Report RJ6209, 1988."},{"key":"CR19","volume-title":"From Modal Logic to Deductive Databases: Introducing a Logic Based Approach to Artificial Intelligence","author":"Andr\u00e9 Thayse","year":"1989","unstructured":"Andr\u00e9 Thayse and et al. From Modal Logic to Deductive Databases: Introducing a Logic Based Approach to Artificial Intelligence, Wiley, New York, 1989."},{"key":"CR20","volume-title":"The Design and Analysis of Computer Algorithms","author":"Alfred V. Aho","year":"1974","unstructured":"Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley, Reading, MA, 1974."},{"issue":"2","key":"CR21","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?339 (1990).","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR22","volume-title":"Data Structures and Algorithms","author":"Alfred V. Aho","year":"1982","unstructured":"Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. Data Structures and Algorithms. Addison Wesley, Reading, MA, 1982."},{"issue":"12","key":"CR23","doi-asserted-by":"crossref","first-page":"2413","DOI":"10.1002\/j.1538-7305.1985.tb00010.x","volume":"64","author":"G.J. Holzmann","year":"1985","unstructured":"G.J. Holzmann. Tracing protocols. AT&T Technical Journal, 64(12):2413?2434 (1985).","journal-title":"AT&T Technical Journal"},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"C. Jard and T. Jeron. Bounded-memory algorithms for verification on the fly. In Proceedings of a Workshop on Computer Aided Verification, Aalborg, July 1991.","DOI":"10.1007\/3-540-55179-4_19"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"P. Godefroid, G.J. Holzmann, and D. Pirottin. State space caching revisited. In Proceedings of the 4th Workshop on Computer Aided Verification, Montreal, June 1992.","DOI":"10.1007\/3-540-56496-9_15"},{"key":"CR26","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, Englewood Cliffs, NJ, 1991."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00121128.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00121128\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00121128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T16:26:46Z","timestamp":1585931206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00121128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,10]]},"references-count":26,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[1992,10]]}},"alternative-id":["BF00121128"],"URL":"https:\/\/doi.org\/10.1007\/bf00121128","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,10]]}}}