{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:10Z","timestamp":1776304930257,"version":"3.50.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,3,17]],"date-time":"2006-03-17T00:00:00Z","timestamp":1142553600000},"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":[[2006,6]]},"DOI":"10.1007\/s10009-005-0193-x","type":"journal-article","created":{"date-parts":[[2006,3,18]],"date-time":"2006-03-18T09:27:36Z","timestamp":1142674056000},"page":"261-279","source":"Crossref","is-referenced-by-count":16,"title":["Liveness with invisible ranking"],"prefix":"10.1007","volume":"8","author":[{"given":"Yi","family":"Fang","sequence":"first","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,3,17]]},"reference":[{"issue":"6","key":"193_CR1","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Proc. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Proc. Lett."},{"key":"193_CR2","doi-asserted-by":"crossref","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer-Aided Verification (CAV\u201901). Lecture Notes in Computer Science, vol. 2102, pp. 221\u2013234. Springer, Berlin Heidelberg New York (2001)","DOI":"10.1007\/3-540-44585-4_19"},{"key":"193_CR3","unstructured":"Bj\u00f8rner, N., Browne, I.A., Chang, E., Col\u00f3on, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: The Stanford temporal prover, user\u2019s manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, Stanford, CA (1995)"},{"key":"193_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parametrized networks using abstraction and regular languages. In: Proceedings of the 6th International Conference on Concurrency Theory (CONCUR92), Philadelphia. Lecture Notes in Computer Science, vol. 962, pp. 395\u2013407. Springer, Berlin Heidelberg New York (1995)","DOI":"10.1007\/3-540-60218-6_30"},{"key":"193_CR5","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Choueka, Y.: Theories of automata on \u03c9-tapes: a simplified approach. J. Comput. Syst. Sci. 8, 117\u2013141 (1974)","journal-title":"J. Comput. Syst. Sci."},{"key":"193_CR6","doi-asserted-by":"crossref","unstructured":"Colon, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of the 14th International Conference on Computer-Aided Verification (CAV\u201902). Lecture Notes in Computer Science, vol. 2404, pp. 442\u2013454. Springer, Berlin Heidelberg New York (2002)","DOI":"10.1007\/3-540-45657-0_36"},{"key":"193_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17), pp. 236\u2013255 (2000)","DOI":"10.1007\/10721959_19"},{"key":"193_CR8","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Procedings of the 22nd ACM Conference on Principles of Programming Languages (POPL\u201995), San Francisco (1995)","DOI":"10.1145\/199448.199468"},{"key":"193_CR9","doi-asserted-by":"crossref","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with incomprehensible ranking. In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904). Lecture Notes in Computer Science, vol. 2988, pp. 482\u2013496. Springer, Berlin Heidelberg New York (2004)","DOI":"10.1007\/978-3-540-24730-2_36"},{"key":"193_CR10","doi-asserted-by":"crossref","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with invisible ranking. In: Proceedings of the 5th conference on Verification, Model Checking, and Abstract Interpretation, Venice, Italy. Lecture Notes in Computer Science, vol. 2937, pp. 223\u2013238. Springer, Berlin Heidelberg New York (2004)","DOI":"10.1007\/978-3-540-24622-0_19"},{"key":"193_CR11","doi-asserted-by":"crossref","unstructured":"Gyuris, V., Sistla, A.P.: On-the-fly model checking under fairness that exploits symmetry. In: Grumberg, O. (ed.) Proceedings of the 9th International Conference on Computer-Aided Verification (CAV\u201997). Lecture Notes in Computer Science, vol. 1254. Springer, Berlin Heidelberg New York (1997)","DOI":"10.1007\/3-540-63166-6_24"},{"key":"193_CR12","doi-asserted-by":"crossref","unstructured":"Gribomont, E.P., Zenner, G.: Automated verification of szymanski\u2019s algorithm. In: Steffen, B. (ed.) Proceedings of 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998). Lecture Notes in Computer Science, vol. 1384, pp. 424\u2013438. Springer, Berlin Heidelberg New York (1998)","DOI":"10.1007\/BFb0054187"},{"key":"193_CR13","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Graf, S., Schwartzbach, M. (eds.) Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201900). Lecture Notes in Computer Science, vol. 1785. Springer, Berlin Heidelberg New York (2000)","DOI":"10.1007\/3-540-46419-0_16"},{"key":"193_CR14","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. In: Hunt Jr, W., Somenzi, F. (eds.) Proceedings of the 15th International Conference on Computer-Aided Verification (CAV\u201903), pp. 381\u2013392. Boulder, CO (2003)","DOI":"10.1007\/978-3-540-45069-6_36"},{"key":"193_CR15","doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL\u201997), Paris (1997)","DOI":"10.1145\/263699.263747"},{"key":"193_CR16","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y., Hu, A.J., Vardi, M.Y. (eds.) Proceedings of the 10th International Conference on Computer-Aided Verification (CAV\u201998). Lecture Notes in Computer Science, vol. 1427, pp. 110\u2013121. Springer, Berlin Heidelberg New York (1998)","DOI":"10.1007\/BFb0028738"},{"key":"193_CR17","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 97\u2013130 (1991)"},{"key":"193_CR18","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin Heidelberg New York (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"193_CR19","unstructured":"Owre, S., Shankar, N., Rushby, J.M.: User guide for the PVS specification and verification system (draft). Technical Report, Computer Science Laboratory, SRI International, Menlo Park, CA (1993)"},{"key":"193_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901). Lecture Notes in Computer Science, vol. 2031, pp. 82\u201397. Springer, Berlin Heidelberg New York (2001)","DOI":"10.1007\/3-540-45319-9_7"},{"key":"193_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, \u221e)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of the 14th International Conference on Computer Aided Verification (CAV\u201902). Lecture Notes in Computer Science, vol. 2404, pp. 107\u2013122. Springer, Berlin Heidelberg New York (2002)","DOI":"10.1007\/3-540-45657-0_9"},{"key":"193_CR22","unstructured":"Shahar, E.: The TLV manual (2000). http:\/\/www.wisdom.weizmann.ac.il\/~verify\/tlv"},{"key":"193_CR23","doi-asserted-by":"crossref","unstructured":"Szymanski, B.K.: A simple solution to Lamport\u2019s concurrent programming problem with linear wait. In: Proceedings of the International Conference on Supercomputing Systems, pp. 621\u2013626, St. Malo, France (1988)","DOI":"10.1145\/55364.55425"},{"key":"193_CR24","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Verification of concurrent programs \u2013 the automata-theoretic framework. Ann. Pure Appl. Logic 51, 79\u201398 (1991)","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"193_CR25","doi-asserted-by":"crossref","unstructured":"Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems. Comput. Lang. Syst. Struct. 30 (3\/4), 139\u2013169 (2004)","DOI":"10.1016\/j.cl.2004.02.006"}],"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-005-0193-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-005-0193-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-005-0193-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:21Z","timestamp":1559114721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-005-0193-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3,17]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,6]]}},"alternative-id":["193"],"URL":"https:\/\/doi.org\/10.1007\/s10009-005-0193-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,3,17]]}}}