{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T06:49:06Z","timestamp":1764053346090},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548611"},{"type":"electronic","value":"9783642548628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_44","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:33:34Z","timestamp":1395408814000},"page":"531-546","source":"Crossref","is-referenced-by-count":12,"title":["Permissive Controller Synthesis for Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Dr\u00e4ger","sequence":"first","affiliation":[]},{"given":"Vojt\u011bch","family":"Forejt","sequence":"additional","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Mateusz","family":"Ujma","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"44_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-tiga: Time for playing games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 121\u2013125. Springer, Heidelberg (2007)"},{"issue":"3","key":"44_CR2","first-page":"261","volume":"36","author":"J. Bernet","year":"2002","unstructured":"Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. ITA\u00a036(3), 261\u2013275 (2002)","journal-title":"ITA"},{"key":"44_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-04081-8_14","volume-title":"CONCUR 2009 - Concurrency Theory","author":"P. Bouyer","year":"2009","unstructured":"Bouyer, P., Duflot, M., Markey, N., Renault, G.: Measuring permissivity in finite games. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 196\u2013210. Springer, Heidelberg (2009)"},{"key":"44_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-24372-1_11","volume-title":"Automated Technology for Verification and Analysis","author":"P. Bouyer","year":"2011","unstructured":"Bouyer, P., Markey, N., Olschewski, J., Ummels, M.: Measuring permissiveness in parity games: Mean-payoff parity games revisited. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 135\u2013149. Springer, Heidelberg (2011)"},{"issue":"9","key":"44_CR5","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/2330667.2330686","volume":"55","author":"R. Calinescu","year":"2012","unstructured":"Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. CACM\u00a055(9), 69\u201377 (2012)","journal-title":"CACM"},{"key":"44_CR6","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Johnson, K., Kikuchi, S.: Compositional reverification of probabilistic safety properties for large-scale complex IT systems. In: LSCITS (2012)","DOI":"10.1007\/978-3-642-34059-8_16"},{"key":"44_CR7","first-page":"460","volume-title":"Proc. STOC 1988","author":"J. Canny","year":"1988","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. In: Proc. STOC 1988, pp. 460\u2013467. ACM, New York (1988)"},{"key":"44_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-28756-5_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Chen","year":"2012","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 315\u2013330. Springer, Heidelberg (2012)"},{"key":"44_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-36742-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: A model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 185\u2013191. Springer, Heidelberg (2013)"},{"key":"44_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-22359-4_14","volume-title":"Computational Logic in Multi-Agent Systems","author":"T. Chen","year":"2011","unstructured":"Chen, T., Kwiatkowska, M., Parker, D., Simaitis, A.: Verifying team formation protocols with probabilistic model checking. In: Leite, J., Torroni, P., \u00c5gotnes, T., Boella, G., van der Torre, L. (eds.) CLIMA XII 2011. LNCS, vol.\u00a06814, pp. 190\u2013207. Springer, Heidelberg (2011)"},{"key":"44_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-642-40196-1_28","volume-title":"Quantitative Evaluation of Systems","author":"T. Chen","year":"2013","unstructured":"Chen, T., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: Synthesis for multi-objective stochastic games: An application to autonomous urban driving. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol.\u00a08054, pp. 322\u2013337. Springer, Heidelberg (2013)"},{"key":"44_CR12","doi-asserted-by":"crossref","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory. DIMACS Series, vol.\u00a013, pp. 51\u201373 (1993)","DOI":"10.1090\/dimacs\/013\/04"},{"key":"44_CR13","unstructured":"Draeger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Technical Report CS-RR-14-01, Department of Computer Science, University of Oxford (2014)"},{"issue":"4","key":"44_CR14","first-page":"1","volume":"4","author":"K. Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. LMCS\u00a04(4), 1\u201321 (2008)","journal-title":"LMCS"},{"key":"44_CR15","doi-asserted-by":"crossref","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer (1997)","DOI":"10.1007\/978-1-4612-4054-9"},{"key":"44_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 112\u2013127. Springer, Heidelberg (2011)"},{"key":"44_CR17","first-page":"10","volume-title":"STOC 1976","author":"M.R. Garey","year":"1976","unstructured":"Garey, M.R., Graham, R.L., Johnson, D.S.: Some np-complete geometric problems. In: STOC 1976, pp. 10\u201322. ACM, New York (1976)"},{"issue":"5","key":"44_CR18","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"44_CR19","doi-asserted-by":"crossref","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer (1976)","DOI":"10.1007\/978-1-4684-9455-6"},{"issue":"4","key":"44_CR20","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1109\/9.917660","volume":"46","author":"R. Kumar","year":"2001","unstructured":"Kumar, R., Garg, V.: Control of stochastic discrete event systems modeled by probabilistic languages. IEEE Trans. Automatic Control\u00a046(4), 593\u2013606 (2001)","journal-title":"IEEE Trans. Automatic Control"},{"key":"44_CR21","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Wasniewski, J., Andersson, S., Belta, C.: Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees. In: Proc. ICRA 2010, pp. 3227\u20133232 (2010)","DOI":"10.1109\/ROBOT.2010.5509686"},{"key":"44_CR22","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Results on the quantitative mu-calculus qMu. ACM Transactions on Computational Logic\u00a08(1) (2007)","DOI":"10.1145\/1182613.1182616"},{"key":"44_CR23","doi-asserted-by":"crossref","unstructured":"Ozay, N., Topcu, U., Murray, R., Wongpiromsarn, T.: Distributed synthesis of control protocols for smart camera networks. In: Proc. ICCPS 2011 (2011)","DOI":"10.1109\/ICCPS.2011.22"},{"key":"44_CR24","doi-asserted-by":"crossref","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons (1994)","DOI":"10.1002\/9780470316887"},{"key":"44_CR25","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons (1998)"},{"key":"44_CR26","unstructured":"Shankar, N.: A tool bus for anytime verification. In: Usable Verification (2010)"},{"issue":"1-2","key":"44_CR27","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.tcs.2006.08.042","volume":"367","author":"G. Steel","year":"2006","unstructured":"Steel, G.: Formal analysis of PIN block attacks. TCS\u00a0367(1-2), 257\u2013270 (2006)","journal-title":"TCS"},{"key":"44_CR28","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time Markov models. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 299\u2013314. Springer, Heidelberg (2012); Extended version available as technical report SFB\/TR 14 AVACS 88","DOI":"10.1007\/978-3-642-28756-5_21"},{"key":"44_CR29","unstructured":"http:\/\/www.prismmodelchecker.org\/files\/tacas14pcs\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T12:01:07Z","timestamp":1558872067000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}