{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T19:10:24Z","timestamp":1736277024647,"version":"3.32.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006,1]]},"DOI":"10.1007\/s10703-006-4342-y","type":"journal-article","created":{"date-parts":[[2006,2,9]],"date-time":"2006-02-09T00:15:00Z","timestamp":1139444100000},"page":"57-84","source":"Crossref","is-referenced-by-count":24,"title":["Model Checking with Strong Fairness"],"prefix":"10.1007","volume":"28","author":[{"given":"Yonit","family":"Kesten","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Li-On","family":"Raviv","sequence":"additional","affiliation":[]},{"given":"Elad","family":"Shahar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"4342_CR1","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 Inf. and Comp., Vol. 98, No. 2, pp. 142\u2013170, 1992.","journal-title":"Inf. and Comp."},{"key":"4342_CR2","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and E.A. Emerson, \u201cDesign and synthesis of synchronization skeletons using branching time temporal logic,\u201d in Proc. IBM Workshop on Logics of Programs, Volume 131 of Lect. Notes in Comp. Sci., Springer-Verlag, 1981, pp. 52\u201371.","DOI":"10.1007\/BFb0025774"},{"key":"4342_CR3","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and K. Hamaguchi, \u201cAnother look at ltl model checking,\u201d Formal Methods in System Design, Vol. 10, No. 1, 1997.","DOI":"10.1023\/A:1008615614281"},{"key":"4342_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, D.E. Long, and X. Zhao, \u201cEfficient generation of counterexamples and witnesses in symbolic model checking,\u201d in Proc. Design Automation Conference 95 (DAC95), 1995.","DOI":"10.1145\/217474.217565"},{"key":"4342_CR5","unstructured":"E.A. Emerson and C.L. Lei, \u201cEfficient model-checking in fragments of the propositional modal \u03bc-calculus,\u201d in Proc. First IEEE Symp. Logic in Comp. Sci., pp. 267\u2013278, 1986."},{"key":"4342_CR6","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"E.A. Emerson and C. Lei, \u201cModalities for model checking: Branching time logic strikes back,\u201d Science of Computer Programming, Vol. 8, pp. 275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"4342_CR7","doi-asserted-by":"crossref","unstructured":"N. Francez, Fairness, Springer-Verlag, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"4342_CR8","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, \u201cOn the temporal analysis of fairness,\u201d in Proc. 7th ACM Symp. Princ. of Prog. Lang., pp. 163\u2013173, 1980.","DOI":"10.1145\/567446.567462"},{"key":"4342_CR9","doi-asserted-by":"crossref","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 O. Grumberg and O. Grumberg (Eds.), Proc. 9th Intl. Conference on Computer Aided Verification, (CAV'97), Volume 1254 of Lect. Notes in Comp. Sci., Springer-Verlag, 1997, pp. 268\u2013278.","DOI":"10.1007\/3-540-63166-6_27"},{"key":"4342_CR10","doi-asserted-by":"crossref","unstructured":"M.R. Henzinger and J.A. Telle, \u201cFaster algorithms for the nonemptiness of street automata and for communication protocol prunning,\u201d in Proceedings of the 5th Scandina vian Workshop on Algorithn Theory, 1996, pp. 10\u201320.","DOI":"10.1007\/3-540-61422-2_117"},{"key":"4342_CR11","doi-asserted-by":"crossref","unstructured":"R. Hojati, H. Touati, R.P. Kurshan, and R.K. Brayton, \u201cEfficient \u03c9-regular language containment,\u201d in G.V. Bochmann and D.K. Probst (Eds.), Proc. 4th Intl. Conference on Computer Aided Verification (CAV'92), Volume 697 of Lect. Notes in Comp. Sci., Springer-Verlag, number 663 in Lect. Notes in Comp. Sci., SPringer-Verlag, 1992, pp. 396\u2013409.","DOI":"10.1007\/3-540-56496-9_31"},{"key":"4342_CR12","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Y. Kesten and A. Pnueli, \u201cVerification by augmented finitary abstraction, Inf. and Comp., Vol. 163, pp. 203\u2013243, 2000.","journal-title":"Inf. and Comp."},{"key":"4342_CR13","doi-asserted-by":"crossref","unstructured":"Y. Kesten, A. Pnueli, and L. Raviv, \u201cAlgorithmic verification of linear temporal logic specifications,\u201d in K.G. Larsen, S. Skyum, and G. Winskel (Eds.), Proc, 25th Int. Col-loq. Aut. Lang. Prog., Volume 1443 of Lect. Notes in Comp. Sci., Springer-Verlag, 1998, pp. 1\u201316.","DOI":"10.1007\/BFb0055036"},{"key":"4342_CR14","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1995","unstructured":"R.P. Kurshan, Computer Aided Verification of Coordinating Processes, Princeton University Press, Princeton, New Jersey, 1995."},{"key":"4342_CR15","unstructured":"O. Lichtenstein, \u201cDecidability, completeness, and extensions of linear time temporal logic,\u201d PhD thesis, Weizmann Institute of Science, 1991."},{"key":"4342_CR16","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 Symp. Princ. of Prog. Lang., 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"4342_CR17","doi-asserted-by":"crossref","unstructured":"D. Lehmann, A. Pnueli, and J. Stavi, \u201cImpartiality, justice and fairness: The ethics of concurrent termination,\u201d in Proc. 8th Int. Colloq. Aut. Lang. Prog., Volume 115 of Lect. Notes in Comp. Sci., Springer-Verlag, 1981, pp. 264\u2013277.","DOI":"10.1007\/3-540-10843-2_22"},{"key":"4342_CR18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck, \u201cThe glory of the past,\u201d in Proc. Conf. Logics of Programs, Volume 193 of Lect. Notes in Comp. Sci., Springer-Verlag, 1985, pp. 196\u2013218.","DOI":"10.1007\/3-540-15648-8_16"},{"issue":"1","key":"4342_CR19","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli, \u201cCompleting the temporal picture,\u201d Theor. Comp. Sci., Vol. 83, No. 1, pp. 97\u2013130, 1991.","journal-title":"Theor. Comp. Sci."},{"key":"4342_CR20","volume-title":"Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli, Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York, 1991."},{"key":"4342_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, Springer-Verlag, New York, 1995."},{"key":"4342_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Shahar, \u201cA platform for combining deductive with algorithmic verification,\u201d in R. Alur and T. Henzinger, R. Alur and T. Henzinger (Eds.), Proc. 8th Intl. Conference on Computer Aided Verification (CAV'96), Volume 1102 of Led. Notes in Comp. Sci., Springer- Verlag, 1996, pp. 184\u2013195.","DOI":"10.1007\/3-540-61474-5_68"},{"key":"4342_CR23","doi-asserted-by":"crossref","unstructured":"J.P. Queille and J. Sifakis, \u201cSpecification and verification of concurrent systems,\u201d in cesar in M. Dezani-Ciancaglini and M. Montanari (Eds.), International Symposium on Programming, Volume 137 of Lect. Notes in Comp. Sci., Springer-Verlag, 1982, pp. 337\u2013351.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"4342_CR24","doi-asserted-by":"crossref","unstructured":"K. Ravi, R. Bloem, and F. Somenzi, \u201cA comparative study of symbolic algorithms for the computation of fair cycles,\u201d in W.A. Hunt, Jr. and S.D. Johnson (Eds.), Formal Methods in Computer Aided Design, Volume 1954 of Lect. Notes in Comp. Sci., Springer-Verlag, 2000, pp. 143\u2013160.","DOI":"10.1007\/3-540-40922-X_10"},{"key":"4342_CR25","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1016\/0890-5401(89)90004-7","volume":"82","author":"F.A. Stomp","year":"1989","unstructured":"F.A. Stomp, W.-P. de Roever, and R.T. Gerth, \u201cThe \u03bc-calculus as an assertion language for fairness arguments,\u201d Inf. and Comp., Vol. 82, pp. 278\u2013322, 1989.","journal-title":"Inf. and Comp."},{"key":"4342_CR26","unstructured":"M.Y. Vardi and P. Wolper, \u201cAn automata-theoretic approach to automatic program verification,\u201d in Proc. First IEEE Symp. Logic in Comp. Sci., 1986, pp. 332\u2013344."},{"key":"4342_CR27","unstructured":"Z. Yang, \u201cPerformance analysis of symbolic reachability algorithms in model checking,\u201d Master's thesis, Rice University, 1999."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-4342-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-4342-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-4342-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T17:59:40Z","timestamp":1736272780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-4342-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["4342"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-4342-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2006,1]]}}}