{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,8]],"date-time":"2023-09-08T09:52:56Z","timestamp":1694166776216},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,2,24]],"date-time":"2015-02-24T00:00:00Z","timestamp":1424736000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10009-015-0370-5","type":"journal-article","created":{"date-parts":[[2015,2,23]],"date-time":"2015-02-23T13:20:09Z","timestamp":1424697609000},"page":"505-526","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Analysing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking"],"prefix":"10.1007","volume":"17","author":[{"given":"Paolo","family":"Ballarini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,2,24]]},"reference":[{"key":"370_CR1","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"M Ajmone Marsan","year":"1995","unstructured":"Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley, London (1995)"},{"key":"370_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for probabilistic real-time systems. In: ICALP\u201991, LNCS 510 (1991)","DOI":"10.1007\/3-540-54233-7_128"},{"key":"370_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-35524-0_1","volume":"14","author":"O Andrei","year":"2012","unstructured":"Andrei, O., Calder, M.: Trend-based analysis of a population model of the akap scaffold protein. Trans. Compt. Syst. Biol. 14, 1\u201325 (2012)","journal-title":"Trans. Compt. Syst. Biol."},{"key":"370_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for CTMCs. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","DOI":"10.1109\/TSE.2003.1205180"},{"key":"370_CR5","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: A statistical model checker for the hybrid automata stochastic logic. In: Proceedings of the 8th international conference on quantitative evaluation of systems (QEST\u201911), pp. 143\u2013144. IEEE Computer Society Press (2011)","DOI":"10.1109\/QEST.2011.24"},{"key":"370_CR6","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: HASL: an expressive language for statistical verification of stochastic models. In: Proceedings of Valuetools (2011)","DOI":"10.4108\/icst.valuetools.2011.245710"},{"issue":"20","key":"370_CR7","doi-asserted-by":"crossref","first-page":"2019","DOI":"10.1016\/j.tcs.2010.02.010","volume":"411","author":"P Ballarini","year":"2010","unstructured":"Ballarini, P., Guerriero, M.: Query-based verification of qualitative trends and oscillations in biochemical systems. Theor. Comput. Sci. 411(20), 2019\u20132036 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"370_CR8","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: Uppaal-SMC: statistical model checking for priced timed automata. In: Proceedings 10th workshop on quantitative aspects of programming languages and systems, volume 85 of EPTCS, pp. 1\u201316 (2012)","DOI":"10.4204\/EPTCS.85.1"},{"key":"370_CR9","doi-asserted-by":"crossref","unstructured":"Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of CTMC against timed automata specifications. In: Proceedings of LICS\u201909 (2009)","DOI":"10.1109\/LICS.2009.21"},{"key":"370_CR10","unstructured":"CosyVerif home page. http:\/\/www.cosyverif.org"},{"key":"370_CR11","unstructured":"Cosmos home page. http:\/\/www.lsv.ens-cachan.fr\/software\/cosmos\/"},{"key":"370_CR12","first-page":"388","volume":"1","author":"A David","year":"2012","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Runtime verification of biological systems. ISoLA 1, 388\u2013404 (2012)","journal-title":"ISoLA"},{"key":"370_CR13","doi-asserted-by":"crossref","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with $$CSL^{TA}$$ C S L T A . IEEE Trans. Softw. Eng., 35, 224\u2013240 (2009)","DOI":"10.1109\/TSE.2008.108"},{"key":"370_CR14","unstructured":"Glynn, P.W.: On the role of generalized semi-Markov processes in simulation output analysis. In: Proceedings of conference winter simulation (1983)"},{"key":"370_CR15","unstructured":"Herault, T., Lassaigne, R., Peyronnet, S.: APMC 3.0: Approximate verification of discrete and continuous time Markov chains. In: Proceedings of QEST\u201906 (2006)"},{"issue":"1","key":"370_CR16","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1186\/1752-0509-5-203","volume":"5","author":"A Ihekwaba","year":"2011","unstructured":"Ihekwaba, A., Sedwards, S.: Communicating oscillatory networks: frequency domain analysis. BMC Syst. Biol. 5(1), 203 (2011)","journal-title":"BMC Syst. Biol."},{"key":"370_CR17","doi-asserted-by":"crossref","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking-plasma. In: TACAS, Volume 7214 of Lecture Notes in Computer Science, pp. 498\u2013503 (2012)","DOI":"10.1007\/978-3-642-28756-5_37"},{"key":"370_CR18","unstructured":"J\u00falvez, J., Kwiatkowska, M., Norman, G., Parker, D.: Evaluation of sustained stochastic oscillations by means of a system of differential equations. Int. J. Comput Appl. (IJCA) 19(2), 101\u2013111 (2012)"},{"key":"370_CR19","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Zapreev, I.S.: Simulation-based CTMC model checking: an empirical evaluation. In: Proceedings of QEST\u201909 (2009)","DOI":"10.1109\/QEST.2009.25"},{"key":"370_CR20","volume-title":"The Art of Computer Programming, Volume 2 (3rd Ed.): Seminumerical Algorithms","author":"DE Knuth","year":"1997","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 2 (3rd Ed.): Seminumerical Algorithms. Addison-Wesley Longman Publishing Co., Inc, Boston (1997)"},{"key":"370_CR21","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation, volume 4486 of LNCS, pp. 220\u2013270, Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"370_CR22","unstructured":"Prism home page. http:\/\/www.prismmodelchecker.org"},{"key":"370_CR23","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: Proceedings of QEST\u201905 (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"370_CR24","unstructured":"Spieler, D. : Model checking of oscillatory and noisy periodic behavior in markovian population models. Master\u2019s thesis, Saarland University (2009)"},{"key":"370_CR25","doi-asserted-by":"crossref","unstructured":"Spieler, D.: Characterizing oscillatory and noisy periodic behavior in markov population models. In: Proceedings of QEST\u201913 (2013)","DOI":"10.1007\/978-3-642-40196-1_8"},{"issue":"9","key":"370_CR26","doi-asserted-by":"crossref","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. Proc. Natl. Acad. Sci. USA 99(9), 5988\u20135992 (2002)","journal-title":"Proc. Natl. Acad. Sci. USA"},{"key":"370_CR27","doi-asserted-by":"crossref","unstructured":"Ymer, H.L. Younes.: A statistical model checker. In: Computer Aided Verification, pp. 429\u2013433, Springer, Berlin (2005)","DOI":"10.1007\/11513988_43"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0370-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0370-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0370-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T01:03:09Z","timestamp":1566349389000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0370-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,24]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["370"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0370-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,24]]}}}