{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T02:24:37Z","timestamp":1773282277340,"version":"3.50.1"},"publisher-location":"Boston","reference-count":26,"publisher":"Kluwer Academic Publishers","isbn-type":[{"value":"1402081405","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8141-3_38","type":"book-chapter","created":{"date-parts":[[2006,2,21]],"date-time":"2006-02-21T15:15:11Z","timestamp":1140534911000},"page":"493-506","source":"Crossref","is-referenced-by-count":24,"title":["Controller Synthesis for Probabilistic Systems (Extended Abstract)"],"prefix":"10.1007","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[]},{"given":"Marcus","family":"Gr\u00f6\u00dfer","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Leucker","sequence":"additional","affiliation":[]},{"given":"Benedikt","family":"Bollig","sequence":"additional","affiliation":[]},{"given":"Frank","family":"Ciesinski","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"38_CR1","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"Baier, C. and Kwiatkowska, M. (1998). Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3): 125\u2013155.","journal-title":"Distributed Computing"},{"key":"38_CR2","first-page":"499","volume":"1026","author":"A. Bianco","year":"1995","unstructured":"Bianco, A. and De Alfaro, L. (1995). Model checking of probabilistic and non-deterministic systems. In Proc. FST & TCS, LNCS 1026, pages 499\u2013513.","journal-title":"LNCS"},{"key":"38_CR3","first-page":"180","volume":"2725","author":"P. Bouyer","year":"2003","unstructured":"Bouyer, P., D\u2019Souza, D., Madhusudan, P., and Petit, A. (2003). Timed control with partial observability. In Proc. CAV LNCS 2725, pages 180\u2013192.","journal-title":"LNCS"},{"key":"38_CR4","first-page":"100","volume":"2803","author":"K. Chatterjee","year":"2003","unstructured":"Chatterjee, K., Jurdzinski, M., and Henzinger, T. (2003). Simple stochastic parity games. In Proc. CSL LNCS 2803, pages 100\u2013113.","journal-title":"LNCS"},{"key":"38_CR5","unstructured":"Chatterjee, K., Jurdzinski, M., and Henzinger, T. (2004). Quantitative simple stochastic parity games. In Proceedings of the Annual Symposium on Discrete Algorithms (SODA). SIAM."},{"key":"38_CR6","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A. Condon","year":"1992","unstructured":"Condon, A. (1992). The complexity of stochastic games. Inf. and Comp., 96:203\u2013224.","journal-title":"Inf. and Comp."},{"key":"38_CR7","first-page":"51","volume":"13","author":"A. Condon","year":"1993","unstructured":"Condon, A. (1993). On algorithms for simple stochastic games. DIMACS, 13:51\u201371.","journal-title":"DIMACS"},{"key":"38_CR8","unstructured":"de Alfaro, L. (1997). Formal Verification of Probabilistic Systems. PhD thesis, Stanford University. Technical report STAN-CS-TR-98-1601."},{"key":"38_CR9","first-page":"144","volume":"2761","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., and Stoelinga, M. (2003). The element of surprise in timed games. In Proc. CONCUR, LNCS 2761, pages 144\u2013158.","journal-title":"LNCS"},{"key":"38_CR10","doi-asserted-by":"crossref","unstructured":"de Alfaro, L. and Henzinger, T. (2000). Concurrent omega-regular games. In Proc. LICS, pages 141\u2013154. IEEE Computer Society Press.","DOI":"10.1109\/LICS.2000.855763"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T., and Kupferman, O. (1998). Concurrent reachability games. In Proc. FOCS, pages 564\u2013575. IEEE Computer Society Press.","DOI":"10.1109\/SFCS.1998.743507"},{"key":"38_CR12","unstructured":"de Alfaro, L. and Majumdar, R. (2001). Quantitative solution of omega-regular games. In Proc. STOC\u201901, pages 675\u2013683. ACM Press."},{"key":"38_CR13","unstructured":"Derman, C. (1970). Finite-State Markovian Decision Processes. Academic Press."},{"key":"38_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E. and Jutla, C. (1991). Tree automata, mu-calculus and determinacy. In Proc.FOCS, pages 368\u2013377. IEEE Computer Society Press.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"38_CR15","unstructured":"Emerson, E. A., Jutla, C. S., and Sistla, A. P. (1993). On model-checking for fragments of mucalculus. In Courcoubetis, C., editor, Proc. CAV, LNCS 697, pages 385\u2013396."},{"key":"38_CR16","unstructured":"Filar, J. and Vrieze, K. (1997). Competitive Markov Decision Processes. Springer."},{"key":"38_CR17","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H. and Jonsson, B. (1994). A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512\u2013535.","journal-title":"Formal Aspects of Computing"},{"key":"38_CR18","first-page":"290","volume":"1770","author":"M. Jurdzinski","year":"2000","unstructured":"Jurdzinski, M. (2000). Small progress for solving parity games. In Proc. STACS, volume 1770 of LNCS, pages 290\u2013301.","journal-title":"LNCS"},{"key":"38_CR19","first-page":"292","volume":"2471","author":"M. Jurdzinski","year":"2003","unstructured":"Jurdzinski, M., Kupferman, O., and Henzinger, T. (2003). Trading probability for fairness. In Proc.CSL, LNCS 2471, pages 292\u2013305.","journal-title":"LNCS"},{"key":"38_CR20","first-page":"23","volume":"2028","author":"J. C. Mitchell","year":"2001","unstructured":"Mitchell, J. C. (2001). Probabilistic polynomial-time process calculus and security protocol analysis. In Proc. ESOP LNCS 2028, pages 23\u201329.","journal-title":"LNCS"},{"key":"38_CR21","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A. and Zuck, L. (1986). Verification of multiprocess probabilistic protocols. Distributed Computing, 1:53\u201372.","journal-title":"Distributed Computing"},{"key":"38_CR22","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M. L. Puterman","year":"1994","unstructured":"Puterman, M. L. (1994). Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York, NY."},{"key":"38_CR23","doi-asserted-by":"crossref","unstructured":"Thomas, W. (1990). Automata on infinite objects. In van Leeuwen, J., editor, Handbook of Theoretical Computer Science, volume B, chapter 4, pages 133\u2013191. Elsevier Science Publishers","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"38_CR24","first-page":"58","volume":"2725","author":"W. Thomas","year":"2003","unstructured":"Thomas, W. (2003). Infinite games and verification In Poc. CAV LNCS 2725, pages 58\u201364.","journal-title":"LNCS"},{"key":"38_CR25","doi-asserted-by":"crossref","unstructured":"Vardi, M. Y. (1985). Automatic verification of probabilistic concurrent finite-state programs. In Proc. FOCS, pages 327\u2013338, Portland, Oregon. IEEE.","DOI":"10.1109\/SFCS.1985.12"},{"key":"38_CR26","first-page":"202","volume":"1855","author":"J. V\u00f6ge","year":"2000","unstructured":"V\u00f6ge, J. and Jurdzinski, M. (2000). A discrete strategy improvement algorithm for solving parity games. In Proc. CAV, LNCS 1855, pages 202\u2013215.","journal-title":"LNCS"}],"container-title":["IFIP International Federation for Information Processing","Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8141-3_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:28:20Z","timestamp":1619555300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8141-3_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081405"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8141-3_38","relation":{},"subject":[]}}