{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T08:16:26Z","timestamp":1775636186326,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540662020","type":"print"},{"value":"9783540486831","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_17","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"172-183","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":75,"title":["Model Checking of Safety Properties"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"MosheY.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F.B. Schneider. Defining liveness. Information processing letters, 21:181\u2013185, 1985.","journal-title":"Information processing letters"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"B. Alpern and F.B. Schneider. Recognizing safety and liveness. Distributed computing, 2:117\u2013126, 1987.","journal-title":"Distributed computing"},{"issue":"2","key":"17_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"[. J.R. Burch","year":"1992","unstructured":"[BCM+92]_ J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"17_CR4","series-title":"Technical Report","volume-title":"Proof-checking, theorem-proving and program verification","author":"R.S. Boyer","year":"1983","unstructured":"R.S. Boyer and J.S. Moore. Proof-checking, theorem-proving and program verification. Technical Report 35, Institute for Computing Science and ComputerApplications, University of Texas at Austin, January 1983."},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc.Workshop on Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc.Workshop on Logic of Programs, LNCS 131, pp. 52\u201371, 1981."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"W. Canfield, E.A. Emerson, and A. Saha. Checking formal specifications under simulation. In Proc. International Conference on Computer Design, pp. 455\u2013460, 1997.","DOI":"10.1109\/ICCD.1997.628908"},{"issue":"1","key":"17_CR7","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114\u2013133, January 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"E.A. Emerson","year":"1983","unstructured":"E.A. Emerson. Alternative semantics for temporal logics. Theoretical Computer Science, 26:121\u2013130, 1983.","journal-title":"Theoretical Computer Science"},{"key":"17_CR10","unstructured":"N. Francez. Program verification. International Computer Science. Addison-Weflay, 1992."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman & Hall, August 1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"17_CR12","series-title":"Lect Notes Comput Sci","first-page":"332","volume-title":"Proc. 3rd CAV","author":"P. Godefroid","year":"1991","unstructured":"P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proc. 3rd CAV, LNCS 575, pp. 332\u2013342, 1991."},{"key":"17_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-63166-6_27","volume-title":"Proc. 9th CAV","author":"R.H. Hardin","year":"1997","unstructured":"R.H. Hardin, R.P. Kurshan, S.K. Shukla, and M.Y. Vardi. A new heuristic for bad cycle detection using BDDs. In Proc. 9th CAV, LNCS 1254, pp. 268\u2013278, 1997."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"H. Iwashita and T. Nakata. Forward model checking techniques oriented to buggy designs. In Proc. IEEE\/ACM ICCAD, pp. 400\u2013404, 1997.","DOI":"10.1109\/ICCAD.1997.643567"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Weak alternating automata are not that weak. In Proc. 5th ISTCS, pp. 147\u2013158. IEEE Computer Society Press, 1997.","DOI":"10.1109\/ISTCS.1997.595167"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Freedom, weakness, and determinism: from linear-time to branching-time. In Proc. 13th LICS, pp. 81\u201392, June 1998.","DOI":"10.1109\/LICS.1998.705645"},{"key":"17_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Distributed systems-methods and tools for specification","author":"L. Lamport","year":"1985","unstructured":"L. Lamport. Logical foundation. In Distributed systems-methods and tools for specification, LNCS 190, 1985."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th POPL, pp. 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Y. Luo, T. Wongsonegoro, and A. Aziz. Hybrid techniques for fast functional simulation. In Proc. 35th DAC. IEEE Computer Society, 1998.","DOI":"10.1145\/277044.277213"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"[MAB+94]_ Z. Manna, A. Anuchitanukul, N. Bjorner, A. Browne, E. Chang, M. Colon, L. DeAlfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Computer Science, Stanford University, 1994.","DOI":"10.21236\/ADA324036"},{"key":"17_CR21","series-title":"Lect Notes Comput Sci","first-page":"164","volume-title":"Proc. 4th CAV","author":"K. McMillan","year":"1992","unstructured":"K. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. 4th CAV, LNCS 663, pp. 164\u2013174, 1992."},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"A.R. Meyer and M.J. Fischer. Economy of description by automata, grammars, and formal systems. In Proc. 12th IEEE Symp. on Switching and Automata Theory, pp. 188\u2013191, 1971.","DOI":"10.1109\/SWAT.1971.11"},{"key":"17_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, January 1992."},{"key":"17_CR24","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer-Verlag, NewYork, 1995."},{"key":"17_CR25","series-title":"Lect Notes Comput Sci","first-page":"364","volume-title":"Proc. 9th CAV","author":"S. Melzer","year":"1997","unstructured":"S. Melzer and S. Roemer. Deadlock checking using net unfoldings. In Proc. 9th CAV, LNCS 1254, pp. 364\u2013375, 1997."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"A.R. Meyer and L.J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential time. In Proc. 13th IEEE Symp. on Switching and Automata Theory, pp. 125\u2013129, 1972.","DOI":"10.1109\/SWAT.1972.29"},{"key":"17_CR27","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th International Symp. on Programming","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, LNCS 137, pp. 337\u2013351, 1981."},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi. High-density reachability analysis. In Proc. CAD, pp. 154\u2013158, 1995.","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"S. Safra. On the complexity of \u03c9-automata. In Proc. 29th FOCS, pp. 319\u2013327, White Plains, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"17_CR30","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32:733\u2013749, 1985.","journal-title":"Journal ACM"},{"key":"17_CR31","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"A.P. Sistla. Satefy, liveness and fairness in temporal logic. Formal Aspects of Computing, 6:495\u2013511, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"17_CR32","series-title":"Technical report","volume-title":"The PVS proof checker: A reference manual (beta release)","author":"R.E. Shankar","year":"1993","unstructured":"R.E. Shankar, S. Owre, and J.M. Rushby. The PVS proof checker: A reference manual (beta release). Technical report, Computer Science laboratory, SRI International, Menlo Park, California, March 1993."},{"issue":"1","key":"17_CR33","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1006\/inco.1995.1055","volume":"118","author":"H.J. Touati","year":"1995","unstructured":"H.J. Touati, R.K. Brayton, and R. Kurshan. Testing language containment for \u03c9-automata using BDD\u2019s. Information and Computation, 118(1):101\u2013109, April 1995.","journal-title":"Information and Computation"},{"key":"17_CR34","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 5nd CAV","author":"A. Valmari","year":"1993","unstructured":"A. Valmari. On-the-fly verification with stubborn sets. In Proc. 5nd CAV, LNCS 697, 1993."},{"key":"17_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M.Y. Vardi","year":"1996","unstructured":"M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata, LNCS 1043, pp. 238\u2013266, 1996."},{"key":"17_CR36","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st LICS, pp. 322\u2013331, 1986."},{"issue":"1","key":"17_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"},{"key":"17_CR38","unstructured":"P. Wolper. Synthesis of Communicating Processes from Temporal Logic Specifications. PhD thesis, Stanford University, 1982."},{"key":"17_CR39","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/3-540-63166-6_37","volume-title":"Proc 9th CAV","author":"J. Yuan","year":"1997","unstructured":"J. Yuan, J. Shen, J. Abraham, and A. Aziz. On combining formal and informal verification. In Proc 9th CAV, LNCS 1254, pp. 376\u2013387, 1997."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T12:37:22Z","timestamp":1737463042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}