{"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":1775636186885,"version":"3.50.1"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2001,11,1]],"date-time":"2001-11-01T00:00:00Z","timestamp":1004572800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,11,1]],"date-time":"2001-11-01T00:00:00Z","timestamp":1004572800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,11]]},"DOI":"10.1023\/a:1011254632723","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T04:18:21Z","timestamp":1040617101000},"page":"291-314","source":"Crossref","is-referenced-by-count":416,"title":["Model Checking of Safety Properties"],"prefix":"10.1007","volume":"19","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"354074_CR1","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1007\/10722167_40","volume":"1855","author":"Y. Abarbanel","year":"2000","unstructured":"Y. Abarbanel, I. Beer, L. Gluhovsky, S. Keidar, and Y. Wolfstal, \u201cFoCs\u2014Automatic generation of simulation checkers from formal specifications,\u201d in Computer Aided Verification, Proc. 12th Int. Conference, Lecture Notes in Computer Science, Vol. 1855, Springer-Verlag, 2000, pp. 538\u2013542.","journal-title":"Computer Aided Verification, Proc. 12th Int. Conference"},{"key":"354074_CR2","doi-asserted-by":"crossref","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, \u201cDefining liveness,\u201d Information Processing Letters, Vol. 21, pp. 181\u2013185, 1985.","journal-title":"Information Processing Letters"},{"key":"354074_CR3","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"B. Alpern and F.B. Schneider, \u201cRecognizing safety and liveness,\u201d Distributed Computing,Vol. 2, pp. 117\u2013126, 1987.","journal-title":"Distributed Computing"},{"key":"354074_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu, \u201cSymbolic model checking using SAT procedures instead of BDDs,\u201d in Proc. 36th Design Automaion Conference, IEEE Computer Society, 1999, pp. 317\u2013320.","DOI":"10.1145\/309847.309942"},{"issue":"2","key":"354074_CR5","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, \u201cSymbolic model checking: 1020 states and beyond,\u201d Information and Computation, Vol. 98, No. 2, pp. 142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"354074_CR6","doi-asserted-by":"crossref","unstructured":"A. Boujjani, J.-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis, \u201cSafety for branching time,\u201d in Proc. 18th International Colloquium on Automata Languages and Programming, LNCS, Springer-Verlag, 1991, pp. 76\u201392.","DOI":"10.1007\/3-540-54233-7_126"},{"key":"354074_CR7","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, \u201cProof-checking, theorem-proving and program verification,\u201d Technical Report 35, Institute for Computing Science and Computer Applications, University of Texas at Austin, 1983."},{"key":"354074_CR8","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume":"131","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson, \u201cDesign and synthesis of synchronization skeletons using branching time temporal logic,\u201d in Proc. Workshop on Logic of Programs, Lecture Notes in Computer Science, Vol. 131, Springer-Verlag, 1981, pp. 52\u201371.","journal-title":"Proc. Workshop on Logic of Programs"},{"issue":"2","key":"354074_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, \u201cAutomatic verification of finite-state concurrent systems using temporal logic specifications,\u201d ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, pp. 244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"354074_CR10","doi-asserted-by":"crossref","unstructured":"W. Canfield, E.A. Emerson, and A. Saha, \u201cChecking formal specifications under simulation,\u201d in Proc. International Conference on Computer Design, 1997, pp. 455\u2013460.","DOI":"10.1109\/ICCD.1997.628908"},{"issue":"1","key":"354074_CR11","doi-asserted-by":"crossref","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, \u201cAlternation,\u201d Journal of the Association for Computing Machinery, Vol. 28, No. 1, pp. 114\u2013133, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"354074_CR12","doi-asserted-by":"crossref","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, \u201cMemory efficient algorithms for the verification of temporal properties,\u201d Formal Methods in System Design, Vol. 1, pp. 275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"354074_CR13","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"E.A. Emerson","year":"1983","unstructured":"E.A. Emerson, \u201cAlternative semantics for temporal logics,\u201d Theoretical Computer Science, Vol. 26, pp. 121\u2013130, 1983.","journal-title":"Theoretical Computer Science"},{"key":"354074_CR14","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, \u201cTemporal and modal logic,\u201d in Handbook of Theoretical Computer Science, 1990, pp. 997\u20131072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"354074_CR15","volume-title":"Program Verification","author":"N. Francez","year":"1992","unstructured":"N. Francez, Program Verification. International Computer Science, Addison-Weflay, 1992."},{"key":"354074_CR16","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper, \u201cSimple on-the-fly automatic verification of linear temporal logic,\u201d in P. Dembiski and M. Sredniawa (Eds), Protocol Specification, Testing, and Verification, Chapman & Hall, 1995, pp. 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"354074_CR17","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-55179-4_32","volume":"575","author":"P. Godefroid","year":"1991","unstructured":"P. Godefroid and P. Wolper, \u201cUsing partial orders for the efficient verification of deadlock freedom and safety properties,\u201d in Proc. 3rd Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 575, Springer-Verlag, 1991, pp. 332\u2013342.","journal-title":"Proc. 3rd Conference on Computer Aided Verification"},{"key":"354074_CR18","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-63166-6_27","volume":"1254","author":"R.H. Hardin","year":"1997","unstructured":"R.H. Hardin, R.P. Kurshan, S.K. Shukla, and M.Y. Vardi, \u201cA new heuristic for bad cycle detection using BDDs,\u201d in Computer Aided Verification, Proc. 9th Int. Conference, Lecture Notes in Computer Science, Vol. 1254, Springer-Verlag, 1997, pp. 268\u2013278.","journal-title":"Computer Aided Verification, Proc. 9th Int. Conference"},{"key":"354074_CR19","doi-asserted-by":"crossref","unstructured":"H. Iwashita and T. Nakata, \u201cForward model checking techniques oriented to buggy designs,\u201d in Proc. IEEE\/ACM International Conference on Computer Aided Design, 1997, pp. 400\u2013404.","DOI":"10.1109\/ICCAD.1997.643567"},{"key":"354074_CR20","doi-asserted-by":"crossref","unstructured":"N. Klarlund, \u201cMona & Fido: The logic-automaton connection in practice,\u201d in Computer Science Logic, CSL '97, Lecture Notes in Computer Science, 1998.","DOI":"10.1007\/BFb0028022"},{"key":"354074_CR21","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi, \u201cWeak alternating automata are not that weak,\u201d in Proc. 5th Israeli Symposium on Theory of Computing and Systems, IEEE Computer Society Press, 1997, pp. 147\u2013158.","DOI":"10.1109\/ISTCS.1997.595167"},{"key":"354074_CR22","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi, \u201cFreedom, weakness, and determinism: From linear-time to branching-time,\u201d in Proc. 13th IEEE Symposium on Logic in Computer Science, 1998, pp. 81\u201392.","DOI":"10.1109\/LICS.1998.705645"},{"key":"354074_CR23","doi-asserted-by":"crossref","unstructured":"O. Kupferman, M.Y. Vardi, and P. Wolper, \u201cAn automata-theoretic approach to branching-time model checking,\u201d Journal of the ACM, Vol. 47, No. 2, 2000.","DOI":"10.1145\/333979.333987"},{"key":"354074_CR24","unstructured":"L. Lamport, \u201cLogical foundation,\u201d in Distributed systems\u2014Methods and Tools for Specification, Lecture Notes in Computer Science, Vol. 190, Springer-Verlag, 1985."},{"key":"354074_CR25","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, \u201cChecking that finite state concurrent programs satisfy their linear specification,\u201d in Proc. 12th ACM Symposium on Principles of Programming Languages, New Orleans, 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"354074_CR26","doi-asserted-by":"crossref","unstructured":"Y. Luo, T. Wongsonegoro, and A. Aziz, \u201cHybrid techniques for fast functional simulation,\u201d in Proc. 35th Design Automation Conference, IEEE Computer Society, 1998.","DOI":"10.1145\/277044.277213"},{"key":"354074_CR27","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, N. Bjorner, A. Browne, E. Chang, M. Colon, L. De Alfaro, H. Devarajan, H. Sipma, and T. Uribe, \u201cSTeP: The Stanford temporal prover,\u201d Technical Report STAN-CS-TR\u201394\u20131518, Dept. of Computer Science, Stanford University, 1994.","DOI":"10.21236\/ADA324036"},{"key":"354074_CR28","first-page":"164","volume":"663","author":"K.L. McMillan","year":"1992","unstructured":"K.L. McMillan, \u201cUsing unfolding to avoid the state explosion problem in the verification of asynchronous circuits,\u201d in Proc. 4th Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 663, Springer-Verlag, 1992, pp. 164\u2013174.","journal-title":"Proc. 4th Conference on Computer Aided Verification"},{"key":"354074_CR29","doi-asserted-by":"crossref","unstructured":"A.R. Meyer and M.J. Fischer, \u201cEconomy of description by automata, grammars, and formal systems,\u201d in Proc. 12th IEEE Symp. on Switching and Automata Theory, 1971, pp. 188\u2013191.","DOI":"10.1109\/SWAT.1971.11"},{"key":"354074_CR30","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"S. Miyano and T. Hayashi, \u201cAlternating finite automata on \u03c9-words,\u201d Theoretical Computer Science, Vol. 32, pp. 321\u2013330, 1984.","journal-title":"Theoretical Computer Science"},{"key":"354074_CR31","doi-asserted-by":"crossref","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, 1992."},{"key":"354074_CR32","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, New York, 1995."},{"key":"354074_CR33","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-63166-6_36","volume":"1254","author":"S. Melzer","year":"1997","unstructured":"S. Melzer and S. Roemer, \u201cDeadlock checking using net unfoldings,\u201d in Computer Aided Verification, Proc. 9th Int. Conference, Lecture Notes in Computer Science, Vol. 1254, Springer-Verlag, 1997, pp. 364\u2013375.","journal-title":"Computer Aided Verification, Proc. 9th Int. Conference"},{"key":"354074_CR34","doi-asserted-by":"crossref","unstructured":"A.R. Meyer and L.J. Stockmeyer, \u201cThe equivalence problem for regular expressions with squaring requires exponential time,\u201d in Proc. 13th IEEE Symp. on Switching and Automata Theory, 1972, pp. 125\u2013129.","DOI":"10.1109\/SWAT.1972.29"},{"issue":"3","key":"354074_CR35","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, \u201cProving liveness properties of concurrent programs,\u201d ACM Transactions on Programming Languages and Systems, Vol. 4, No. 3, pp. 455\u2013495, 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"354074_CR36","first-page":"337","volume":"137","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis, \u201cSpecification and verification of concurrent systems in Cesar,\u201d in Proc. 5th International Symp. on Programming, Lecture Notes in Computer Science, Vol. 137, Springer-Verlag, 1981, pp. 337\u2013351.","journal-title":"Proc. 5th International Symp. on Programming"},{"key":"354074_CR37","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi, \u201cHigh-density reachability analysis,\u201d in Proc. Int'l Conf. on Computer-Aided Design, San Jose, 1995, pp. 154\u2013158.","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"354074_CR38","doi-asserted-by":"crossref","unstructured":"S. Safra, \u201cOn the complexity of \u03c9-automata,\u201d in Proc. 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988, pp. 319\u2013327.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"354074_CR39","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke, \u201cThe complexity of propositional linear temporal logic,\u201d Journal ACM, Vol. 32, pp. 733\u2013749, 1985.","journal-title":"Journal ACM"},{"key":"354074_CR40","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"A.P. Sistla, \u201cSatefy, liveness and fairness in temporal logic,\u201d Formal Aspects of Computing,Vol. 6, pp. 495\u2013511, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"354074_CR41","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, \u201cThe PVS proof checker: A reference manual (beta release),\u201d Technical Report, Computer Science laboratory, SRI International, Menlo Park, California, 1993."},{"issue":"1","key":"354074_CR42","doi-asserted-by":"crossref","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, \u201cTesting language containment for ?-automata using BDD's,\u201d Information and Computation, Vol. 118, No. 1, pp. 101\u2013109, 1995.","journal-title":"Information and Computation"},{"key":"354074_CR43","doi-asserted-by":"crossref","unstructured":"A. Valmari, \u201cOn-the-fly verification with stubborn sets,\u201d in Proc. 5nd Conference on Computer Aided Verifi-cation, Lecture Notes in Computer Science, Vol. 697, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_33"},{"key":"354074_CR44","doi-asserted-by":"crossref","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.6Vardi, \u201cAn automata-theoretic approach to linear temporal logic,\u201d in F. Moller and G. Birtwistle (Eds.), Logics for Concurrency: Structure versus Automata, Lecture Notes in Computer Science, Vol. 1043, Springer-Verlag, Berlin, 1996, pp. 238\u2013266."},{"key":"354074_CR45","unstructured":"M.Y. Vardi and P. Wolper, \u201cAn automata-theoretic approach to automatic program verification,\u201d in Proc. First Symposium on Logic in Computer Science, Cambridge, 1986, pp. 332\u2013344."},{"issue":"2","key":"354074_CR46","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi and P. Wolper, \u201cAutomata-theoretic techniques for modal logics of programs,\u201d Journal of Computer and System Science, Vol. 32, No. 2, pp. 182\u2013221, 1986.","journal-title":"Journal of Computer and System Science"},{"issue":"1","key":"354074_CR47","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper, \u201cReasoning about infinite computations,\u201d Information and Computation, Vol. 115, No. 1, pp. 1\u201337, 1994.","journal-title":"Information and Computation"},{"key":"354074_CR48","unstructured":"P. Wolper, \u201cSynthesis of Communicating Processes from Temporal Logic Specifications,\u201d Ph.D. Thesis, Stanford University, 1982."},{"key":"354074_CR49","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1007\/3-540-63166-6_37","volume":"1254","author":"J. Yuan","year":"1997","unstructured":"J. Yuan, J. Shen, J. Abraham, and A. Aziz, \u201cOn combining formal and informal verification,\u201d in Computer Aided Verification, Proc. 9th Int. Conference, Lecture Notes in Computer Science, Vol. 1254, Springer-Verlag, 1997, pp. 376\u2013387.","journal-title":"Computer Aided Verification, Proc. 9th Int. Conference"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011254632723.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011254632723\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011254632723.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:06:44Z","timestamp":1754420804000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011254632723"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,11]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2001,11]]}},"alternative-id":["354074"],"URL":"https:\/\/doi.org\/10.1023\/a:1011254632723","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,11]]}}}