{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T14:25:05Z","timestamp":1725978305024},"publisher-location":"Cham","reference-count":94,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105741"},{"type":"electronic","value":"9783319105758"}],"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:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_31","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"1111-1147","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Model Checking in Non-Boolean Domains"],"prefix":"10.1007","author":[{"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"31_CR1","first-page":"313","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0313\u2013321. IEEE, Piscataway (1996)"},{"key":"31_CR2","series-title":"LNCS","first-page":"102","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R., Lugiez, D. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a02761, pp.\u00a0102\u2013126. Springer, Heidelberg (2003)"},{"key":"31_CR3","series-title":"LNCS","first-page":"142","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R., Lugiez, D. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a02761, pp.\u00a0142\u2013156. Springer, Heidelberg (2003)"},{"issue":"1","key":"31_CR4","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.tcs.2005.07.033","volume":"345","author":"L. Alfaro de","year":"2005","unstructured":"de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theor. Comput. Sci. 345(1), 139\u2013170 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"31_CR5","first-page":"141","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Henzinger, T.: Concurrent omega-regular games. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0141\u2013154. IEEE, Piscataway (2000)"},{"key":"31_CR6","first-page":"564","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"L. Alfaro de","year":"1998","unstructured":"de Alfaro, L., Henzinger, T., Kupferman, O.: Concurrent reachability games. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0564\u2013575. IEEE, Piscataway (1998)"},{"key":"31_CR7","first-page":"279","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0279\u2013290. IEEE, Piscataway (2001)"},{"key":"31_CR8","series-title":"LNCS","first-page":"536","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: Larsen, K.G., Nielsen, M. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a02154, pp.\u00a0536\u2013550 (2001)"},{"issue":"2","key":"31_CR9","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1016\/j.jcss.2003.07.009","volume":"68","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374\u2013397 (2004)","journal-title":"J. Comput. Syst. Sci."},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Log. Methods Comput. Sci. 4(3) (2008)","DOI":"10.2168\/LMCS-4(3:7)2008"},{"key":"31_CR11","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"31_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T., Kupferman, O., Vardi, M.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01466, pp.\u00a0163\u2013178. Springer, Heidelberg (1998)"},{"key":"31_CR13","series-title":"LNCS","first-page":"1","volume-title":"Hybrid Systems (II)","author":"E. Asarin","year":"1995","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Antsaklis, P., Nerode, A., Kohn, W., Sastry, S. (eds.) Hybrid Systems (II). LNCS, vol.\u00a0999, pp.\u00a01\u201320. Springer, Heidelberg (1995)"},{"issue":"1\u20132","key":"31_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R. Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"31_CR15","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S. Bardin","year":"2008","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf. 10(5), 401\u2013424 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"31_CR16","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1145\/320211.320240","volume":"46","author":"S. Basu","year":"1999","unstructured":"Basu, S.: New results on quantifier elimination over real closed fields and applications to constraint databases. J. ACM 46(4), 537\u2013555 (1999)","journal-title":"J. ACM"},{"key":"31_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"G. Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K., Lime, D.: UPPAAL-Tiga: time for playing games! In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04590, pp.\u00a0121\u2013125. Springer, Heidelberg (2007)"},{"key":"31_CR18","series-title":"LNCS","first-page":"107","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"G. Bhat","year":"1996","unstructured":"Bhat, G., Cleaveland, R.: Efficient local model-checking for fragments of the modal \u03bc$\\mu$-calculus. In: Margaria, T., Steffen, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01055, pp.\u00a0107\u2013126. Springer, Heidelberg (1996)"},{"key":"31_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05643, pp.\u00a0140\u2013156. Springer, Heidelberg (2009)"},{"issue":"3","key":"31_CR20","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R. Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"31_CR21","first-page":"339","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"R. Bod\u00edk","year":"2010","unstructured":"Bod\u00edk, R., Chandra, S., Galenson, J., Kimelman, D., Tung, N., Barman, S., Rodarmor, C.: Programming with angelic nondeterminism. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0339\u2013352. ACM, New York (2010)"},{"key":"31_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a07358, pp.\u00a0652\u2013657. Springer, Heidelberg (2012)"},{"issue":"2","key":"31_CR23","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s10009-011-0206-x","volume":"14","author":"B. Boigelot","year":"2012","unstructured":"Boigelot, B.: Domain-specific regular acceleration. Int. J. Softw. Tools Technol. Transf. 14(2), 193\u2013206 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"31_CR24","series-title":"LNCS","volume-title":"Intl. Joint Conf. on Automated Reasoning (IJCAR)","author":"B. Boigelot","year":"2001","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol.\u00a02083. Springer, Heidelberg (2001)"},{"key":"31_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-540-70844-5_7","volume-title":"Implementation and Applications of Automata (CIAA)","author":"A. Bouajjani","year":"2008","unstructured":"Bouajjani, A., Habermehl, P., Hol\u00edk, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Ibarra, O.H., Ravikumar, B. (eds.) Implementation and Applications of Automata (CIAA). LNCS, vol.\u00a05148, pp.\u00a057\u201367. Springer, Heidelberg (2008)"},{"key":"31_CR26","series-title":"LNCS","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"31_CR27","series-title":"LNCS","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Bouajjani","year":"2002","unstructured":"Bouajjani, A., Touili, T.: Extrapolating tree transformations. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02404. Springer, Heidelberg (2002)"},{"key":"31_CR28","series-title":"LNCS","first-page":"620","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"P. Bouyer","year":"2003","unstructured":"Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol.\u00a02607, pp.\u00a0620\u2013631. Springer, Heidelberg (2003)"},{"issue":"2","key":"31_CR29","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(97)00217-X","volume":"195","author":"J. Bradfield","year":"1998","unstructured":"Bradfield, J.: The modal \u03bc$\\mu$-calculus alternation hierarchy is strict. Theor. Comput. Sci. 195(2), 133\u2013153 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"31_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-48224-5_35","volume-title":"Intl. Colloquium on Automata, Languages and Programming","author":"F. Breugel van","year":"2001","unstructured":"van Breugel, F., Worrel, J.: Towards quantitative verification of probabilistic systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) Intl. Colloquium on Automata, Languages and Programming. LNCS, vol.\u00a02076, pp.\u00a0421\u2013432. Springer, Heidelberg (2001)"},{"issue":"8","key":"31_CR31","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"Trans. Comput."},{"key":"31_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"T. Bultan","year":"1997","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite systems using Presburger arithmetic. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01254, pp.\u00a0400\u2013411. Springer, Heidelberg (1997)"},{"issue":"2","key":"31_CR33","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. Burch","year":"1992","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 1020$10^{20}$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"31_CR34","series-title":"LNCS","first-page":"522","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"D. Bustan","year":"2004","unstructured":"Bustan, D., Kupferman, O., Vardi, M.: A measured collapse of the modal \u03bc$\\mu$-calculus. In: Diekert, V., Habib, M. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol.\u00a02996, pp.\u00a0522\u2013533. Springer, Heidelberg (2004)"},{"key":"31_CR35","series-title":"LNCS","first-page":"66","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"F. Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a03653, pp.\u00a066\u201380. Springer, Heidelberg (2005)"},{"key":"31_CR36","first-page":"121","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"S. Chandra","year":"2011","unstructured":"Chandra, S., Torlak, E., Barman, S., Bod\u00edk, R.: Angelic debugging. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0121\u2013130. ACM, New York (2011)"},{"key":"31_CR37","first-page":"678","volume-title":"Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.: The complexity of quantitative concurrent parity games. In: Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.\u00a0678\u2013687. ACM, New York (2006)"},{"issue":"4","key":"31_CR38","first-page":"28","volume":"12","author":"K. Chatterjee","year":"2011","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.: Qualitative concurrent parity games. Trans. Comput. Log. 12(4), 28 (2011)","journal-title":"Trans. Comput. Log."},{"issue":"4","key":"31_CR39","first-page":"23:1","volume":"11","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.: Quantitative languages. Trans. Comput. Log. 11(4), 23:1\u201323:38 (2010)","journal-title":"Trans. Comput. Log."},{"key":"31_CR40","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"25 Years of Model Checking","author":"K. Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a0107\u2013138. Springer, Heidelberg (2008)"},{"issue":"2","key":"31_CR41","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, T.: A survey of stochastic \u03c9$\\omega$-regular games. J. Comput. Syst. Sci. 78(2), 394\u2013413 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"31_CR42","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Symp. on Principles of Programming Languages (POPL). ACM, New York (1977)"},{"key":"31_CR43","series-title":"LNCS","volume-title":"Programming Language Implementation and Logic Programming (PLILP)","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) Programming Language Implementation and Logic Programming (PLILP). LNCS, vol.\u00a0631. Springer, Heidelberg (1992)"},{"key":"31_CR44","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"Dam, M.: CTL\u2217 and ECTL\u2217 as fragments of the modal \u03bc$\\mu$-calculus. Theor. Comput. Sci. 126, 77\u201396 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"31_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"M. Wulf De","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a017\u201330. Springer, Heidelberg (2006)"},{"key":"31_CR46","series-title":"LNCS","first-page":"63","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Wulf De","year":"2008","unstructured":"De Wulf, M., Doyen, L., Maquet, N., Raskin, J.F.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04963, pp.\u00a063\u201377. Springer, Heidelberg (2008)"},{"key":"31_CR47","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/3-540-48320-9_19","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"J. Desharnais","year":"1999","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov systems. In: Baeten, J.C.M., Mauw, S. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01664, pp.\u00a0258\u2013273. Springer, Heidelberg (1999)"},{"key":"31_CR48","first-page":"413","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"J. Desharnais","year":"2002","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0413\u2013422. IEEE, Piscataway (2002)"},{"key":"31_CR49","doi-asserted-by":"publisher","first-page":"413","DOI":"10.2307\/2370405","volume":"35","author":"L. Dickson","year":"1913","unstructured":"Dickson, L.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am. J. Math. 35, 413\u2013422 (1913)","journal-title":"Am. J. Math."},{"key":"31_CR50","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)"},{"key":"31_CR51","first-page":"5","volume":"1","author":"L. Doyen","year":"2009","unstructured":"Doyen, L., Raskin, J.F.: Antichains for the automata-based approach to model-checking. Log. Methods Comput. Sci. 1, 5 (2009)","journal-title":"Log. Methods Comput. Sci."},{"key":"31_CR52","series-title":"LNCS","first-page":"2","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"L. Doyen","year":"2010","unstructured":"Doyen, L., Raskin, J.F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a06015, pp.\u00a02\u201322. Springer, Heidelberg (2010)"},{"key":"31_CR53","first-page":"368","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"E. Emerson","year":"1991","unstructured":"Emerson, E., Jutla, C.: Tree automata, mu-calculus and determinacy. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0368\u2013377. IEEE, Piscataway (1991)"},{"key":"31_CR54","first-page":"267","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"E. Emerson","year":"1986","unstructured":"Emerson, E., Lei, C.: Efficient model checking in fragments of the propositional \u03bc$\\mu$-calculus. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0267\u2013278. IEEE, Piscataway (1986)"},{"issue":"3","key":"31_CR55","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2008.11.019","volume":"220","author":"M. Faella","year":"2008","unstructured":"Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electron. Notes Theor. Comput. Sci. 220(3), 61\u201377 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"31_CR56","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"E. Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05643, pp.\u00a0263\u2013277. Springer, Heidelberg (2009)"},{"issue":"3","key":"31_CR57","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10703-011-0115-3","volume":"39","author":"E. Filiot","year":"2011","unstructured":"Filiot, E., Jin, N., Raskin, J.F.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261\u2013296 (2011)","journal-title":"Form. Methods Syst. Des."},{"key":"31_CR58","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere. Tech. Rep. LSV-98-4, Laboratoire Sp\u00e9cification et V\u00e9rification (1998)"},{"issue":"3","key":"31_CR59","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G. Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263\u2013279 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"31_CR60","first-page":"62","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Gulwani","year":"2011","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Hall, M.W., Padua, D.A. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a062\u201373. ACM, New York (2011)"},{"key":"31_CR61","first-page":"60","volume-title":"Annual Symp. on the Theory of Computing","author":"Y. Gurevich","year":"1982","unstructured":"Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Lewis, H.R., Simons, B.B., Burkhard, W.A., Landweber, L.H. (eds.) Annual Symp. on the Theory of Computing, pp.\u00a060\u201365. ACM, New York (1982)"},{"key":"31_CR62","first-page":"56","volume-title":"Real-Time Systems Symposium (RTSS)","author":"T. Henzinger","year":"1995","unstructured":"Henzinger, T., Ho, P.H., Wong-Toi, H.: HyTech: the next generation. In: Real-Time Systems Symposium (RTSS), pp.\u00a056\u201365. IEEE, Piscataway (1995)"},{"key":"31_CR63","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/3-540-48320-9_23","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"T. Henzinger","year":"1999","unstructured":"Henzinger, T., Horowitz, B., Majumdar, R.: Rectangular hybrid games. In: Baeten, J., Mauw, S. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01664, pp.\u00a0320\u2013335. Springer, Heidelberg (1999)"},{"key":"31_CR64","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BFb0028745","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"T. Henzinger","year":"1998","unstructured":"Henzinger, T., Kupferman, O., Qadeer, S.: From prehistoric to postmodern symbolic model checking. In: Hu, A., Vardi, M. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01427, pp.\u00a0195\u2013206. Springer, Heidelberg (1998)"},{"issue":"1","key":"31_CR65","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"31_CR66","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1042038.1042039","volume":"6","author":"T.A. Henzinger","year":"2005","unstructured":"Henzinger, T.A., Majumdar, R., Raskin, J.F.: A classification of symbolic transition systems. Trans. Comput. Log. 6(1), 1\u201332 (2005)","journal-title":"Trans. Comput. Log."},{"key":"31_CR67","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"B. Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.A.: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04590, pp.\u00a0258\u2013262. Springer, Heidelberg (2007)"},{"issue":"2","key":"31_CR68","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/j.jcss.2011.05.005","volume":"78","author":"B. Jobstmann","year":"2012","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441\u2013460 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"31_CR69","volume-title":"Classical Descriptive Set Theory","author":"A. Kechris","year":"1994","unstructured":"Kechris, A.: Classical Descriptive Set Theory. Springer, Heidelberg (1994)"},{"key":"31_CR70","first-page":"91","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"R. K\u00f6nighofer","year":"2011","unstructured":"K\u00f6nighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: Bjesse, P., Slobodov\u00e1, A. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a091\u2013100. FMCAD, Austin (2011)"},{"issue":"3","key":"31_CR71","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc$\\mu$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"31_CR72","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1109\/MRA.2011.942116","volume":"18","author":"H. Kress-Gazit","year":"2011","unstructured":"Kress-Gazit, H., Wongpiromsarn, T., Topcu, U.: Correct, reactive robot control from abstraction and temporal logic specifications. Robot. Autom. Mag. 18(3), 65\u201374 (2011)","journal-title":"Robot. Autom. Mag."},{"key":"31_CR73","series-title":"LNCS","first-page":"457","volume-title":"Intl. Symposium on Algorithms and Computation (ISAAC)","author":"S. Kristoffer","year":"2013","unstructured":"Kristoffer, S., Frederiksen, S., Miltersen, P.: Approximating the value of a concurrent reachability game in the polynomial time hierarchy. In: Cai, L., Cheng, S.W., Lam, T. (eds.) Intl. Symposium on Algorithms and Computation (ISAAC). LNCS, vol.\u00a08283, pp.\u00a0457\u2013467. Springer, Heidelberg (2013)"},{"issue":"1\u20132","key":"31_CR74","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"31_CR75","series-title":"LNCS","first-page":"229","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"O. Maler","year":"1995","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol.\u00a0900, pp.\u00a0229\u2013242. Springer, Heidelberg (1995)"},{"key":"31_CR76","doi-asserted-by":"publisher","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"D. Martin","year":"1975","unstructured":"Martin, D.: Borel determinacy. Ann. Math. 102, 363\u2013371 (1975)","journal-title":"Ann. Math."},{"issue":"4","key":"31_CR77","doi-asserted-by":"publisher","first-page":"1565","DOI":"10.2307\/2586667","volume":"63","author":"D. Martin","year":"1998","unstructured":"Martin, D.: The determinacy of Blackwell games. J. Symb. Log. 63(4), 1565\u20131581 (1998)","journal-title":"J. Symb. Log."},{"key":"31_CR78","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State-Explosion Problem","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking: An Approach to the State-Explosion Problem. Kluwer Academic, Norwell (1993)"},{"key":"31_CR79","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"issue":"1","key":"31_CR80","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High.-Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High.-Order Symb. Comput."},{"key":"31_CR81","volume-title":"Theory of Games and Economic Behavior","author":"J. Neumann von","year":"1947","unstructured":"von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1947)"},{"key":"31_CR82","volume-title":"Game Theory","author":"G. Owen","year":"1995","unstructured":"Owen, G.: Game Theory. Academic Press, Cambridge (1995)"},{"key":"31_CR83","first-page":"46","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a046\u201357. IEEE, Piscataway (1977)"},{"key":"31_CR84","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri Nets: An Introduction","author":"W. Reisig","year":"1985","unstructured":"Reisig, W.: Petri Nets: An Introduction. Springer, Heidelberg (1985)"},{"key":"31_CR85","first-page":"281","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"A. Solar-Lezama","year":"2005","unstructured":"Solar-Lezama, A., Rabbah, R., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Sarkar, V., Hall, M.W. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0281\u2013294. ACM, New York (2005)"},{"key":"31_CR86","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1145\/1168857.1168907","volume-title":"Intl. Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"A. Solar-Lezama","year":"2006","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Shen, J.P., Martonosi, M. (eds.) Intl. Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp.\u00a0404\u2013415. ACM, New York (2006)"},{"key":"31_CR87","first-page":"313","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"S. Srivastava","year":"2010","unstructured":"Srivastava, S., Gulwani, S., Foster, J.: From program verification to program synthesis. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0313\u2013326. ACM, New York (2010)"},{"key":"31_CR88","unstructured":"Stockmeyer, L.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, Massachusetts Institute of Technology (1974)"},{"key":"31_CR89","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp.\u00a0133\u2013191. Elsevier, Amsterdam (1990)"},{"key":"31_CR90","series-title":"LNCS","first-page":"1","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"W. Thomas","year":"1995","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol.\u00a0900, pp.\u00a01\u201313. Springer, Heidelberg (1995)"},{"key":"31_CR91","first-page":"327","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"M. Vardi","year":"1985","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state systems. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0327\u2013338. IEEE, Piscataway (1985)"},{"issue":"1","key":"31_CR92","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"31_CR93","series-title":"LNCS","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"P. Wolper","year":"1995","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints (extended abstract). In: Mycroft, A. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a0983. Springer, Heidelberg (1995)"},{"key":"31_CR94","first-page":"4607","volume-title":"Decision and Control","author":"H. Wong-Toi","year":"1997","unstructured":"Wong-Toi, H.: The synthesis of controllers for linear hybrid automata. In: Decision and Control, pp.\u00a04607\u20134612. IEEE, Piscataway (1997)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:20:38Z","timestamp":1526631638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":94,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_31","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}