{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T10:51:56Z","timestamp":1778669516132,"version":"3.51.4"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,12,3]],"date-time":"2016-12-03T00:00:00Z","timestamp":1480723200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["IAPP project AMBI 324432"],"award-info":[{"award-number":["IAPP project AMBI 324432"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007723","name":"Oxford university Press","doi-asserted-by":"crossref","award":["John Fell OUP Research Fund"],"award-info":[{"award-number":["John Fell OUP Research Fund"]}],"id":[{"id":"10.13039\/501100007723","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s00236-016-0287-9","type":"journal-article","created":{"date-parts":[[2016,12,3]],"date-time":"2016-12-03T09:52:00Z","timestamp":1480758720000},"page":"217-242","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Dynamic Bayesian networks for formal verification of structured stochastic processes"],"prefix":"10.1007","volume":"54","author":[{"given":"Sadegh","family":"Esmaeil Zadeh Soudjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,12,3]]},"reference":[{"issue":"10","key":"287_CR1","doi-asserted-by":"crossref","first-page":"1120","DOI":"10.1002\/rnc.2798","volume":"22","author":"A Abate","year":"2012","unstructured":"Abate, A., Hillen, R.C., Wahl, S.A.: Piecewise affine approximation of fluxes and enzyme kinetics from in-vivo $$13c$$ 13 c labeling experiments. Int. J. Robust Nonlinear Control 22(10), 1120\u20131139 (2012). Special Issue on System Identification for Biological Systems","journal-title":"Int. J. Robust Nonlinear Control"},{"key":"287_CR2","doi-asserted-by":"crossref","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"6","author":"A Abate","year":"2010","unstructured":"Abate, A., Katoen, J.-P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 6, 624\u2013641 (2010)","journal-title":"Eur. J. Control"},{"key":"287_CR3","doi-asserted-by":"crossref","unstructured":"Abate, A., Katoen, J.-P., Mereacre, A.: Quantitative automata model checking of autonomous stochastic hybrid systems. In: HSCC, pp. 83\u201392, (2011)","DOI":"10.1145\/1967701.1967715"},{"issue":"11","key":"287_CR4","doi-asserted-by":"crossref","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724\u20132734 (2008)","journal-title":"Automatica"},{"issue":"6","key":"287_CR5","doi-asserted-by":"crossref","first-page":"1607","DOI":"10.1109\/TCBB.2012.126","volume":"9","author":"A Abate","year":"2012","unstructured":"Abate, A., Vincent, S., Dobbe, R., Silletti, A., Master, N., Axelrod, J., Tomlin, C.J.: A mechanical modeling framework for the study of epithelial morphogenesis. IEEE\/ACM Trans. Comput. Biol. Bioinf. 9(6), 1607\u20131620 (2012)","journal-title":"IEEE\/ACM Trans. Comput. Biol. Bioinf."},{"key":"287_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-1027-1","volume-title":"Dynamic Response of Linear Mechanical Systems\u2014Modeling. Analysis and Simulation","author":"J Angeles","year":"2012","unstructured":"Angeles, J.: Dynamic Response of Linear Mechanical Systems\u2014Modeling. Analysis and Simulation. Springer, New York (2012)"},{"key":"287_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"287_CR8","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1109\/TAC.1975.1100984","volume":"20","author":"DP Bertsekas","year":"1975","unstructured":"Bertsekas, D.P.: Convergence of discretization procedures in dynamic programming. IEEE Trans. Autom. Control 20(3), 415\u2013419 (1975)","journal-title":"IEEE Trans. Autom. Control"},{"key":"287_CR9","doi-asserted-by":"crossref","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Higher-order approximations for verification of stochastic hybrid systems. In: ATVA, volume 7561 of LNCS, pp. 416\u2013434. Springer, (2012)","DOI":"10.1007\/978-3-642-33386-6_32"},{"issue":"2","key":"287_CR10","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"S Esmaeil Zadeh Soudjani","year":"2013","unstructured":"Esmaeil Zadeh 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."},{"issue":"2","key":"287_CR11","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1109\/TAC.2013.2273300","volume":"59","author":"S Esmaeil Zadeh Soudjani","year":"2014","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Probabilistic reach-avoid computation for partially-degenerate stochastic processes. IEEE Trans. Autom. Control 59(2), 528\u2013534 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"3","key":"287_CR12","first-page":"1","volume":"11","author":"S Esmaeil Zadeh Soudjani","year":"2015","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Quantitative approximation of the probability distribution of a Markov process by formal abstractions. Logical methods in computer. Science 11(3), 1\u201329 (2015). arXiv:1504.00039","journal-title":"Science"},{"key":"287_CR13","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A., Majumdar, R.: Dynamic Bayesian networks as formal abstractions of structured stochastic processes. In: 26th International Conference on Concurrency Theory (CONCUR\u201915), vol. 42, pp. 169\u2013183, (2015)"},{"key":"287_CR14","unstructured":"Esmaeil Zadeh\u00a0Soudjani, S., Gevaerts, C., Abate, A.: FAUST $$^{2}$$ 2 : formal abstractions of uncountable-state stochastic processes. In: TACAS, volume 9035 of LNCS, pp. 272\u2013286. Springer, (2015)"},{"issue":"20","key":"287_CR15","doi-asserted-by":"crossref","first-page":"5063","DOI":"10.1021\/jp0128832","volume":"106","author":"DT Gillespie","year":"2002","unstructured":"Gillespie, D.T.: The chemical langevin and Fokker\u2013Planck equations for the reversible isomerization reaction. J. Phys. Chem. A 106(20), 5063\u20135071 (2002)","journal-title":"J. Phys. Chem. A"},{"key":"287_CR16","doi-asserted-by":"crossref","unstructured":"Gusrialdi, A., Hirche, S.: Communication topology design for large-scale interconnected systems with time delay. In: American Control Conference, pp. 4508\u20134513, June (2011)","DOI":"10.1109\/ACC.2011.5990947"},{"key":"287_CR17","doi-asserted-by":"crossref","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian approach to model checking biological systems. In: Computational Methods in Systems Biology, volume 5688 of LNCS, pp. 218\u2013234. Springer, (2009)","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"287_CR18","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243\u2013244. IEEE, (2005)","DOI":"10.1109\/QEST.2005.2"},{"key":"287_CR19","volume-title":"Probabilistic Graphical Models: Principles and Techniques\u2013Adaptive Computation and Machine Learning","author":"D Koller","year":"2009","unstructured":"Koller, D., Friedman, N.: Probabilistic Graphical Models: Principles and Techniques\u2013Adaptive Computation and Machine Learning. The MIT Press, Cambridge (2009)"},{"issue":"3","key":"287_CR20","doi-asserted-by":"crossref","first-page":"4794","DOI":"10.1007\/s10958-006-0278-4","volume":"137","author":"LY Kolotilina","year":"2006","unstructured":"Kolotilina, L.Y.: Bounds for the singular values of a matrix involving its sparsity pattern. J. Math. Sci. 137(3), 4794\u20134800 (2006)","journal-title":"J. Math. Sci."},{"issue":"2","key":"287_CR21","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/18.910572","volume":"47","author":"FR Kschischang","year":"2001","unstructured":"Kschischang, F.R., Frey, B.J., Loeliger, H.-A.: Factor graphs and the sum-product algorithm. IEEE Trans. Inf. Theory 47(2), 498\u2013519 (2001)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"287_CR22","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV, volume 6806 of LNCS, pp. 585\u2013591. Springer, (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"287_CR23","unstructured":"Langmead, C.J.: Generalized queries and Bayesian statistical model checking in dynamic Bayesian networks: application to personalized medicine. In: Proceedings of the 8th International Conference on Computational Systems Bioinformatics, pp. 201\u2013212, (2009)"},{"key":"287_CR24","first-page":"122","volume-title":"Statistical Model Checking: an Overview","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, A.: Statistical Model Checking: an Overview, pp. 122\u2013135. Springer, Berlin (2010)"},{"key":"287_CR25","unstructured":"Murphy, K.P.: Dynamic Bayesian networks: representation, inference and learning. PhD thesis, UC Berkeley, Computer Science Division, (2002)"},{"key":"287_CR26","doi-asserted-by":"crossref","unstructured":"Palaniappan, S.K., Thiagarajan, P.S.: Dynamic Bayesian networks: a factored model of probabilistic dynamics. In: ATVA, volume 7561 of LNCS, pp. 17\u201325. Springer, (2012)","DOI":"10.1007\/978-3-642-33386-6_2"},{"key":"287_CR27","volume-title":"Probability, Random Variables, and Stochastic Processes","author":"A Papoulis","year":"1991","unstructured":"Papoulis, A.: Probability, Random Variables, and Stochastic Processes, 3rd edn. McGraw-Hill, New York (1991)","edition":"3"},{"key":"287_CR28","doi-asserted-by":"crossref","unstructured":"Ramponi, F., Chatterjee, D., Summers, S., Lygeros, J.: On the connections between PCTL and dynamic programming. In: HSCC, pp. 253\u2013262, (2010)","DOI":"10.1145\/1755952.1755988"},{"issue":"23","key":"287_CR29","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1016\/j.mcm.2003.06.009","volume":"41","author":"V Sundarapandian","year":"2005","unstructured":"Sundarapandian, V.: Distributed control schemes for large-scale interconnected discrete-time linear systems. Math. Comput. Model. 41(23), 313\u2013319 (2005)","journal-title":"Math. Comput. Model."},{"key":"287_CR30","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: HSCC, pp. 283\u2013292, (2013)","DOI":"10.1145\/2461328.2461372"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0287-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0287-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0287-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T01:11:48Z","timestamp":1498353108000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0287-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,3]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["287"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0287-9","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,3]]}}}