{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T23:42:07Z","timestamp":1768347727147,"version":"3.49.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030010898","type":"print"},{"value":"9783030010904","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","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-030-01090-4_11","type":"book-chapter","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T11:23:23Z","timestamp":1538220203000},"page":"177-193","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Temporal Logic Verification of Stochastic Systems Using Barrier Certificates"],"prefix":"10.1007","author":[{"given":"Pushpak","family":"Jagtap","sequence":"first","affiliation":[]},{"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[]},{"given":"Majid","family":"Zamani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,9,30]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., Katoen, J.P., Mereacre, A.: Quantitative automata model checking of autonomous stochastic hybrid systems. In: Proceedings of the 14th International Conference on Hybrid systems: Computation and Control, pp. 83\u201392. ACM (2011)","DOI":"10.1145\/1967701.1967715"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Ayala, A.I.M., Andersson, S.B., Belta, C.: Probabilistic control from time-bounded temporal logic specifications in dynamic environments. In: 2012 IEEE International Conference on Robotics and Automation, pp. 4705\u20134710 (2012)","DOI":"10.1109\/ICRA.2012.6224963"},{"key":"11_CR3","unstructured":"Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT press, Cambridge (2008)"},{"key":"11_CR4","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: International Joint Conference on Artificial Intelligence, vol. 13, pp. 854\u2013860 (2013)"},{"key":"11_CR5","unstructured":"De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: International Joint Conference on Artificial Intelligence, vol. 15, pp. 1558\u20131564 (2015)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Dimitrova, R., Majumdar, R.: Deductive control synthesis for alternating-time logics. In: 2014 International Conference on Embedded Software (EMSOFT), pp. 1\u201310 (2014)","DOI":"10.1145\/2656045.2656054"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"Alexandre Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JG Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89\u2013110. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_5"},{"issue":"5s","key":"11_CR9","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1145\/3126508","volume":"16","author":"C Huang","year":"2017","unstructured":"Huang, C., Chen, X., Lin, W., Yang, Z., Li, X.: Probabilistic safety verification of stochastic hybrid systems using barrier certificates. ACM Trans. Embed. Comput. Syst. 16(5s), 186 (2017)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-66335-7_21","volume-title":"Quantitative Evaluation of Systems","author":"P Jagtap","year":"2017","unstructured":"Jagtap, P., Zamani, M.: QUEST: a tool for state-space quantization-free synthesis of symbolic controllers. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 309\u2013313. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_21"},{"key":"11_CR11","unstructured":"Klein, J., Baier, C.: Experiments with deterministic $$\\omega $$-automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), 182\u2013195 (2006)"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"Orna Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. In: International Conference on Computer Aided Verification, pp. 172\u2013183. Springer, Berlin (1999)"},{"issue":"1","key":"11_CR13","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1073\/pnas.53.1.8","volume":"53","author":"HJ Kushner","year":"1965","unstructured":"Kushner, H.J.: On the stability of stochastic dynamical systems. Proc. Natl. Acad. Sci. 53(1), 8\u201312 (1965)","journal-title":"Proc. Natl. Acad. Sci."},{"issue":"8","key":"11_CR14","doi-asserted-by":"publisher","first-page":"2031","DOI":"10.1109\/TAC.2015.2398883","volume":"60","author":"Morteza Lahijanian","year":"2015","unstructured":"Lahijanian, M., Andersson, S.B., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60(8), 2031\u20132045 (2015)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Lavaei, A., Soudjani, S., Zamani, M.: From dissipativity theory to compositional construction of finite Markov decision processes. In: Hybrid Systems: Computation and Control (HSCC), pp. 21\u201330. ACM, New York (2018)","DOI":"10.1145\/3178126.3178135"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Maity, D., Baras, J.S.: Motion planning in dynamic environments with bounded time temporal logic specifications. In: 2015 23rd Mediterranean Conference on Control and Automation, pp. 940\u2013946 (2015)","DOI":"10.1109\/MED.2015.7158879"},{"issue":"2","key":"11_CR17","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293\u2013320 (2003)","journal-title":"Math. Program."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Postoyan, R., Nesic, D.: Time-triggered control of nonlinear discrete-time systems. In: 2016 IEEE 55th Conference on Decision and Control, pp. 6814\u20136819 (2016)","DOI":"10.1109\/CDC.2016.7799318"},{"issue":"8","key":"11_CR19","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"Stephen Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"11_CR20","unstructured":"Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing SOSTOOLS: a general purpose sum of squares programming solver. In: Proceedings of the 41st IEEE Conference on Decision and Control, vol. 1, pp. 741\u2013746 (2002). http:\/\/www.cds.caltech.edu\/sostools\/"},{"key":"11_CR21","volume-title":"Artificial Intelligence: A Modern Approach","author":"SJ Russell","year":"2003","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Pearson Education, London (2003)","edition":"2"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Saha, I., Ramaithitima, R., Kumar, V., Pappas, G.J., Seshia, S.A.: Automated composition of motion primitives for multi-robot systems from safe LTL specifications. In: 2014 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 1525\u20131532 (2014)","DOI":"10.1109\/IROS.2014.6942758"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-54862-8_45","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Esmaeil Zadeh Soudjani","year":"2014","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Precise approximations of the probability distribution of a Markov process in time: an application to probabilistic invariance. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 547\u2013561. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_45"},{"key":"11_CR24","unstructured":"Soudjani, S., Abate, A., Majumdar, R.: Dynamic Bayesian networks as formal abstractions of structured stochastic processes. In: 26th International Conference on Concurrency Theory, pp. 1\u201314. Dagstuhl Publishing, Madrid (2015)"},{"issue":"2","key":"11_CR25","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"S Soudjani","year":"2013","unstructured":"Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921\u2013956 (2013)","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Soudjani, S., Gevaerts, C., Abate, A.: FAUST$$^2$$: formal abstractions of uncountable-state stochastic processes. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 272\u2013286. Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-46681-0_23"},{"issue":"7","key":"11_CR27","doi-asserted-by":"publisher","first-page":"901","DOI":"10.1177\/0278364912444146","volume":"31","author":"J Steinhardt","year":"2012","unstructured":"Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31(7), 901\u2013923 (2012)","journal-title":"Int. J. Robot. Res."},{"issue":"1-4","key":"11_CR28","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1080\/10556789908805766","volume":"11","author":"Jos F. Sturm","year":"1999","unstructured":"Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim. Methods Softw. 11(1\u20134), 625\u2013653 (1999). http:\/\/sedumi.ie.lehigh.edu\/","journal-title":"Optimization Methods and Software"},{"key":"11_CR29","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-1-4419-0224-5_7","volume-title":"Verification and Control of Hybrid Systems","author":"Paulo Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer Science & Business Media, Berlin (2009)"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 283\u2013292. ACM (2013)","DOI":"10.1145\/2461328.2461372"},{"issue":"1","key":"11_CR31","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/BF02169423","volume":"1","author":"TL Vincent","year":"1991","unstructured":"Vincent, T.L., Yu, J.: Control of a chaotic system. Dyn. Control 1(1), 35\u201352 (1991)","journal-title":"Dyn. Control"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Wisniewski, R., Bujorianu, M.L.: Stochastic safety analysis of stochastic hybrid systems. In: 2017 IEEE 56th Annual Conference on Decision and Control, pp. 2390\u20132395 (2017)","DOI":"10.1109\/CDC.2017.8263999"},{"issue":"11","key":"11_CR33","doi-asserted-by":"publisher","first-page":"3344","DOI":"10.1109\/TAC.2015.2511722","volume":"61","author":"Tichakorn Wongpiromsarn","year":"2016","unstructured":"Wongpiromsarn, T., Topcu, U., Lamperski, A.: Automata theory meets barrier certificates: temporal logic verification of nonlinear systems. IEEE Trans. Autom. Control 61(11), 3344\u20133355 (2016)","journal-title":"IEEE Transactions on Automatic Control"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-01090-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,21]],"date-time":"2025-10-21T14:48:04Z","timestamp":1761058084000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-01090-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030010898","9783030010904"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01090-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}