{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:07Z","timestamp":1776316927899,"version":"3.50.1"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T00:00:00Z","timestamp":1284595200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2011,11]]},"DOI":"10.1007\/s10009-010-0169-3","type":"journal-article","created":{"date-parts":[[2010,9,15]],"date-time":"2010-09-15T21:26:23Z","timestamp":1284585983000},"page":"571-584","source":"Crossref","is-referenced-by-count":11,"title":["LTL generalized model checking revisited"],"prefix":"10.1007","volume":"13","author":[{"given":"Patrice","family":"Godefroid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,9,16]]},"reference":[{"key":"169_CR1","unstructured":"Antonik, A., Huth, M., Larsen, K., Nyman, U., Wasowski, A.: 20 years of mixed and modal specifications. Bulletin of the European Association for Theoretical Computer Science (2008)"},{"key":"169_CR2","unstructured":"Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC Symp. on System Structure and Control, pp. 469\u2013474. Elsevier, Amsterdam (1998)"},{"key":"169_CR3","doi-asserted-by":"crossref","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: 11th Computer Aided Verification, pp. 274\u2013287 (1999)","DOI":"10.1007\/3-540-48683-6_25"},{"key":"169_CR4","doi-asserted-by":"crossref","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: 11th Concurrency Theory. Lecture Notes in Computer Science, vol. 1877, pp. 168\u2013182 (2000)","DOI":"10.1007\/3-540-44618-4_14"},{"key":"169_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM Toolkit. In: 13th Computer Aided Verification. Lecture Notes in Computer Science, vol. 2102, pp. 260\u2013264, Springer, Paris (2001)","DOI":"10.1007\/3-540-44585-4_25"},{"key":"169_CR6","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Chechik, M.: How thorough is thorough enough? In: 13th Correct Hardware Design and Verification Methods (2005)","DOI":"10.1007\/11560548_8"},{"key":"169_CR7","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Huth, M.: Model checking vs. generalized model checking: semantic minimizations for temporal logics. In: 20th Logic in Computer Science, pp. 158\u2013167, Chicago, June (2005)","DOI":"10.1109\/LICS.2005.28"},{"key":"169_CR8","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: 12th Concurrency Theory. Lecture Notes in Computer Science, vol. 2154, pp. 426\u2013440. Springer, Aalborg (2001)","DOI":"10.1007\/3-540-44685-0_29"},{"key":"169_CR9","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: 14th Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 137\u2013150. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_11"},{"key":"169_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Jagadeesan, R.: On the Expressiveness of 3-valued models. In: 4th Verification, Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2575, pp. 206\u2013222. Springer, New York (2003)","DOI":"10.1007\/3-540-36384-X_18"},{"key":"169_CR11","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: 9th Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254, pp. 72\u201383. Springer, Haifa (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"169_CR12","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. Lecture Notes in Computer Science, vol. 2500. Springer, Berlin (2002)","DOI":"10.1007\/3-540-36387-4"},{"key":"169_CR13","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Systematic construction of abstractions for model-checking. In: 7th Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 3855, pp. 381\u2013397. Springer, Berlin (2006)","DOI":"10.1007\/11609773_25"},{"key":"169_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: 29th Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"169_CR15","doi-asserted-by":"crossref","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: a foundation for three-valued program analysis. In: 10th European Symp. on Programming. Lecture Notes in Computer Science, vol. 2028. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45309-1_11"},{"key":"169_CR16","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: 17th Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 1770, pp. 290\u2013301. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46541-3_24"},{"key":"169_CR17","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1987","unstructured":"Kleene S.C.: Introduction to Metamathematics. North Holland, Amsterdam (1987)"},{"key":"169_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Morgenstern, G., Murano, A.: Typeness for \u03c9-regular automata. In: 2nd Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 3299, pp. 324\u2013338. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30476-0_27"},{"key":"169_CR19","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace containment. In: 15th Computer Aided Verification. Lecture Notes in Computer Science, vol. 2725, pp. 381\u2013393. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_36"},{"issue":"2","key":"169_CR20","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman O., Vardi M.Y., Wolper P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"169_CR21","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: 3rd Logic in Computer Science, pp. 203\u2013210 (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"169_CR22","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: 9th Symposium on Principles of Distributed Computing, pp. 377\u2013410. ACM, New York (1990)","DOI":"10.1145\/93385.93442"},{"key":"169_CR23","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"3","key":"169_CR24","doi-asserted-by":"crossref","first-page":"5","DOI":"10.2168\/LMCS-3(3:5)2007","volume":"3","author":"N. Piterman","year":"2007","unstructured":"Piterman N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Logical Methods Comput. Sci. 3(3), 5 (2007)","journal-title":"Logical Methods Comput. Sci."},{"key":"169_CR25","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Saar, Y.: Synthesis of reactive(1) designs. In: 7th Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 3855, pp. 364\u2013380. Springer, Berlin (2006)","DOI":"10.1007\/11609773_24"},{"key":"169_CR26","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"169_CR27","first-page":"81","volume":"77","author":"P.J.G. Ramadge","year":"1989","unstructured":"Ramadge P.J.G., Wonham W.M.: The control of discrete event systems. IEEE Trans. Control Theory 77, 81\u201398 (1989)","journal-title":"IEEE Trans. Control Theory"},{"key":"169_CR28","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: 29th Foundations of Computer Science, pp. 319\u2013327, White Plains, October (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"169_CR29","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla A.P., Vardi M.Y., Wolper P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"169_CR30","unstructured":"van Emde Boas, P.: The convenience of tilings. In: Complexity, Logic and Recursion Theory. Lecture Notes in Pure and Applied Mathetaics, vol. 187, pp. 331\u2013363 (1997)"},{"issue":"2","key":"169_CR31","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi M.Y., Wolper P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 182\u2013221 (1986)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"169_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi M.Y., Wolper P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0169-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0169-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0169-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T21:27:32Z","timestamp":1740518852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0169-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,16]]},"references-count":32,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["169"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0169-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,9,16]]}}}