{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:51Z","timestamp":1740099051360,"version":"3.37.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319893655"},{"type":"electronic","value":"9783319893662"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89366-2_21","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T19:52:34Z","timestamp":1523649154000},"page":"384-402","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["A Hierarchy of Scheduler Classes for\u00a0Stochastic Automata"],"prefix":"10.1007","author":[{"given":"Pedro R.","family":"D\u2019Argenio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2655-9617","authenticated-orcid":false,"given":"Marcus","family":"Gerhold","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2903-0823","authenticated-orcid":false,"given":"Sean","family":"Sedwards","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"unstructured":"de Alfaro, L.: The verification of probabilistic systems under memoryless partial-information policies is hard. Technical report, DTIC Document (1999)","key":"21_CR1"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1991","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for probabilistic real-time systems. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 115\u2013126. Springer, Heidelberg (1991). \nhttps:\/\/doi.org\/10.1007\/3-540-54233-7_128"},{"issue":"7","key":"21_CR3","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/MC.2006.242","volume":"39","author":"TR Andel","year":"2006","unstructured":"Andel, T.R., Yasinsac, A.: On the credibility of MANET simulations. IEEE Comput. 39(7), 48\u201354 (2006)","journal-title":"IEEE Comput."},{"key":"21_CR4","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2014.12.010","volume":"310","author":"A Avritzer","year":"2015","unstructured":"Avritzer, A., Carnevali, L., Ghasemieh, H., Happe, L., Haverkort, B.R., Koziolek, A., Menasch\u00e9, D.S., Remke, A., Sarvestani, S.S., Vicario, E.: Survivability evaluation of gas, water and electricity infrastructures. Electr. Notes Theor. Comput. Sci. 310, 5\u201325 (2015)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"21_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-40196-1_30","volume-title":"Quantitative Evaluation of Systems","author":"P Ballarini","year":"2013","unstructured":"Ballarini, P., Bertrand, N., Horv\u00e1th, A., Paolieri, M., Vicario, E.: Transient analysis of networks of stochastic timed automata using stochastic state classes. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 355\u2013371. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-40196-1_30"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-319-48989-6_34","volume-title":"FM 2016: Formal Methods","author":"M Bisgaard","year":"2016","unstructured":"Bisgaard, M., Gerhardt, D., Hermanns, H., Kr\u010d\u00e1l, J., Nies, G., Stenger, M.: Battery-aware scheduling in low orbit: the GomX\u20133 case. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 559\u2013576. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_34"},{"issue":"10","key":"21_CR8","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24611-4_2","volume-title":"Validation of Stochastic Systems","author":"M Bravetti","year":"2004","unstructured":"Bravetti, M., D\u2019Argenio, P.R.: Tutte le algebre insieme: concepts, discussions and relations of stochastic process algebras with general distributions. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 44\u201388. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24611-4_2"},{"issue":"1","key":"21_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0304-3975(01)00043-3","volume":"282","author":"M Bravetti","year":"2002","unstructured":"Bravetti, M., Gorrieri, R.: The theory of interactive generalized semi-Markov processes. Theor. Comput. Sci. 282(1), 5\u201332 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-23217-6_10","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"T Br\u00e1zdil","year":"2011","unstructured":"Br\u00e1zdil, T., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., \u0158eh\u00e1k, V.: Fixed-delay events in generalized semi-Markov processes revisited. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 140\u2013155. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-23217-6_10"},{"issue":"4","key":"21_CR12","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1145\/937555.937558","volume":"4","author":"J Bryans","year":"2003","unstructured":"Bryans, J., Bowman, H., Derrick, J.: Model checking stochastic automata. ACM Trans. Comput. Log. 4(4), 452\u2013492 (2003)","journal-title":"ACM Trans. Comput. Log."},{"doi-asserted-by":"crossref","unstructured":"Buchholz, P., Kriege, J., Scheftelowitsch, D.: Model checking stochastic automata for dependability and performance measures. In: DSN, pp. 503\u2013514. IEEE Computer Society (2014)","key":"21_CR13","DOI":"10.1109\/DSN.2014.53"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-24953-7_12","volume-title":"Automated Technology for Verification and Analysis","author":"Y Butkova","year":"2015","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Kr\u010d\u00e1l, J.: Optimal continuous time Markov decisions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 166\u2013182. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-24953-7_12"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-33693-0_7","volume-title":"Integrated Formal Methods","author":"PR D\u2019Argenio","year":"2016","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Legay, A., Sedwards, S.: Statistical approximation of optimal schedulers for probabilistic timed automata. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 99\u2013114. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33693-0_7"},{"issue":"1","key":"21_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2005.07.001","volume":"203","author":"PR D\u2019Argenio","year":"2005","unstructured":"D\u2019Argenio, P.R., Katoen, J.P.: A theory of stochastic systems part I: stochastic automata. Inf. Comput. 203(1), 1\u201338 (2005)","journal-title":"Inf. Comput."},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-319-44878-7_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"PR D\u2019Argenio","year":"2016","unstructured":"D\u2019Argenio, P.R., Lee, M.D., Monti, R.E.: Input\/output stochastic automata. In: Fr\u00e4nzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 53\u201368. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-44878-7_4"},{"issue":"4","key":"21_CR18","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s10009-015-0383-0","volume":"17","author":"PR D\u2019Argenio","year":"2015","unstructured":"D\u2019Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.M.: Smart sampling for lightweight verification of Markov decision processes. STTT 17(4), 469\u2013484 (2015)","journal-title":"STTT"},{"doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE Computer Society (2010)","key":"21_CR19","DOI":"10.1109\/LICS.2010.41"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-540-75454-1_14","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Giro","year":"2007","unstructured":"Giro, S., D\u2019Argenio, P.R.: Quantitative model checking revisited: neither decidable nor approximable. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 179\u2013194. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-75454-1_14"},{"issue":"3","key":"21_CR21","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1080\/15326348708807064","volume":"3","author":"PJ Haas","year":"1987","unstructured":"Haas, P.J., Shedler, G.S.: Regenerative generalized semi-Markov processes. commun. stat. Stochast. Models 3(3), 409\u2013438 (1987)","journal-title":"commun. stat. Stochast. Models"},{"unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H.: Reachability and reward checking for stochastic timed automata. In: Electronic Communications of the EASST, AVoCS 2014, vol. 70 (2014)","key":"21_CR22"},{"issue":"1","key":"21_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1093\/logcom\/10.1.3","volume":"10","author":"PG Harrison","year":"2000","unstructured":"Harrison, P.G., Strulo, B.: SPADES - a process algebra for discrete event simulation. J. Log. Comput. 10(1), 3\u201342 (2000)","journal-title":"J. Log. Comput."},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-27810-0_11","volume-title":"Semantics, Logics, and Calculi","author":"A Hartmanns","year":"2016","unstructured":"Hartmanns, A., Hermanns, H., Kr\u010d\u00e1l, J.: Schedulers are no Prophets. In: Probst, C.W., Hankin, C., Hansen, R.R. (eds.) Semantics, Logics, and Calculi. LNCS, vol. 9560, pp. 214\u2013235. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-27810-0_11"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Sedwards, S., D\u2019Argenio, P.: Efficient simulation-based verification of probabilistic timed automata. In: WSC. IEEE (2017). \nhttps:\/\/doi.org\/10.1109\/WSC.2017.8247885","key":"21_CR26","DOI":"10.1109\/WSC.2017.8247885"},{"key":"21_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains: The Quest for Quantified Quality","author":"H Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45804-2"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-662-49635-0_9","volume-title":"Principles of Security and Trust","author":"H Hermanns","year":"2016","unstructured":"Hermanns, H., Kr\u00e4mer, J., Kr\u010d\u00e1l, J., Stoelinga, M.: The value of attack-defence diagrams. In: Piessens, F., Vigan\u00f2, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 163\u2013185. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49635-0_9"},{"issue":"4","key":"21_CR29","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/1096166.1096174","volume":"9","author":"S Kurkowski","year":"2005","unstructured":"Kurkowski, S., Camp, T., Colagrosso, M.: MANET simulation studies: the incredibles. Mob. Comput. Commun. Rev. 9(4), 50\u201361 (2005)","journal-title":"Mob. Comput. Commun. Rev."},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-44618-4_11","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"M Kwiatkowska","year":"2000","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 123\u2013137. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/3-540-44618-4_11"},{"unstructured":"Legay, A., Sedwards, S., Traonouez, L.M.: Estimating rewards & rare events in nondeterministic systems. In: Electronic Communications of the EASST, AVoCS 2015, vol. 72 (2015)","key":"21_CR31"},{"key":"21_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-15201-1_23","volume-title":"Software Engineering and Formal Methods","author":"A Legay","year":"2015","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 350\u2013362. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-15201-1_23"},{"unstructured":"Matthes, K.: Zur Theorie der Bedienungsprozesse. In: 3rd Prague Conference on Information Theory, Stat. Dec. Fns. and Random Processes, pp. 513\u2013528 (1962)","key":"21_CR33"},{"unstructured":"NS-3 Consortium: ns-3: A Discrete-event Network Simulator for Internet Systems. \nhttps:\/\/www.nsnam.org\/","key":"21_CR34"},{"unstructured":"Pongor, G.: OMNeT: objective modular network testbed. In: MASCOTS, pp. 323\u2013326. The Society for Computer Simulation (1993)","key":"21_CR35"},{"key":"21_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-47166-2_10","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"E Ruijters","year":"2016","unstructured":"Ruijters, E., Stoelinga, M.: Better railway engineering through statistical model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 151\u2013165. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-47166-2_10"},{"unstructured":"Song, L., Zhang, L., Godskesen, J.C.: Late weak bisimulation for Markov automata. CoRR abs\/1202.4116 (2012)","key":"21_CR37"},{"unstructured":"Strulo, B.: Process algebra for discrete event simulation. Ph.D. thesis, Imperial College of Science, Technology and Medicine. University of London, October 1993","key":"21_CR38"},{"issue":"3","key":"21_CR39","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/j.entcs.2006.07.019","volume":"164","author":"V Wolf","year":"2006","unstructured":"Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace semantics for stochastic systems with nondeterminism. Electr. Notes Theor. Comput. Sci. 164(3), 187\u2013204 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"unstructured":"Wolovick, N.: Continuous probability and nondeterminism in labeled transition systems. Ph.D. thesis, Universidad Nacional de C\u00f3rdoba, C\u00f3rdoba, Argentina (2012)","key":"21_CR40"},{"key":"21_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11867340_25","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"N Wolovick","year":"2006","unstructured":"Wolovick, N., Johr, S.: A characterization of meaningful schedulers for continuous-time Markov decision processes. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 352\u2013367. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11867340_25"},{"doi-asserted-by":"crossref","unstructured":"Zeng, X., Bagrodia, R.L., Gerla, M.: Glomosim: a library for parallel simulation of large-scale wireless networks. In: PADS, pp. 154\u2013161. IEEE Computer Society (1998)","key":"21_CR42","DOI":"10.1145\/278009.278027"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89366-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T19:59:09Z","timestamp":1523649549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89366-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893655","9783319893662"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89366-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}