{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,20]],"date-time":"2024-08-20T13:09:12Z","timestamp":1724159352218},"reference-count":35,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.92.9","type":"journal-article","created":{"date-parts":[[2012,8,15]],"date-time":"2012-08-15T16:04:03Z","timestamp":1345046643000},"page":"122-136","source":"Crossref","is-referenced-by-count":56,"title":["Statistical Model Checking for Stochastic Hybrid Systems"],"prefix":"10.4204","volume":"92","author":[{"given":"Alexandre","family":"David","sequence":"first","affiliation":[{"name":"Aalborg University"}]},{"given":"Dehui","family":"Du","sequence":"additional","affiliation":[{"name":"East China Normal University"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[{"name":"Aalborg University"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[{"name":"INRIA Rennes"}]},{"given":"Marius","family":"Miku\u010dionis","sequence":"additional","affiliation":[{"name":"Aalborg University"}]},{"given":"Danny B\u00f8gsted","family":"Poulsen","sequence":"additional","affiliation":[{"name":"Aalborg University"}]},{"given":"Sean","family":"Sedwards","sequence":"additional","affiliation":[{"name":"INRIA Rennes"}]}],"member":"2720","published-online":{"date-parts":[[2012,8,15]]},"reference":[{"key":"WTA01","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","article-title":"Optimal Paths in Weighted Timed Automata","volume-title":"Hybrid Systems: Computation and Control","volume":"2034","author":"Rajeev Alur","year":"2001"},{"key":"BDDHP11","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1109\/QEST.2011.24","article-title":"COSMOS: A Statistical Model Checker for the Hybrid Automata Stochastic Logic","volume-title":"QEST","author":"Paolo Ballarini","year":"2011"},{"key":"BarkaiLeibler2000","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1038\/35002258","article-title":"Biological rhythms: Circadian clocks limited by noise","volume":"403","author":"Naama Barkai","year":"2000","journal-title":"Nature"},{"key":"BBBCDL10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-13464-7_4","article-title":"Statistical Abstraction and Model-Checking of Large Heterogeneous Systems","volume-title":"FMOODS\/FORTE","volume":"6117","author":"Ananda Basu","year":"2010"},{"issue":"1","key":"DBLP:journals\/sttt\/BasuBBDL12","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10009-011-0201-2","article-title":"Statistical abstraction and model-checking of large heterogeneous systems","volume":"14","author":"Ananda Basu","year":"2012","journal-title":"STTT"},{"key":"BBBDLS10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-16612-9_25","article-title":"Verification of an AFDX Infrastructure Using Simulations and Probabilities","volume-title":"RV","volume":"6418","author":"Ananda Basu","year":"2010"},{"key":"PTA01","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","article-title":"Minimum-Cost Reachability for Priced Timed Automata","volume-title":"HSCC","author":"Gerd Behrmann","year":"2001"},{"key":"BDLLM12","series-title":"EPTCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.78.1","article-title":"Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach","volume-title":"IWIGP","volume":"78","author":"Peter E. Bulychev","year":"2012"},{"key":"MITLSMC","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-28717-6_15","article-title":"Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic","volume-title":"LPAR","volume":"7180","author":"Peter E. Bulychev","year":"2012"},{"key":"CDL10","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10703-009-0076-y","article-title":"On simulation-based probabilistic model checking of mixed-analog circuits","volume":"36","author":"Edmund Clarke","year":"2010","journal-title":"Formal Methods in System Design"},{"key":"chinesepaper","article-title":"An Evaluation Framework for Energy Aware Buildings using Statistical Model Checking","author":"Alexandre David","year":"2012"},{"key":"ourherschel","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-34032-1_28","article-title":"Schedulability of Herschel-Planck Revisited Using Statistical Model Checking","volume-title":"5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation","author":"Alexandre David","year":"2012"},{"key":"ourbio","article-title":"Runtime Verification of Biological Systems","volume-title":"5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation","author":"Alexandre David","year":"2012"},{"key":"DLLMPVW11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","article-title":"Statistical Model Checking for Networks of Priced Timed Automata","volume-title":"FORMATS","author":"Alexandre David","year":"2011"},{"key":"DLLMW11","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","article-title":"Time for statistical model checking of real-time systems","volume-title":"Proceedings of the 23rd international conference on Computer aided verification","author":"Alexandre David","year":"2011"},{"key":"hscc2010","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1145\/1755952.1755967","article-title":"Timed I\/O automata: a complete specification theory for real-time systems","volume-title":"HSCC","author":"Alexandre David","year":"2010"},{"key":"Fehnker04","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","article-title":"Benchmarks for Hybrid Systems Verification","volume-title":"HSCC","volume":"2993","author":"Ansgar Fehnker","year":"2004"},{"key":"Gillespie1977","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","article-title":"Exact Stochastic Simulation of Coupled Chemical Reactions","volume":"81","author":"Daniel T. Gillespie","year":"1977","journal-title":"Journal of Physical Chemistry"},{"key":"gomez09","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-04368-0_15","article-title":"A Compositional Translation of Timed Automata with Deadlines to UPPAAL Timed Automata","volume-title":"Formal Modeling and Analysis of Timed Systems","volume":"5813","author":"Rodolfo G\u00f3mez","year":"2009"},{"key":"GZKFC10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-28067-2_7","article-title":"Computational Modeling and Verification of Signaling Pathways in Cancer","volume-title":"ANB","volume":"6479","author":"Haijun Gong","year":"2010"},{"key":"Jegourel2012","series-title":"LNCS","article-title":"Cross-entropy optimisation of importance sampling parameters for statistical model checking","volume-title":"CAV","author":"Cyrille Jegourel","year":"2012"},{"key":"Sedwards2012","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_37","article-title":"A Platform for High Performance Statistical Model Checking \u2013 PLASMA","volume-title":"TACAS","author":"Cyrille Jegourel","year":"2012"},{"key":"JCLLPZ09","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","article-title":"A Bayesian Approach to Model Checking Biological Systems","volume-title":"CMSB","volume":"5688","author":"Sumit Kumar Jha","year":"2009"},{"issue":"2","key":"KZHHJ11","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","article-title":"The ins and outs of the probabilistic model checker MRMC","volume":"68","author":"Joost-Pieter Katoen","year":"2011","journal-title":"Perform. Eval."},{"issue":"4","key":"MTL","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying Real-Time Properties with Metric Temporal Logic","volume":"2","author":"Ron Koymans","year":"1990","journal-title":"Real-Time Systems"},{"issue":"4","key":"LMPR07","doi-asserted-by":"publisher","DOI":"10.1145\/1276920.1276922","article-title":"Probabilistic abstraction for model checking: An approach based on property testing","volume":"8","author":"S. Laplante","year":"2007","journal-title":"ACM TCS"},{"issue":"1","key":"LS91","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","article-title":"Bisimulation through Probabilistic Testing","volume":"94","author":"Kim Guldstrand Larsen","year":"1991","journal-title":"Inf. Comput."},{"key":"LDB10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","article-title":"Statistical Model Checking: An Overview","volume-title":"RV","volume":"6418","author":"Axel Legay","year":"2010"},{"key":"MPL11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-24559-6_11","article-title":"Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications","volume-title":"ICFEM","volume":"6991","author":"Jo\u00e3o Martins","year":"2011"},{"key":"LTL","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/SFCS.1977.32","article-title":"The Temporal Logic of Programs","volume-title":"FOCS","author":"Amir Pnueli","year":"1977"},{"key":"SVA04","series-title":"LNCS 3114","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/11513988_26","article-title":"Statistical Model Checking of Black-Box Probabilistic Systems","volume-title":"CAV","author":"Koushik Sen","year":"2004"},{"issue":"9","key":"Vilar2002","doi-asserted-by":"publisher","first-page":"5988","DOI":"10.1073\/pnas.092133899","article-title":"Mechanisms of noise-resistance in genetic oscillators","volume":"99","author":"Jos\u00e9 M. G. Vilar","year":"2002","journal-title":"Proceedings of the National Academy of Sciences"},{"key":"YS02","series-title":"LNCS 2404","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","article-title":"Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling","volume-title":"CAV","author":"H\u00e5kan L. S. Younes","year":"2002"},{"key":"ZBC12","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/2185632.2185665","article-title":"Rare-event verification for stochastic hybrid systems","volume-title":"HSCC","author":"Paolo Zuliani","year":"2012"},{"key":"ZPC10","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1145\/1755952.1755987","article-title":"Bayesian statistical model checking with application to Simulink\/Stateflow verification","volume-title":"HSCC","author":"Paolo Zuliani","year":"2010"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T22:53:07Z","timestamp":1497999187000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1208.3856v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,15]]},"references-count":35,"URL":"https:\/\/doi.org\/10.4204\/eptcs.92.9","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,15]]}}}