{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T15:24:22Z","timestamp":1784215462417,"version":"3.55.0"},"reference-count":50,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"10","license":[{"start":{"date-parts":[[2016,10,1]],"date-time":"2016-10-01T00:00:00Z","timestamp":1475280000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"European Commission Marie Curie","award":["MANTRAS 249295"],"award-info":[{"award-number":["MANTRAS 249295"]}]},{"name":"IAPP project AMBI","award":["324432"],"award-info":[{"award-number":["324432"]}]},{"DOI":"10.13039\/501100004789","name":"John Fell OUP Research Fund","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004789","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Automat. Contr."],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1109\/tac.2015.2502781","type":"journal-article","created":{"date-parts":[[2015,11,23]],"date-time":"2015-11-23T14:28:36Z","timestamp":1448288916000},"page":"2861-2876","source":"Crossref","is-referenced-by-count":13,"title":["Formal Verification of Stochastic Max-Plus-Linear Systems"],"prefix":"10.1109","volume":"61","author":[{"given":"Sadegh","family":"Esmaeil Zadeh Soudjani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dieky","family":"Adzkiya","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461378"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_32"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1137\/120871456"},{"key":"ref31","first-page":"59","article-title":"Adaptive gridding for abstraction and verification of stochastic hybrid systems","author":"esmaeil zadeh soudjani","year":"0","journal-title":"Proc 8th Int Conf Quantitative Eval Syst (QEST'11)"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.16.624-641"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2962"},{"key":"ref36","first-page":"3","article-title":"Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: A survey","author":"abate","year":"2014","journal-title":"Electronic Notes Theoret Comput Sci"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461372"},{"key":"ref34","first-page":"169","article-title":"Dynamic Bayesian networks as formal abstractions of structured stochastic processes","volume":"42","author":"esmaeil zadeh soudjani","year":"2015","journal-title":"26th Int Conf Concurrency Theory (CONCUR'15)"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1201\/9781420008548.ch5"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_29"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.03.027"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/9.8644"},{"key":"ref1","first-page":"415","article-title":"Recursive equations and basic properties of timed Petri nets","volume":"1","author":"baccelli","year":"1992","journal-title":"Discrete Event Dynamic Syst Theory Appl"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2013.2273299"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_12"},{"key":"ref21","author":"kurshan","year":"1994","journal-title":"Computer-Aided Verification of Coordinating Processes The Automata-Theoretic Approach"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_11"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2537948"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0007-6"},{"key":"ref50","first-page":"1","article-title":"Quantitative approximation of the probability distribution of a Markov process by formal abstractions","volume":"11","author":"esmaeil zadeh soudjani","year":"2015","journal-title":"Log Meth in Comp Sci"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejor.2010.09.035"},{"key":"ref11","author":"baccelli","year":"1992","journal-title":"Synchronization and Linearity An Algebra for Discrete Event Systems"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942750"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1214\/aoap\/1019487510"},{"key":"ref13","author":"gaubert","year":"2000","journal-title":"Series Expansions of Lyapunov Exponents and Forgetful Monoids"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1214\/EJP.v13-488"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.3182\/20100830-3-DE-4013.00062"},{"key":"ref16","first-page":"1","article-title":"Exact and approximate approaches to the identification of stochastic max-plus-linear systems","author":"farahani","year":"2013","journal-title":"Discrete Event Dynamic Systems Theory and Applications"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/S0024-3795(01)00405-0","article-title":"Interval systems of max-separable linear equations","volume":"340","author":"cechl\u00e1rov\u00e1 and r a cuninghame-green","year":"2002","journal-title":"Linear Algebra Appl"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2005.02.016"},{"key":"ref19","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/j.laa.2005.02.011","article-title":"Interval systems of max-separable linear equations","volume":"403","author":"myscaron kov\u00e1","year":"2005","journal-title":"Linear Algebra Appl"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2005.1582196"},{"key":"ref3","author":"heidergott","year":"2006","journal-title":"Max Plus at Work-Modeling and Analysis of Synchronized Systems A Course on Max-Plus Algebra and Its Applications"},{"key":"ref6","author":"heidergott","year":"2006","journal-title":"Max-Plus Linear Stochastic Systems and Perturbation Analysis (The International Series on Discrete Event Dynamic Systems)"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2006.377701"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0304-4149(90)90091-6"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/9.50340"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_45"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2006.382515"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1016\/j.trb.2006.02.003"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10696-0_7"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_23"},{"key":"ref47","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2298143"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0195-3"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2005.2"},{"key":"ref43","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","article-title":"PRISM 4.0: Verification of probabilistic real-time systems","volume":"6806","author":"kwiatkowska","year":"2011","journal-title":"Proc 23rd Int Conf Computer Aided Verification (CAV'11)"}],"container-title":["IEEE Transactions on Automatic Control"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9\/7575613\/07335578.pdf?arnumber=7335578","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T11:45:54Z","timestamp":1641987954000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7335578\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10]]},"references-count":50,"journal-issue":{"issue":"10"},"URL":"https:\/\/doi.org\/10.1109\/tac.2015.2502781","relation":{},"ISSN":["0018-9286","1558-2523"],"issn-type":[{"value":"0018-9286","type":"print"},{"value":"1558-2523","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10]]}}}