{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T10:47:42Z","timestamp":1753181262629,"version":"3.41.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319961415"},{"type":"electronic","value":"9783319961422"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_13","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T19:55:08Z","timestamp":1532116508000},"page":"178-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Monika","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Veronika","family":"Loitzenbauer","sequence":"additional","affiliation":[]},{"given":"Simin","family":"Oraee","sequence":"additional","affiliation":[]},{"given":"Viktor","family":"Toman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"6","key":"13_CR1","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C\u201327","author":"SB Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C\u201327(6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR2","unstructured":"Alur, R., Henzinger, T.A.: Computer-aided verification (2004). http:\/\/www.cis.upenn.edu\/group\/cis673\/"},{"key":"13_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"1","key":"13_CR4","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1093\/logcom\/exp003","volume":"21","author":"J Barnat","year":"2011","unstructured":"Barnat, J., Chaloupka, J., van de Pol, J.: Distributed algorithms for SCC decomposition. J. Log. Comput. 21(1), 23\u201344 (2011)","journal-title":"J. Log. Comput."},{"issue":"1","key":"13_CR5","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s10703-006-4341-z","volume":"28","author":"R Bloem","year":"2006","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in $$n$$n log $$n$$n symbolic steps. Form. Methods Syst. Des. 28(1), 37\u201356 (2006)","journal-title":"Form. Methods Syst. Des."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic manipulation of Boolean functions using a graphical representation. In: Conference on Design Automation, DAC, pp. 688\u2013694 (1985)","DOI":"10.1109\/DAC.1985.1586017"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Dvo\u0159\u00e1k, W., Henzinger, M., Loitzenbauer, V.: Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In: LICS, pp. 197\u2013206 (2016)","DOI":"10.1145\/2933575.2935304"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: SODA, pp. 1318\u20131336 (2011)","DOI":"10.1137\/1.9781611973082.101"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: An $$O(n^2)$$O(n2) time algorithm for alternating B\u00fcchi games. In: SODA, pp. 1386\u20131399 (2012)","DOI":"10.1137\/1.9781611973099.109"},{"issue":"3","key":"13_CR10","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/2597631","volume":"61","author":"K Chatterjee","year":"2014","unstructured":"Chatterjee, K., Henzinger, M.: Efficient and dynamic algorithms for alternating B\u00fcchi games and maximal end-component decomposition. J. ACM 61(3), 15 (2014)","journal-title":"J. ACM"},{"issue":"3","key":"13_CR11","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/s10703-012-0180-2","volume":"42","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., Henzinger, M., Joglekar, M., Shah, N.: Symbolic algorithms for qualitative analysis of Markov decision processes with B\u00fcchi objectives. Form. Methods Syst. Des. 42(3), 301\u2013327 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M., Loitzenbauer, V.: Improved algorithms for one-pair and $$k$$k-pair Streett objectives. In: LICS, pp. 269\u2013280 (2015)","DOI":"10.1109\/LICS.2015.34"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M., Loitzenbauer, V., Oraee, S., Toman, V.: Symbolic algorithms for graphs and Markov decision processes with fairness objectives. arXiv:1804.00206 (2018)","DOI":"10.1007\/978-3-319-96142-2_13"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-45220-1_11","volume-title":"Computer Science Logic","author":"K Chatterjee","year":"2003","unstructured":"Chatterjee, K., Jurdzi\u0144ski, M., Henzinger, T.A.: Simple stochastic parity games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 100\u2013113. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45220-1_11"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Dvo\u0159\u00e1k, W., Henzinger, M., Loitzenbauer, V.: Lower bounds for symbolic computation on graphs: strongly connected components, liveness, safety, and diameter. In: SODA, pp. 2341\u20132356 (2018)","DOI":"10.1137\/1.9781611975031.151"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-642-39799-8_37","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., Gaiser, A., K\u0159et\u00ednsk\u00fd, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559\u2013575. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_37"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Ciesinski, F., Baier, C.: LiQuor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: QEST, pp. 131\u2013132 (2006)","DOI":"10.1109\/QEST.2006.25"},{"issue":"4","key":"13_CR18","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. (STTT) 2(4), 410\u2013425 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"13_CR19","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR20","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Symbolic model checking. In: Model Checking. MIT Press (1999)"},{"key":"13_CR21","unstructured":"CWI\/SEN2 and INRIA\/VASY: The VLTS Benchmark Suite. http:\/\/cadp.inria.fr\/resources\/vlts"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-319-08867-9_13","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2014","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192\u2013208. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_13"},{"key":"13_CR24","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected components in a linear number of symbolic steps. In: SODA, pp. 573\u2013582 (2003)"},{"issue":"1","key":"13_CR25","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/s00453-007-9079-5","volume":"50","author":"R Gentilini","year":"2008","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Symbolic graphs: linear solutions to connectivity related problems. Algorithmica 50(1), 120\u2013158 (2008)","journal-title":"Algorithmica"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-61422-2_117","volume-title":"Algorithm Theory\u2014SWAT 1996","author":"MR Henzinger","year":"1996","unstructured":"Henzinger, M.R., Telle, J.A.: Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. In: Karlsson, R., Lingas, A. (eds.) SWAT 1996. LNCS, vol. 1097, pp. 16\u201327. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61422-2_117"},{"issue":"5","key":"13_CR27","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-11936-6_17","volume-title":"Automated Technology for Verification and Analysis","author":"Z Kom\u00e1rkov\u00e1","year":"2014","unstructured":"Kom\u00e1rkov\u00e1, Z., K\u0159et\u00ednsk\u00fd, J.: Rabinizer 3: safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 235\u2013241. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_17"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"4","key":"13_CR30","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"CY Lee","year":"1959","unstructured":"Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38(4), 985\u2013999 (1959)","journal-title":"Bell Syst. Tech. J."},{"key":"13_CR31","unstructured":"Loitzenbauer, V.: Improved algorithms and conditional lower bounds for problems in formal verification and reactive synthesis. Ph.D. thesis. University of Vienna (2016)"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Progress (Draft) (1996)","DOI":"10.21236\/ADA329718"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-40922-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"K Ravi","year":"2000","unstructured":"Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 162\u2013179. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_10"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of $$\\omega $$\u03c9-automata. In: FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"13_CR35","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 3.0.0 (2015). http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T22:59:11Z","timestamp":1751756351000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}