{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:46:16Z","timestamp":1761597976367,"version":"3.37.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319991535"},{"type":"electronic","value":"9783319991542"}],"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-99154-2_15","type":"book-chapter","created":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T14:14:35Z","timestamp":1534256075000},"page":"240-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Bounded Verification of Reachability of Probabilistic Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Ratan","family":"Lal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavithra","family":"Prabhakar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,15]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-71493-4_4","volume-title":"Hybrid Systems: Computation and Control","author":"A Abate","year":"2007","unstructured":"Abate, A., Amin, S., Prandini, M., Lygeros, J., Sastry, S.: Computational approaches to reachability analysis of stochastic hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 4\u201317. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71493-4_4"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: An approximate dynamic programming approach to probabilistic reachability for stochastic hybrid systems. In: 47th IEEE Conference on Decision and Control, 2008. CDC 2008 (2008)","DOI":"10.1109\/CDC.2008.4739410"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44, 2724\u20132734 (2008)","DOI":"10.1016\/j.automatica.2008.03.027"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11730637_7","volume-title":"Hybrid Systems: Computation and Control","author":"S Amin","year":"2006","unstructured":"Amin, S., Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Reachability analysis for controlled discrete time stochastic hybrid systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 49\u201363. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_7"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: $$\\nu $$ Z - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_14"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Blom, H.A.P., Bakker, G.J., Krystul, J.: Probabilistic reachability analysis for large scale stochastic hybrid systems. In: 2007 46th IEEE Conference on Decision and Control (2007)","DOI":"10.1109\/CDC.2007.4434095"},{"key":"15_CR7","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Forejt, V., Ku\u010dera, A.: Reachability in recursive Markov decision processes. Inf. Comput. 206, 520\u2013537 (2008)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-540-24743-2_16","volume-title":"Hybrid Systems: Computation and Control","author":"ML Bujorianu","year":"2004","unstructured":"Bujorianu, M.L.: Extended stochastic hybrid systems and their reachability problem. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 234\u2013249. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_16"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Bujorianu, M.L., Lygeros, J.: Toward a general theory of stochastic hybrid systems. In: Blom H.A.P., Lygeros J. (eds.) Stochastic Hybrid Systems. LNCS, vol. 337. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11587392_1","DOI":"10.1007\/11587392_1"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"PR D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39\u201356. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44804-7_3"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-78929-1_13","volume-title":"Hybrid Systems: Computation and Control","author":"M Fr\u00e4nzle","year":"2008","unstructured":"Fr\u00e4nzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: a novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172\u2013186. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78929-1_13"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258\u2013273. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_17"},{"key":"15_CR13","unstructured":"Fr\u00e4nzle, M., Herde, C.: Efficient proof engines for bounded model checking of hybrid systems. Electron. Notes Theor. Comput. Sci. 133, 119\u2013137 (2005)"},{"key":"15_CR14","unstructured":"Gilles, A., Marco, B., Alessandro, C., Roberto, S.: Verifying industrial hybrid systems with mathSAT. Electron. Notes Theor. Comput. Sci. 119, 17\u201332 (2005)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-11439-2_10","volume-title":"Reachability Problems","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 125\u2013137. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A..: The theory of hybrid automata. In: Proceedings of the Symposium on Logic in Computer Science (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"15_CR17","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57, 94\u2013124 (1998)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-25141-7_7","volume-title":"Cyber Physical Systems. Design, Modeling, and Evaluation","author":"H Hermanns","year":"2015","unstructured":"Hermanns, H., Kr\u010d\u00e1l, J., Nies, G.: Recharging probably keeps batteries alive. In: Berger, C., Mousavi, M.R. (eds.) CyPhy 2015. LNCS, vol. 9361, pp. 83\u201398. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25141-7_7"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-48983-5_15","volume-title":"Hybrid Systems: Computation and Control","author":"G Lafferriere","year":"1999","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 137\u2013151. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48983-5_15"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: Symposium on Principles of Programming Languages, POPL (2014)","DOI":"10.1145\/2535838.2535857"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Neuhausser, M.R., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: 2010 Seventh International Conference on the Quantitative Evaluation of Systems (QEST) (2010)","DOI":"10.1109\/QEST.2010.47"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-540-31954-2_37","volume-title":"Hybrid Systems: Computation and Control","author":"S Ratschan","year":"2005","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 573\u2013589. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_37"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Rutten, J.J.M.M., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical techniques for analyzing concurrent and probabilistic systems. American Mathematical Society (2004)","DOI":"10.1090\/crmm\/023"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Shmarov, F., Zuliani, P.: Probreach: verified probabilistic delta-reachability for stochastic hybrid systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (2015)","DOI":"10.1145\/2728606.2728625"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J Sproston","year":"2000","unstructured":"Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 31\u201345. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45352-0_5"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Summers, S., Lygeros, J.: Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem. Automatica 46, 1951\u20131961 (2010)","DOI":"10.1016\/j.automatica.2010.08.006"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Wang, Q., Zuliani, P., Kong, S., Gao, S., Clarke, E.M.: Sreach: a probabilistic bounded delta-reachability analyzer for stochastic hybrid systems. In: Proceeding of the Computational Methods in Systems Biology (2015)","DOI":"10.1007\/978-3-319-23401-4_3"},{"key":"15_CR28","unstructured":"Wu, D., Koutsoukos, X.: Reachability analysis of uncertain systems using bounded-parameter Markov decision processes. Artif. Intell. 172, 945\u2013354 (2008)"},{"key":"15_CR29","unstructured":"Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M..: Safety verification for probabilistic hybrid systems. Eur. J. Control 18, 572\u2013587 (2012)"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Zhang, W., Prabhakar, P., Natarajan, B.: Abstraction based reachability analysis for finite branching stochastic hybrid systems. In: ACM\/IEEE International Conference on Cyber-Physical Systems (ICCPS) (2017)","DOI":"10.1145\/3055004.3055023"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99154-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T05:07:05Z","timestamp":1571720825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99154-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319991535","9783319991542"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99154-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}