{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T12:03:15Z","timestamp":1702468995807},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,7,21]],"date-time":"2012-07-21T00:00:00Z","timestamp":1342828800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10703-012-0165-1","type":"journal-article","created":{"date-parts":[[2012,7,20]],"date-time":"2012-07-20T23:52:32Z","timestamp":1342828352000},"page":"313-337","source":"Crossref","is-referenced-by-count":13,"title":["On-the-fly verification and optimization of DTA-properties for large Markov chains"],"prefix":"10.1007","volume":"43","author":[{"given":"Linar","family":"Mikeev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin R.","family":"Neuh\u00e4u\u00dfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Spieler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Verena","family":"Wolf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,7,21]]},"reference":[{"issue":"2","key":"165_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"165_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-642-22110-1_8","volume-title":"Proc of 23rd international conference on computer aided verification (CAV\u201911)","author":"A Andreychenko","year":"2011","unstructured":"Andreychenko A, Mikeev L, Spieler D, Wolf V (2011) Parameter identification for Markov models of biochemical reactions. In: Proc of 23rd international conference on computer aided verification (CAV\u201911). LNCS, vol 6806. Springer, Berlin, pp 83\u201398"},{"key":"165_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3038-0","volume-title":"Continuous-time Markov chains: an applications-oriented approach","author":"W Anderson","year":"1991","unstructured":"Anderson W (1991) Continuous-time Markov chains: an applications-oriented approach. Springer, Berlin"},{"key":"165_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-642-19835-9_12","volume-title":"Proc of 17th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201911)","author":"B Barbot","year":"2011","unstructured":"Barbot B, Chen T, Han T, Katoen J-P, Mereacre A (2011) Efficient CTMC model checking of linear real-time objectives. In: Proc of 17th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201911). LNCS, vol 6605. Springer, Berlin, pp 128\u2013142"},{"key":"165_CR5","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier C, Haverkort B, Hermanns H, Katoen J-P (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29:524\u2013541","journal-title":"IEEE Trans Softw Eng"},{"key":"165_CR6","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1038\/35002258","volume":"403","author":"N Barkai","year":"2000","unstructured":"Barkai N, Leibler S (2000) Biological rhythms: Circadian clocks limited by noise. Nature 403:267\u2013268","journal-title":"Nature"},{"key":"165_CR7","series-title":"ENTCS","first-page":"3","volume-title":"Proc 2nd workshop from biology to concurrency and back (FBTC\u201908)","author":"P Ballarini","year":"2009","unstructured":"Ballarini P, Mardare R, Mura I (2009) Analysing biochemical oscillation through probabilistic model checking. In: Proc 2nd workshop from biology to concurrency and back (FBTC\u201908). ENTCS, vol 229. Elsevier, Amsterdam, pp 3\u201319"},{"key":"165_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-7(1:12)2011","volume":"7","author":"T Chen","year":"2011","unstructured":"Chen T, Han T, Katoen J-P, Mereacre A (2011) Model checking of continuous-time Markov chains against timed automata specifications. Log Methods Comput Sci 7:1\u201334","journal-title":"Log Methods Comput Sci"},{"key":"165_CR9","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1109\/TSE.2008.108","volume":"35","author":"S Donatelli","year":"2009","unstructured":"Donatelli S, Haddad S, Sproston J (2009) Model checking timed and stochastic properties with CSL TA . IEEE Trans Softw Eng 35:224\u2013240","journal-title":"IEEE Trans Softw Eng"},{"key":"165_CR10","volume-title":"Numerical linear algebra with applications","author":"T Dayar","year":"2011","unstructured":"Dayar T, Hermanns H, Spieler D, Wolf V (2011) Bounding the equilibrium distribution of Markov population models. In: Numerical linear algebra with applications"},{"issue":"6767","key":"165_CR11","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1038\/35002125","volume":"403","author":"M Elowitz","year":"2000","unstructured":"Elowitz M, Leibler S (2000) A synthetic oscillatory network of transcriptional regulators. Nature 403(6767):335\u2013338","journal-title":"Nature"},{"key":"165_CR12","volume-title":"Performance analysis of communication systems with non-Markovian stochastic Petri nets","author":"R German","year":"2000","unstructured":"German R (2000) Performance analysis of communication systems with non-Markovian stochastic Petri nets. Wiley, New York"},{"key":"165_CR13","volume-title":"Solving ordinary differential equations I: nonstiff problems","author":"E Hairer","year":"2008","unstructured":"Hairer E, Norsett S, Wanner G (2008) Solving ordinary differential equations I: nonstiff problems. Springer, Berlin"},{"key":"165_CR14","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Proc 23rd international conference on computer aided verification (CAV\u201911)","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proc 23rd international conference on computer aided verification (CAV\u201911). LNCS, vol 6806. Springer, Berlin, pp 585\u2013591"},{"issue":"2","key":"165_CR15","doi-asserted-by":"crossref","DOI":"10.1103\/PhysRevE.75.021904","volume":"75","author":"A Loinger","year":"2007","unstructured":"Loinger A, Lipshtat A, Balaban NQ, Biham O (2007) Stochastic simulations of genetic switch systems. Phys Rev E 75(2):021904","journal-title":"Phys Rev E"},{"issue":"6","key":"165_CR16","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1049\/iet-syb.2010.0005","volume":"4","author":"M Mateescu","year":"2010","unstructured":"Mateescu M, Wolf V, Didier F, Henzinger T (2010) Fast adaptive uniformisation of the chemical master equation. IET Syst Biol J 4(6):441\u2013452","journal-title":"IET Syst Biol J"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0165-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0165-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0165-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,1]],"date-time":"2019-07-01T11:24:20Z","timestamp":1561980260000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0165-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,21]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["165"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0165-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,21]]}}}