{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T06:10:05Z","timestamp":1746511805927,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":106,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662454886"},{"type":"electronic","value":"9783662454893"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45489-3_1","type":"book-chapter","created":{"date-parts":[[2014,11,3]],"date-time":"2014-11-03T10:42:42Z","timestamp":1415011362000},"page":"1-25","source":"Crossref","is-referenced-by-count":2,"title":["Analyzing Oscillatory Behavior with Formal Methods"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Andreychenko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thilo","family":"Kr\u00fcger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Spieler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-73368-3_38","volume-title":"Computer Aided Verification","author":"L. Alfaro de","year":"2007","unstructured":"de Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 325\u2013338. Springer, Heidelberg (2007)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Alfonsi, A., Canc\u00e8s, E., Turinici, G., Di Ventura, B., Huisinga, W.: Exact simulation of hybrid stochastic and deterministic models for biochemical systems. Research Report RR-5435, INRIA (2004)","DOI":"10.1051\/proc:2005001"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Alfonsi, A., Canc\u00e8s, E., Turinici, G., Ventura, B.D., Huisinga, W.: Adaptive simulation of hybrid stochastic and deterministic models for biochemical systems. ESAIM: Proc., 14:1\u201314:13 (2005)","DOI":"10.1051\/proc:2005001"},{"issue":"2","key":"1_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/BF00282276","volume":"19","author":"R. Aris","year":"1965","unstructured":"Aris, R.: Prolegomena to the rational analysis of systems of chemical reactions. Archive for Rational Mechanics and Analysis\u00a019, 81\u201399 (1965)","journal-title":"Archive for Rational Mechanics and Analysis"},{"issue":"4","key":"1_CR6","doi-asserted-by":"crossref","first-page":"1633","DOI":"10.1093\/genetics\/149.4.1633","volume":"149","author":"A. Arkin","year":"1998","unstructured":"Arkin, A., Ross, J., McAdams, H.H.: Stochastic kinetic analysis of developmental pathway bifurcation in phage lambda-infected escherichia coli cells. Genetics\u00a0149(4), 1633\u20131648 (1998)","journal-title":"Genetics"},{"issue":"3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1287\/ijoc.1090.0357","volume":"22","author":"M. Arns","year":"2009","unstructured":"Arns, M., Buchholz, P., Panchenko, A.: On the numerical analysis of inhomogeneous continuous-time Markov chains. INFORMS Journal on Computing\u00a022(3), 416\u2013432 (2009)","journal-title":"INFORMS Journal on Computing"},{"issue":"6","key":"1_CR8","doi-asserted-by":"publisher","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.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR9","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press (2008)"},{"issue":"4","key":"1_CR10","doi-asserted-by":"publisher","first-page":"1925","DOI":"10.1214\/105051606000000420","volume":"16","author":"K. Ball","year":"2006","unstructured":"Ball, K., Kurtz, T.G., Popovic, L., Rempala, G.: Asymptotic analysis of multiscale approximations to reaction networks. The Annals of Applied Probability\u00a016(4), 1925\u20131961 (2006)","journal-title":"The Annals of Applied Probability"},{"issue":"20","key":"1_CR11","doi-asserted-by":"publisher","first-page":"2019","DOI":"10.1016\/j.tcs.2010.02.010","volume":"411","author":"P. Ballarini","year":"2010","unstructured":"Ballarini, P., Guerriero, M.L.: Query-based verification of qualitative trends and oscillations in biochemical systems. Theoretical Computer Science\u00a0411(20), 2019\u20132036 (2010)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"1_CR12","first-page":"3","volume":"229","author":"P. Ballarini","year":"2009","unstructured":"Ballarini, P., Mardare, R., Mura, I.: Analysing biochemical oscillation through probabilistic model checking. ENTCS\u00a0229(1), 3\u201319 (2009)","journal-title":"ENTCS"},{"key":"1_CR13","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1038\/35002258","volume":"403","author":"N. Barkai","year":"2000","unstructured":"Barkai, N., Leibler, S.: Biological rhythms: Circadian clocks limited by noise. Nature\u00a0403, 267\u2013268 (2000)","journal-title":"Nature"},{"issue":"1","key":"1_CR14","first-page":"41","volume":"229","author":"E. Bartocci","year":"2009","unstructured":"Bartocci, E., Corradini, F., Merelli, E., Tesei, L.: Model checking biological oscillators. ENTCS\u00a0229(1), 41\u201358 (2009)","journal-title":"ENTCS"},{"key":"1_CR15","first-page":"21","volume-title":"Markov Anniversary Meeting 2006: An International Conference to Celebrate the 150th Anniversary of the Birth of A. A. Markov","author":"K. Burrage","year":"2006","unstructured":"Burrage, K., Hegland, M., Macnamara, S., Sidje, R.: A Krylov-based finite state projection algorithm for solving the chemical master equation arising in the discrete modeling of biological systems. In: Langville, A.N., Stewart, W.J. (eds.) Markov Anniversary Meeting 2006: An International Conference to Celebrate the 150th Anniversary of the Birth of A. A. Markov, pp. 21\u201338. Boston Books, Charleston (2006)"},{"key":"1_CR16","first-page":"82","volume-title":"Advances in Scientific Computing and Applications","author":"K. Burrage","year":"2004","unstructured":"Burrage, K., Tian, T.: Poisson Runge-Kutta methods for chemical reaction systems. In: Lu, Y., Sun, W., Tang, T. (eds.) Advances in Scientific Computing and Applications, pp. 82\u201396. Science Press, Beijing (2004)"},{"issue":"2-3","key":"1_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/j.pbiomolbio.2004.01.014","volume":"85","author":"K. Burrage","year":"2004","unstructured":"Burrage, K., Tian, T., Burrage, P.: A multi-scaled approach for simulating chemical reaction systems. Progress in Biophysics and Molecular Biology\u00a085(2-3), 217\u2013234 (2004)","journal-title":"Progress in Biophysics and Molecular Biology"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Cao, Y., Gillespie, D.T., Petzold, L.R.: The slow-scale stochastic simulation algorithm. The Journal of Chemical Physics\u00a0122(1), 014116 (2005)","DOI":"10.1063\/1.1824902"},{"key":"1_CR19","unstructured":"Cardelli, L.: Artificial biochemistry. Technical report, Microsoft Research (2006)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Cardelli, L.: Artificial biochemistry. In: Algorithmic Bioproceses. LNCS. Springer (2008)","DOI":"10.1007\/978-3-540-88869-7_22"},{"key":"1_CR21","first-page":"61","volume-title":"Proceedings of the First International Conference on Algebraic Biology","author":"A. Casagrande","year":"2005","unstructured":"Casagrande, A., Mysore, V., Piazza, C., Mishra, B.: Independent dynamics hybrid automata in systems biology. In: Proceedings of the First International Conference on Algebraic Biology, pp. 61\u201373. Universal Academy Press, Tokyo (2005)"},{"key":"1_CR22","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2004.03.063","volume":"325","author":"N. Chabrier-Rivier","year":"2003","unstructured":"Chabrier-Rivier, N., Chiaverini, M., Danos, V., Fages, F., Sch\u00e4chter, V.: Modeling and querying biomolecular interaction networks. Theoretical Computer Science\u00a0325, 25\u201344 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"1_CR23","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1109\/MCS.2009.932926","volume":"29","author":"V. Chellaboina","year":"2009","unstructured":"Chellaboina, V., Bhat, S., Haddad, W., Bernstein, D.: Modeling and analysis of mass-action kinetics. IEEE Control Systems Magazine\u00a029(4), 60\u201378 (2009)","journal-title":"IEEE Control Systems Magazine"},{"key":"1_CR24","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logic of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, pp. 52\u201371. Springer, London (1982)"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Cloth, L., Katoen, J.-P., Khattri, M., Pulungan, R.: Model-checking Markov reward models with impulse rewards. In: DSN, Yokohama (2005)","DOI":"10.1109\/QEST.2005.2"},{"issue":"1","key":"1_CR26","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1186\/1752-0509-3-89","volume":"3","author":"A. Crudu","year":"2009","unstructured":"Crudu, A., Debussche, A., Radulescu, O.: Hybrid stochastic simplifications for multiscale gene networks. BMC Systems Biology\u00a03(1), 89 (2009)","journal-title":"BMC Systems Biology"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol.\u00a02165, pp. 39\u201356. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44804-7_3"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Dayar, T., Mikeev, L., Wolf, V.: On the numerical analysis of stochastic Lotka-Volterra models. In: IMCSIT, pp. 289\u2013296 (2010)","DOI":"10.1109\/IMCSIT.2010.5680059"},{"issue":"1","key":"1_CR29","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1089\/10665270252833208","volume":"9","author":"H. Jong de","year":"2002","unstructured":"de Jong, H.: Modeling and simulation of genetic regulatory systems: A literature review. Journal of Computational Biology\u00a09(1), 67\u2013103 (2002)","journal-title":"Journal of Computational Biology"},{"key":"1_CR30","first-page":"118","volume-title":"Proc., HIBI 2009","author":"F. Didier","year":"2009","unstructured":"Didier, F., Henzinger, T.A., Mateescu, M., Wolf, V.: Fast adaptive uniformization of the chemical master equation. In: Proc., HIBI 2009, pp. 118\u2013127. IEEE Computer Society, Washington, DC (2009)"},{"issue":"5584","key":"1_CR31","doi-asserted-by":"publisher","first-page":"1183","DOI":"10.1126\/science.1070919","volume":"297","author":"M.B. Elowitz","year":"2002","unstructured":"Elowitz, M.B.: Stochastic gene expression in a single cell. Science\u00a0297(5584), 1183\u20131186 (2002)","journal-title":"Science"},{"issue":"6767","key":"1_CR32","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1038\/35002125","volume":"403","author":"M.B. Elowitz","year":"2000","unstructured":"Elowitz, M.B., Leibler, S.: A synthetic oscillatory network of transcriptional regulators. Nature\u00a0403(6767), 335\u2013338 (2000)","journal-title":"Nature"},{"issue":"6","key":"1_CR33","doi-asserted-by":"publisher","first-page":"874","DOI":"10.1016\/j.cell.2011.03.006","volume":"144","author":"J.E. Ferrell","year":"2011","unstructured":"Ferrell, J.E., Tsai, T.Y.-C., Yang, Q.: Modeling the cell cycle: Why do certain circuits oscillate? Cell\u00a0144(6), 874\u2013885 (2011)","journal-title":"Cell"},{"issue":"6767","key":"1_CR34","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1038\/35002131","volume":"403","author":"T.S. Gardner","year":"2000","unstructured":"Gardner, T.S., Cantor, C.R., Collins, J.J.: Construction of a genetic toggle switch in Escherichia coli. Nature\u00a0403(6767), 339\u2013342 (2000)","journal-title":"Nature"},{"issue":"9","key":"1_CR35","doi-asserted-by":"publisher","first-page":"1876","DOI":"10.1021\/jp993732q","volume":"104","author":"M.A. Gibson","year":"2000","unstructured":"Gibson, M.A., Bruck, J.: Efficient exact stochastic simulation of chemical systems with many species and many channels. The Journal of Physical Chemistry A\u00a0104(9), 1876\u20131889 (2000)","journal-title":"The Journal of Physical Chemistry A"},{"issue":"4","key":"1_CR36","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/0021-9991(76)90041-3","volume":"22","author":"D.T. Gillespie","year":"1976","unstructured":"Gillespie, D.T.: A general method for numerically simulating the stochastic time evolution of coupled chemical reactions. Journal of Computational Physics\u00a022(4), 403\u2013434 (1976)","journal-title":"Journal of Computational Physics"},{"issue":"25","key":"1_CR37","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"D.T. Gillespie","year":"1977","unstructured":"Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. The Journal of Physical Chemistry\u00a081(25), 2340\u20132361 (1977)","journal-title":"The Journal of Physical Chemistry"},{"key":"1_CR38","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1016\/0378-4371(92)90283-V","volume":"188","author":"D.T. Gillespie","year":"1992","unstructured":"Gillespie, D.T.: A rigorous derivation of the chemical master equation. Physica A\u00a0188, 404\u2013425 (1992)","journal-title":"Physica A"},{"issue":"4","key":"1_CR39","doi-asserted-by":"publisher","first-page":"1716","DOI":"10.1063\/1.1378322","volume":"115","author":"D.T. Gillespie","year":"2001","unstructured":"Gillespie, D.T.: Approximate accelerated stochastic simulation of chemically reacting systems. The Journal of Chemical Physics\u00a0115(4), 1716 (2001)","journal-title":"The Journal of Chemical Physics"},{"issue":"1-2","key":"1_CR40","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/0025-5564(88)90060-0","volume":"90","author":"L. Glass","year":"1988","unstructured":"Glass, L., Beuter, A., Larocque, D.: Time delays, oscillations, and chaos in physiological control systems. Mathematical Biosciences\u00a090(1-2), 111\u2013125 (1988)","journal-title":"Mathematical Biosciences"},{"issue":"1362","key":"1_CR41","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1098\/rspb.1995.0153","volume":"261","author":"A. Goldbeter","year":"1995","unstructured":"Goldbeter, A.: A model for circadian oscillations in the drosophila period protein (PER). Proceedings of the Royal Society B: Biological Sciences\u00a0261(1362), 319\u2013324 (1995)","journal-title":"Proceedings of the Royal Society B: Biological Sciences"},{"issue":"6912","key":"1_CR42","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1038\/nature01259","volume":"420","author":"A. Goldbeter","year":"2002","unstructured":"Goldbeter, A.: Computational approaches to cellular rhythms. Nature\u00a0420(6912), 238\u2013245 (2002)","journal-title":"Nature"},{"issue":"4","key":"1_CR43","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1023\/A:1021286607354","volume":"28","author":"D. Gonze","year":"2002","unstructured":"Gonze, D., Halloy, J., Goldbeter, A.: Deterministic versus stochastic models for circadian rhythms. Journal of Biological Physics\u00a028(4), 637\u2013653 (2002)","journal-title":"Journal of Biological Physics"},{"key":"1_CR44","unstructured":"Grassmann, W.: Finding transient solutions in Markovian event systems through randomization. In: The First International Conference on the Numerical Solution of Markov Chains, pp. 375\u2013385 (1990)"},{"issue":"22","key":"1_CR45","doi-asserted-by":"publisher","first-page":"2782","DOI":"10.1093\/bioinformatics\/btl465","volume":"22","author":"M. Griffith","year":"2006","unstructured":"Griffith, M., Courtney, T., Peccoud, J., Sanders, W.H.: Dynamic partitioning for hybrid simulation of the bistable HIV-1 transactivation network. Bioinformatics\u00a022(22), 2782\u20132789 (2006)","journal-title":"Bioinformatics"},{"issue":"2","key":"1_CR46","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1287\/opre.32.2.343","volume":"32","author":"D. Gross","year":"1984","unstructured":"Gross, D., Miller, D.R.: The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research\u00a032(2), 343\u2013361 (1984)","journal-title":"Operations Research"},{"key":"1_CR47","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/B978-0-12-381270-4.00008-1","volume":"487","author":"M.L. Guerriero","year":"2011","unstructured":"Guerriero, M.L., Heath, J.K.: Computational modeling of biological pathways by executable biology. Methods in Enzymology\u00a0487, 217\u2013251 (2011)","journal-title":"Methods in Enzymology"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-02658-4_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2009","unstructured":"Henzinger, T.A., Mateescu, M., Wolf, V.: Sliding window abstraction for infinite Markov chains. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 337\u2013352. Springer, Heidelberg (2009)"},{"key":"1_CR49","first-page":"55","volume-title":"Proc., CMSB 2010","author":"T.A. Henzinger","year":"2010","unstructured":"Henzinger, T.A., Mikeev, L., Mateescu, M., Wolf, V.: Hybrid numerical solution of the chemical master equation. In: Proc., CMSB 2010, pp. 55\u201365. ACM, New York (2010)"},{"key":"1_CR50","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1021\/ie50689a006","volume":"59","author":"J. Higgins","year":"1967","unstructured":"Higgins, J.: The theory of oscillating reactions. Industrial and Engineering Chemistry\u00a059, 18\u201362 (1967)","journal-title":"Industrial and Engineering Chemistry"},{"key":"1_CR51","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/BF00251225","volume":"47","author":"F. Horn","year":"1972","unstructured":"Horn, F., Jackson, R.: General mass action kinetics. ARMA\u00a047, 81\u2013116 (1972)","journal-title":"ARMA"},{"issue":"1","key":"1_CR52","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/S0377-2217(97)00028-3","volume":"105","author":"G. Horton","year":"1998","unstructured":"Horton, G., Kulkarni, V.G., Nicol, D.M., Trivedi, K.S.: Fluid stochastic Petri nets: Theory, applications, and solution techniques. European Journal of Operational Research\u00a0105(1), 184\u2013201 (1998)","journal-title":"European Journal of Operational Research"},{"issue":"1.2","key":"1_CR53","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1049\/iet-stb:20070001","volume":"1","author":"J. Lohmueller","year":"2007","unstructured":"Lohmueller, J., et al.: Progress toward construction and modelling of a tri-stable toggle switch in e. coli. IET Synthetic Biology\u00a01(1.2), 25\u201328 (2007)","journal-title":"IET Synthetic Biology"},{"issue":"1","key":"1_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00285-006-0034-x","volume":"54","author":"T. Jahnke","year":"2006","unstructured":"Jahnke, T., Huisinga, W.: Solving the chemical master equation for monomolecular reaction systems analytically. Journal of Mathematical Biology\u00a054(1), 1\u201326 (2006)","journal-title":"Journal of Mathematical Biology"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Jensen, A.: Markoff chains as an aid in the study of Markoff processes. Scandinavian Actuarial Journal 1953(suppl. 1), 87\u201391 (1953)","DOI":"10.1080\/03461238.1953.10419459"},{"key":"1_CR56","unstructured":"Kampen, N.V.: Stochastic processes in physics and chemistry. North Holland (2007)"},{"key":"1_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-73368-3_37","volume-title":"Computer Aided Verification","author":"J.-P. Katoen","year":"2007","unstructured":"Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 311\u2013324. Springer, Heidelberg (2007)"},{"key":"1_CR58","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BF01457949","volume":"104","author":"A. Kolmogoroff","year":"1931","unstructured":"Kolmogoroff, A.: \u00dcber die analytischen Methoden in der Wahrscheinlichkeitsrechnung. Mathematische Annalen\u00a0104, 415\u2013458 (1931)","journal-title":"Mathematische Annalen"},{"issue":"1","key":"1_CR59","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1076\/1387-3954(200003)6:1;1-Q;FT051","volume":"6","author":"S. Kowalewski","year":"2000","unstructured":"Kowalewski, S., Engell, S., Stursberg, O.: On the generation of timed discrete approximations for continuous systems. MCMDS\u00a06(1), 51\u201370 (2000)","journal-title":"MCMDS"},{"issue":"29","key":"1_CR60","doi-asserted-by":"publisher","first-page":"10840","DOI":"10.1073\/pnas.0604085103","volume":"103","author":"S. Krishna","year":"2006","unstructured":"Krishna, S.: Minimal model of spiky oscillations in NF-\u03bab signaling. PNAS\u00a0103(29), 10840\u201310845 (2006)","journal-title":"PNAS"},{"issue":"3","key":"1_CR61","doi-asserted-by":"publisher","first-page":"1603","DOI":"10.1529\/biophysj.104.057216","volume":"89","author":"U. Kummer","year":"2005","unstructured":"Kummer, U., Krajnc, B., Pahle, J., Green, A.K., Dixon, C.J., Marhl, M.: Transition from stochastic to deterministic behavior in calcium oscillations. Biophysical Journal\u00a089(3), 1603\u20131611 (2005)","journal-title":"Biophysical Journal"},{"issue":"7","key":"1_CR62","doi-asserted-by":"publisher","first-page":"2976","DOI":"10.1063\/1.1678692","volume":"57","author":"T.G. Kurtz","year":"1972","unstructured":"Kurtz, T.G.: The Relationship between Stochastic and Deterministic Models for Chemical Reactions. The Journal of Chemical Physics\u00a057(7), 2976\u20132978 (1972)","journal-title":"The Journal of Chemical Physics"},{"key":"1_CR63","unstructured":"Kwiatkowska, M., Norman, G., Pacheco, A.: Model checking expected time and expected reward formulae with random time bounds. In: Proc. 2nd Euro-Japanese Workshop on Stochastic Risk Modelling for Finance, Insurance, Production and Reliability (2002)"},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: Proc. QEST, pp. 157\u2013166. IEEE CS Press (2006)","DOI":"10.1109\/QEST.2006.19"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"Lapin, M., Mikeev, L., Wolf, V.: SHAVE \u2013 Stochastic hybrid analysis of Markov population models. In: Proc. HSCC. ACM, New York (2011)","DOI":"10.1145\/1967701.1967746"},{"issue":"12","key":"1_CR67","doi-asserted-by":"publisher","first-page":"7051","DOI":"10.1073\/pnas.1132112100","volume":"100","author":"J.C. Leloup","year":"2003","unstructured":"Leloup, J.C.: Toward a detailed computational model for the mammalian circadian clock. PNAS\u00a0100(12), 7051\u20137056 (2003)","journal-title":"PNAS"},{"issue":"6","key":"1_CR68","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1177\/074873099129000948","volume":"14","author":"J.C. Leloup","year":"1999","unstructured":"Leloup, J.C., Gonze, D., Goldbeter, A.: Limit cycle models for circadian rhythms based on transcriptional regulation in drosophila and neurospora. Journal of Biological Rhythms\u00a014(6), 433\u2013448 (1999)","journal-title":"Journal of Biological Rhythms"},{"issue":"16","key":"1_CR69","doi-asserted-by":"publisher","first-page":"1398","DOI":"10.1016\/S0960-9822(03)00534-7","volume":"13","author":"J. Lewis","year":"2003","unstructured":"Lewis, J.: Autoinhibition with transcriptional delay: A simple mechanism for the zebrafish somitogenesis oscillator. Current Biology\u00a013(16), 1398\u20131408 (2003)","journal-title":"Current Biology"},{"key":"#cr-split#-1_CR70.1","unstructured":"Lotka, A.: Elements of mathematical biology. Dover Publications (1956)"},{"key":"#cr-split#-1_CR70.2","unstructured":"Reprinted from Lotka, A.J. Elements of physical biology (1924)"},{"key":"1_CR71","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-68413-8_6","volume-title":"Formal Methods in Systems Biology","author":"O. Maler","year":"2008","unstructured":"Maler, O., Batt, G.: Approximating continuous systems by timed automata. In: Fisher, J. (ed.) FMSB 2008. LNCS (LNBI), vol.\u00a05054, pp. 77\u201389. Springer, Heidelberg (2008)"},{"issue":"5","key":"1_CR72","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1016\/S0006-3495(87)83275-7","volume":"52","author":"J.-L. Martiel","year":"1987","unstructured":"Martiel, J.-L., Goldbeter, A.: A model based on receptor desensitization for cyclic AMP signaling in dictyostelium cells. Biophysical Journal\u00a052(5), 807\u2013828 (1987)","journal-title":"Biophysical Journal"},{"key":"1_CR73","unstructured":"MATLAB. Version 7.11.0.584 (R2010b). The MathWorks Inc., Natick, Massachusetts (2010)"},{"issue":"3","key":"1_CR74","doi-asserted-by":"publisher","first-page":"814","DOI":"10.1073\/pnas.94.3.814","volume":"94","author":"H.H. McAdams","year":"1997","unstructured":"McAdams, H.H., Arkin, A.: Stochastic mechanisms in gene expression. Proceedings of the National Academy of Sciences of the United States of America\u00a094(3), 814\u2013819 (1997)","journal-title":"Proceedings of the National Academy of Sciences of the United States of America"},{"issue":"4","key":"1_CR75","doi-asserted-by":"publisher","first-page":"1232","DOI":"10.1137\/110825716","volume":"10","author":"S. Menz","year":"2012","unstructured":"Menz, S., Latorre, J.C., Schtte, C., Huisinga, W.: Hybrid stochastic\u2013deterministic solution of the chemical master equation. MMS\u00a010(4), 1232\u20131262 (2012)","journal-title":"MMS"},{"issue":"24","key":"1_CR76","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1016\/j.ecolmodel.2007.07.001","volume":"209","author":"K.M. Meyer","year":"2007","unstructured":"Meyer, K.M., Wiegand, K., Ward, D., Moustakas, A.: SATCHMO: A spatial simulation model of growth, competition, and mortality in cycling savanna patches. Ecological Modelling\u00a0209(24), 377\u2013391 (2007)","journal-title":"Ecological Modelling"},{"key":"1_CR77","doi-asserted-by":"crossref","unstructured":"Mikeev, L., Neuh\u00e4u\u00dfer, M.R., Spieler, D., Wolf, V.: On-the-fly verification and optimization of DTA-properties for large Markov chains. FMSD, 1\u201325 (2012)","DOI":"10.1007\/s10703-012-0165-1"},{"issue":"5","key":"1_CR78","doi-asserted-by":"publisher","first-page":"1111","DOI":"10.1007\/s10910-011-9955-8","volume":"50","author":"M. Mincheva","year":"2011","unstructured":"Mincheva, M.: Oscillations in non-mass action kinetics models of biochemical reaction networks arising from pairs of subnetworks. Journal of Mathematical Chemistry\u00a050(5), 1111\u20131125 (2011)","journal-title":"Journal of Mathematical Chemistry"},{"key":"1_CR79","unstructured":"van Moorsel, A.P.A., Wolter, K.: Numerical solution of non-homogeneous Markov processes through uniformization. In: Proceedings of the 12th European Simulation Multiconference on Simulation - Past, Present and Future, pp. 710\u2013717. SCS Europe (1998)"},{"key":"1_CR80","doi-asserted-by":"crossref","unstructured":"Munsky, B., Khammash, M.: The finite state projection algorithm for the solution of the chemical master equation. The Journal of Chemical Physics\u00a0124(4), 044104 (2006)","DOI":"10.1063\/1.2145882"},{"key":"1_CR81","doi-asserted-by":"publisher","DOI":"10.1007\/b98869","volume-title":"Mathematical Biology","author":"J.D. Murray","year":"1993","unstructured":"Murray, J.D.: Mathematical Biology. Springer, New York (1993)"},{"key":"1_CR82","unstructured":"Nakano, S., Yamaguchi, S.: Two modeling methods for signaling pathways with multiple signals using uppaal. Proc. BioPPN, 87\u2013101 (2011)"},{"key":"1_CR83","unstructured":"Parker, D.: PRISM Tutorial - Circadian Clock, http:\/\/www.prismmodelchecker.org\/tutorial\/circadian.php"},{"key":"1_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/11513988_3","volume-title":"Computer Aided Verification","author":"C. Piazza","year":"2005","unstructured":"Piazza, C., Antoniotti, M., Mysore, V., Policriti, A., Winkler, F., Mishra, B.: Algorithmic algebraic model checking I: Challenges from systems biology. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 5\u201319. Springer, Heidelberg (2005)"},{"key":"1_CR85","first-page":"46","volume-title":"Proc., SFCS","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc., SFCS, pp. 46\u201357. IEEE Computer Society, Washington, DC (1977)"},{"issue":"11","key":"1_CR86","doi-asserted-by":"publisher","first-page":"4999","DOI":"10.1063\/1.1545446","volume":"118","author":"C.V. Rao","year":"2003","unstructured":"Rao, C.V., Arkin, A.P.: Stochastic chemical kinetics and the quasi-steady-state assumption: Application to the Gillespie algorithm. The Journal of Chemical Physics\u00a0118(11), 4999 (2003)","journal-title":"The Journal of Chemical Physics"},{"issue":"6901","key":"1_CR87","doi-asserted-by":"publisher","first-page":"935","DOI":"10.1038\/nature00965","volume":"418","author":"S.M. Reppert","year":"2002","unstructured":"Reppert, S.M., Weaver, D.R.: Coordination of circadian timing in mammals. Nature\u00a0418(6901), 935\u2013941 (2002)","journal-title":"Nature"},{"issue":"5","key":"1_CR88","doi-asserted-by":"publisher","first-page":"54103","DOI":"10.1063\/1.1835951","volume":"122","author":"H. Salis","year":"2005","unstructured":"Salis, H., Kaznessis, Y.: Accurate hybrid stochastic simulation of a system of coupled chemical or biochemical reactions. The Journal of Chemical Physics\u00a0122(5), 54103 (2005)","journal-title":"The Journal of Chemical Physics"},{"issue":"1","key":"1_CR89","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1049\/iet-syb.2009.0057","volume":"5","author":"K. Sanft","year":"2011","unstructured":"Sanft, K., Gillespie, D., Petzold, L.: Legitimacy of the stochastic Michaelis Menten approximation. IET Systems Biology\u00a05(1), 58 (2011)","journal-title":"IET Systems Biology"},{"key":"1_CR90","doi-asserted-by":"crossref","unstructured":"Schivo, S., et al.: Modelling biological pathway dynamics with timed automata. In: BIBE, pp. 447\u2013453. IEEE (2012)","DOI":"10.1109\/BIBE.2012.6399719"},{"issue":"5","key":"1_CR91","doi-asserted-by":"publisher","first-page":"1333","DOI":"10.1046\/j.0014-2956.2001.02720.x","volume":"269","author":"S. Schuster","year":"2002","unstructured":"Schuster, S., Marhl, M., H\u00f6fer, T.: Modelling of simple and complex calcium oscillations. European Journal of Biochemistry\u00a0269(5), 1333\u20131355 (2002)","journal-title":"European Journal of Biochemistry"},{"issue":"1930","key":"1_CR92","doi-asserted-by":"publisher","first-page":"4995","DOI":"10.1098\/rsta.2010.0211","volume":"368","author":"A. Singh","year":"2010","unstructured":"Singh, A., Hespanha, J.P.: Stochastic hybrid systems for studying biochemical processes. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences\u00a0368(1930), 4995\u20135011 (2010)","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"issue":"5","key":"1_CR93","doi-asserted-by":"publisher","first-page":"2786","DOI":"10.1016\/S0006-3495(04)74332-5","volume":"86","author":"P. Smolen","year":"2004","unstructured":"Smolen, P., Hardin, P.E., Lo, B.S., Baxter, D.A., Byrne, J.H.: Simulation of drosophila circadian oscillations, mutations, and light responses by a model with VRI, PDP-1, and CLK. Biophysical Journal\u00a086(5), 2786\u20132802 (2004)","journal-title":"Biophysical Journal"},{"issue":"17","key":"1_CR94","doi-asserted-by":"crossref","first-page":"11068","DOI":"10.1016\/S0021-9258(18)99129-5","volume":"266","author":"R. Somogyi","year":"1991","unstructured":"Somogyi, R., Stucki, J.W.: Hormone-induced calcium oscillations in liver cells can be explained by a simple one pool model. Journal of Biological Chemistry\u00a0266(17), 11068\u201311077 (1991)","journal-title":"Journal of Biological Chemistry"},{"key":"1_CR95","unstructured":"Spieler, D.: Model checking of oscillatory and noisy periodic behavior in Markovian population models. Technical report, Saarland University (2009), Master thesis available at http:\/\/mosi.cs.uni-saarland.de\/?page_id=93"},{"key":"1_CR96","unstructured":"Steinfeld, J., Francisco, J., Hase, W.: Chemical kinetics and dynamics. Prentice Hall (1989)"},{"key":"1_CR97","doi-asserted-by":"crossref","unstructured":"Stiver, J.A., Antsaklis, P.J.: State space partitioning for hybrid control systems. In: American Control Conference, pp. 2303\u20132304. IEEE (1993)","DOI":"10.23919\/ACC.1993.4793297"},{"issue":"1328","key":"1_CR98","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1098\/rstb.1995.0102","volume":"349","author":"Y. Tang","year":"1995","unstructured":"Tang, Y., Othmer, H.G.: Excitation, oscillations and wave propagation in a G-protein-based model of signal transduction in dictyostelium discoideum. Philosophical Transactions of the Royal Society B: Biological Sciences\u00a0349(1328), 179\u2013195 (1995)","journal-title":"Philosophical Transactions of the Royal Society B: Biological Sciences"},{"key":"1_CR99","doi-asserted-by":"crossref","unstructured":"Tyson, J.J.: Biological switches and clocks. Journal of the Royal Society Interface\u00a05, S1\u2013S8 (2008)","DOI":"10.1098\/rsif.2008.0179.focus"},{"issue":"5","key":"1_CR100","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1016\/0167-6377(92)90086-I","volume":"12","author":"N.M. Dijk van","year":"1992","unstructured":"van Dijk, N.M.: Uniformization for nonhomogeneous Markov chains. Operations Research Letters\u00a012(5), 283\u2013291 (1992)","journal-title":"Operations Research Letters"},{"issue":"9","key":"1_CR101","doi-asserted-by":"publisher","first-page":"5988","DOI":"10.1073\/pnas.092133899","volume":"99","author":"J. Vilar","year":"2002","unstructured":"Vilar, J., Kueh, H.-Y., Barkai, N., Leibler, S.: Mechanisms of noise-resistance in genetic oscillators. PNAS\u00a099(9), 5988\u20135992 (2002)","journal-title":"PNAS"},{"key":"1_CR102","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1038\/118558a0","volume":"118","author":"V. Volterra","year":"1926","unstructured":"Volterra, V.: Fluctuations in the abundance of a species considered mathematically. Nature\u00a0118, 558\u2013560 (1926)","journal-title":"Nature"},{"issue":"17","key":"1_CR103","doi-asserted-by":"publisher","first-page":"174104","DOI":"10.1063\/1.2361284","volume":"125","author":"H. Wagner","year":"2006","unstructured":"Wagner, H., M\u00f6ller, M., Prank, K.: COAST: controllable approximative stochastic reaction algorithm. The Journal of Chemical Physics\u00a0125(17), 174104 (2006)","journal-title":"The Journal of Chemical Physics"},{"issue":"3","key":"1_CR104","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1109\/TNB.2004.833694","volume":"3","author":"O. Wolkenhauer","year":"2004","unstructured":"Wolkenhauer, O., Ullah, M., Kolch, W., Cho, K.-H.: Modeling and simulation of intracellular dynamics: Choosing an appropriate framework. IEEE Transactions on Nanobioscience\u00a03(3), 200\u2013207 (2004)","journal-title":"IEEE Transactions on Nanobioscience"},{"key":"1_CR105","doi-asserted-by":"crossref","unstructured":"Zeilinger, M.N., Farr, E.M., Taylor, S.R., Kay, S.A., Doyle, F.J.: A novel computational model of the circadian clock in arabidopsis that incorporates PRR7 and PRR9. Molecular Systems Biology\u00a02 (2006)","DOI":"10.1038\/msb4100101"}],"container-title":["Lecture Notes in Computer Science","Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45489-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T05:47:26Z","timestamp":1746510446000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-45489-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662454886","9783662454893"],"references-count":106,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-45489-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}