{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:09:41Z","timestamp":1771700981241,"version":"3.50.1"},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,10,12]],"date-time":"2012-10-12T00:00:00Z","timestamp":1350000000000},"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-0177-x","type":"journal-article","created":{"date-parts":[[2012,10,11]],"date-time":"2012-10-11T13:48:23Z","timestamp":1349963303000},"page":"164-190","source":"Crossref","is-referenced-by-count":91,"title":["Model checking for probabilistic timed automata"],"prefix":"10.1007","volume":"43","author":[{"given":"Gethin","family":"Norman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Sproston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,12]]},"reference":[{"key":"177_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Proc of 19th international colloquium on automata, languages and programming (ICALP\u201991)","author":"R Alur","year":"1991","unstructured":"Alur R, Courcoubetis C, Dill D (1991) Model-checking for probabilistic real-time systems. In: Proc of 19th international colloquium on automata, languages and programming (ICALP\u201991). LNCS, vol\u00a0510. Springer, Berlin, pp\u00a0115\u2013136"},{"issue":"1","key":"177_CR2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill D (1993) Model checking in dense real time. Inf Comput 104(1):2\u201334","journal-title":"Inf Comput"},{"key":"177_CR3","series-title":"LNCS","first-page":"340","volume-title":"Proc of 3rd int conf on concurrency theory (CONCUR\u201992)","author":"R Alur","year":"1992","unstructured":"Alur R, Courcoubetis C, Halbwachs N, Dill D, Wong-Toi H (1992) Minimization of timed transition systems. In: Cleaveland R (ed) Proc of 3rd int conf on concurrency theory (CONCUR\u201992). LNCS, vol\u00a0630. Springer, Berlin, pp\u00a0340\u2013354"},{"key":"177_CR4","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\u00a0theory of timed automata. Theor Comput Sci 126:183\u2013235","journal-title":"Theor Comput Sci"},{"issue":"3","key":"177_CR5","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/j.tcs.2003.10.038","volume":"318","author":"R Alur","year":"2004","unstructured":"Alur R, La Torre S, Pappas G (2004) Optimal paths in weighted timed automata. Theor Comput Sci 318(3):297\u2013322","journal-title":"Theor Comput Sci"},{"key":"177_CR6","first-page":"165","volume-title":"Proc of 11th int conf on embedded software (EMSOFT\u201911)","author":"R Alur","year":"2011","unstructured":"Alur R, Trivedi A (2011) Relating average and discounted costs for quantitative analysis of timed systems. In: Proc of 11th int conf on embedded software (EMSOFT\u201911). ACM, New York, pp\u00a0165\u2013174"},{"key":"177_CR7","author":"E Andr\u00e9","year":"2012","unstructured":"Andr\u00e9 E, Fribourg L, Sproston J (2012) An extension of the inverse method to probabilistic timed automata. Form Methods Syst Des. doi: 10.1007\/s10703-012-0169-x","journal-title":"Form Methods Syst Des"},{"key":"177_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/BFb0055642","volume-title":"Proc of 9th int conf on concurrency theory (CONCUR\u201998)","author":"E Asarin","year":"1998","unstructured":"Asarin E, Maler O, Pnueli A (1998) On discretization of delays in timed automata and digital circuits. In: Sangiorgi D, de Simone R (eds) Proc of 9th int conf on concurrency theory (CONCUR\u201998). LNCS, vol\u00a01466. Springer, Berlin, pp\u00a0470\u2013484"},{"key":"177_CR9","first-page":"104","volume-title":"Proc of 9th workshop on quantitative aspects of programming languages (QAPL\u201911)","author":"J Assouramou","year":"2011","unstructured":"Assouramou J, Desharnais J (2011) Analysis of non-linear probabilistic hybrid systems. In: Massink M, Norman G (eds) Proc of 9th workshop on quantitative aspects of programming languages (QAPL\u201911), pp\u00a0104\u2013119"},{"issue":"3","key":"177_CR10","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C Baier","year":"1998","unstructured":"Baier C, Kwiatkowska M (1998) Model checking for a probabilistic branching time logic with fairness. Distrib Comput 11(3):125\u2013155","journal-title":"Distrib Comput"},{"issue":"1","key":"177_CR11","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S0304-3975(01)00215-8","volume":"292","author":"D Beauquier","year":"2003","unstructured":"Beauquier D (2003) On probabilistic timed automata. Theor Comput Sci 292(1):65\u201384","journal-title":"Theor Comput Sci"},{"key":"177_CR12","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Proc of 19th international conference on computer aided verification (CAV\u201907)","author":"G Behrmann","year":"2007","unstructured":"Behrmann G, Cougnard A, David A, Fleury E, Larsen K, Lime D (2007) UPPAAL-Tiga: time for playing games! In: Proc of 19th international conference on computer aided verification (CAV\u201907). LNCS, vol\u00a04590. Springer, Berlin, pp\u00a0121\u2013125"},{"key":"177_CR13","first-page":"125","volume-title":"Proc of 3rd int conf on quantitative evaluation of systems (QEST\u201906)","author":"G Behrmann","year":"2006","unstructured":"Behrmann G, David A, Larsen KG, H\u00e5kansson J, Pettersson P, Yi W, Hendriks M (2006) Uppaal 4.0. In: Proc of 3rd int conf on quantitative evaluation of systems (QEST\u201906). IEEE Press, New York, pp\u00a0125\u2013126"},{"key":"177_CR14","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Proc of 4th int workshop on hybrid systems: computation and control (HSCC\u201901)","author":"G Behrmann","year":"2001","unstructured":"Behrmann G, Fehnker A, Hune T, Larsen K, Pettersson P, Romijn J, Vaandrager F (2001) Minimum-cost reachability for linearly priced timed automata. In: Benedetto MD, Sangiovanni-Vincentelli A (eds) Proc of 4th int workshop on hybrid systems: computation and control (HSCC\u201901). LNCS, vol\u00a02034. Springer, Berlin, pp\u00a0147\u2013162"},{"issue":"2\u20133","key":"177_CR15","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/FI-1998-36233","volume":"36","author":"B B\u00e9rard","year":"1998","unstructured":"B\u00e9rard B, Petit A, Diekert V, Gastin P (1998) Characterization of the expressive power of silent transitions in timed automata. Fundam Inform 36(2\u20133):145\u2013182","journal-title":"Fundam Inform"},{"key":"177_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-642-02017-9_16","volume-title":"Proc of 6th conf on theory and applications of models of computation (TAMC\u201909)","author":"J Berendsen","year":"2009","unstructured":"Berendsen J, Chen T, Jansen D (2009) Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen J, Cooper SB (eds) Proc of 6th conf on theory and applications of models of computation (TAMC\u201909). LNCS, vol\u00a05532. Springer, Berlin, pp\u00a0128\u2013137"},{"key":"177_CR17","first-page":"311","volume-title":"Proc of 3rd int conf on quantitative evaluation of systems (QEST\u201906)","author":"J Berendsen","year":"2006","unstructured":"Berendsen J, Jansen D, Katoen JP (2006) Probably on time and within budget: on reachability in priced probabilistic timed automata. In: Proc of 3rd int conf on quantitative evaluation of systems (QEST\u201906). IEEE Press, New York, pp\u00a0311\u2013322"},{"key":"177_CR18","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1109\/QEST.2010.41","volume-title":"Proc of 7th int conf on quantitative evaluation of systems (QEST\u201910)","author":"J Berendsen","year":"2010","unstructured":"Berendsen J, Jansen D, Vaandrager F (2010) Fortuna: model checking priced probabilistic timed automata. In: Proc of 7th int conf on quantitative evaluation of systems (QEST\u201910). IEEE Press, New York, pp\u00a0273\u2013281"},{"key":"177_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-45251-6_18","volume-title":"Int symp of formal methods Europe, FME 2001: formal methods for increasing software productivity","author":"D Beyer","year":"2001","unstructured":"Beyer D (2001) Improvements in BDD-based reachability analysis of timed automata. In: Oliveira J, Zave P (eds) Int symp of formal methods Europe, FME 2001: formal methods for increasing software productivity. LNCS, vol\u00a02021. Springer, Berlin, pp\u00a0318\u2013343"},{"key":"177_CR20","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Proc of 15th conf on foundations of software technology and theoretical computer science (FSTTCS\u201995)","author":"A Bianco","year":"1995","unstructured":"Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Thiagarajan P (ed) Proc of 15th conf on foundations of software technology and theoretical computer science (FSTTCS\u201995). LNCS, vol\u00a01026. Springer, Berlin, pp\u00a0499\u2013513"},{"issue":"10","key":"177_CR21","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"H Bohnenkamp","year":"2006","unstructured":"Bohnenkamp H, D\u2019Argenio P, Hermanns H, Katoen JP (2006) Modest: a\u00a0compositional modeling formalism for hard and softly timed systems. IEEE Trans Softw Eng 32(10):812\u2013830","journal-title":"IEEE Trans Softw Eng"},{"key":"177_CR22","series-title":"LNCS","first-page":"620","volume-title":"Proc of 20th int symp on theoretical aspects of computer science (STACS\u201903)","author":"P Bouyer","year":"2003","unstructured":"Bouyer P (2003) Untameable timed automata! In: Alt H, Habib M (eds) Proc of 20th int symp on theoretical aspects of computer science (STACS\u201903). LNCS, vol\u00a02607. Springer, Berlin, pp\u00a0620\u2013631"},{"key":"177_CR23","unstructured":"Bouyer P (2009) From qualitative to quantitative analysis of timed systems. M\u00e9moire d\u2019habilitation. Universit\u00e9 Paris 7, Paris, France"},{"issue":"1","key":"177_CR24","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10703-007-0043-4","volume":"32","author":"P Bouyer","year":"2008","unstructured":"Bouyer P, Brinksma E, Larsen K (2008) Optimal infinite scheduling for multi-priced timed automata. Form Methods Syst Des 32(1):3\u201323","journal-title":"Form Methods Syst Des"},{"issue":"4","key":"177_CR25","first-page":"393","volume":"10","author":"P Bouyer","year":"2005","unstructured":"Bouyer P, Chevalier F (2005) On conciseness of extensions of timed automata. J Autom Lang Comb 10(4):393\u2013405","journal-title":"J Autom Lang Comb"},{"issue":"2\u20133","key":"177_CR26","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/j.tcs.2004.04.003","volume":"321","author":"P Bouyer","year":"2004","unstructured":"Bouyer P, Dufourd C, Fleury E, Petit A (2004) Updatable timed automata. Theor Comput Sci 321(2\u20133):291\u2013345","journal-title":"Theor Comput Sci"},{"issue":"9","key":"177_CR27","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1145\/1995376.1995396","volume":"54","author":"P Bouyer","year":"2011","unstructured":"Bouyer P, Fahrenberg U, Larsen K, Markey N (2011) Quantitative analysis of real-time systems using priced timed automata. Commun ACM 54(9):78\u201387","journal-title":"Commun ACM"},{"key":"177_CR28","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1109\/TASE.2008.29","volume-title":"Proc of 2nd IEEE int symp on theoretical aspects of software engineering (TASE\u201908)","author":"T Chen","year":"2008","unstructured":"Chen T, Han T, Katoen JP (2008) Time-abstracting bisimulation for probabilistic timed automata. In: Proc of 2nd IEEE int symp on theoretical aspects of software engineering (TASE\u201908). IEEE Press, New York, pp\u00a0177\u2013184"},{"key":"177_CR29","series-title":"LNCS","volume-title":"Proc of workshop on logic of programs","author":"E Clarke","year":"1981","unstructured":"Clarke E, Emerson A (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen D (ed) Proc of workshop on logic of programs. LNCS, vol\u00a0131. Springer, Berlin"},{"key":"177_CR30","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/REAL.1995.495197","volume-title":"Proc of IEEE real-time systems symposium (RTSS\u201995)","author":"C Daws","year":"1995","unstructured":"Daws C, Yovine S (1995) Two examples of verification of multirate timed automata with KRONOS. In: Proc of IEEE real-time systems symposium (RTSS\u201995). IEEE Press, New York, pp\u00a066\u201375"},{"key":"177_CR31","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1109\/LICS.2010.41","volume-title":"Proc of 25th annual IEEE symposium on logic in computer science (LICS\u201910)","author":"C Eisentraut","year":"2010","unstructured":"Eisentraut C, Hermanns H, Zhang L (2010) On probabilistic automata in continuous time. In: Proc of 25th annual IEEE symposium on logic in computer science (LICS\u201910). IEEE Comput. Soc., Los Alamitos, pp\u00a0342\u2013351"},{"key":"177_CR32","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal methods for eternal networked software systems (SFM\u201911)","author":"V Forejt","year":"2011","unstructured":"Forejt V, Kwiatkowska M, Norman G, Parker D (2011) Automated verification techniques for probabilistic systems. In: Bernardo M, Issarny V (eds) Formal methods for eternal networked software systems (SFM\u201911). LNCS, vol\u00a06659. Springer, Berlin, pp\u00a053\u2013113"},{"key":"177_CR33","volume-title":"Proc of 2nd int symp on leveraging applications of formal methods, verification and validation (ISOLA\u201906)","author":"M Fruth","year":"2006","unstructured":"Fruth M (2006) Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol. In: Proc of 2nd int symp on leveraging applications of formal methods, verification and validation (ISOLA\u201906)"},{"key":"177_CR34","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-69209-6_18","volume-title":"Intelligence and security informatics","author":"U Gl\u00e4sser","year":"2008","unstructured":"Gl\u00e4sser U, Rastkar S, Vajihollahi M (2008) Modeling and validation of aviation security. In: Intelligence and security informatics, vol\u00a0135. Springer, Berlin, pp\u00a0337\u2013355"},{"key":"177_CR35","unstructured":"Gregersen H, Jensen HE (1995) Formal design of reliable real time systems. Master\u2019s thesis, Department of Mathematics and Computer Science, Aalborg University"},{"key":"177_CR36","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/QEST.2011.17","volume-title":"Proc of 8th int conf on quantitative evaluation of systems (QEST\u201911)","author":"EM Hahn","year":"2011","unstructured":"Hahn EM, Norman G, Parker D, Wachter B, Zhang L (2011) Game-based abstraction and controller synthesis for probabilistic hybrid systems. In: Proc of 8th int conf on quantitative evaluation of systems (QEST\u201911). IEEE Press, New York, pp\u00a069\u201378"},{"issue":"5","key":"177_CR37","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A\u00a0logic for reasoning about time and reliability. Form Asp Comput 6(5):512\u2013535","journal-title":"Form Asp Comput"},{"key":"177_CR38","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1109\/QEST.2009.41","volume-title":"Proc of 6th int conf on quantitative evaluation of systems (QEST\u201909)","author":"A Hartmanns","year":"2009","unstructured":"Hartmanns A, Hermanns H (2009) A\u00a0modest approach to checking probabilistic timed automata. In: Proc of 6th int conf on quantitative evaluation of systems (QEST\u201909). IEEE Press, New York, pp\u00a0187\u2013196"},{"key":"177_CR39","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Proc of 19th int colloq on automata, languages and programming (ICALP\u201992)","author":"T Henzinger","year":"1992","unstructured":"Henzinger T, Manna Z, Pnueli A (1992) What good are digital clocks? In: Kuich W (ed) Proc of 19th int colloq on automata, languages and programming (ICALP\u201992). LNCS, vol\u00a0623. Springer, Berlin, pp\u00a0545\u2013558"},{"issue":"2","key":"177_CR40","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T Henzinger","year":"1994","unstructured":"Henzinger T, Nicollin X, Sifakis J, Yovine S (1994) Symbolic model checking for real-time systems. Inf Comput 111(2):193\u2013244","journal-title":"Inf Comput"},{"key":"177_CR41","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov chains and the quest for quantified quality","author":"H Hermanns","year":"2002","unstructured":"Hermanns H (2002) Interactive Markov chains and the quest for quantified quality. LNCS, vol\u00a02428. Springer, Berlin"},{"key":"177_CR42","series-title":"Report","first-page":"247","volume-title":"Proc of 7th Nordic workshop on programming theory","author":"H Jensen","year":"1996","unstructured":"Jensen H (1996) Model checking probabilistic real time systems. In: Bjerner B, Larsson M, Nordstr\u00f6m\u00a0B (eds) Proc of 7th Nordic workshop on programming theory. Report, vol\u00a086. Chalmers University of Technology, Chalmers, pp\u00a0247\u2013261"},{"key":"177_CR43","series-title":"LNCS","first-page":"415","volume-title":"Proc of 20th int conf on concurrency theory (CONCUR\u201909)","author":"M Jurdzi\u0144ski","year":"2009","unstructured":"Jurdzi\u0144ski M, Kwiatkowska M, Norman G, Trivedi A (2009) Concavely-priced probabilistic timed automata. In: Bravetti M, Zavattaro G (eds) Proc of 20th int conf on concurrency theory (CONCUR\u201909). LNCS, vol\u00a05710. Springer, Berlin, pp\u00a0415\u2013430"},{"key":"177_CR44","doi-asserted-by":"crossref","unstructured":"Jurdzinski M, Sproston J, Laroussinie F (2008) Model checking probabilistic timed automata with one or two clocks. Logical Methods in Computer Science 4(3)","DOI":"10.2168\/LMCS-4(3:12)2008"},{"key":"177_CR45","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1109\/QEST.2009.11","volume-title":"Proc of 6th int conf on quantitative evaluation of systems (QEST\u201909)","author":"JP Katoen","year":"2009","unstructured":"Katoen JP, Hahn EM, Hermanns H, Jansen D, Zapreev I (2009) The ins and outs of the probabilistic model checker MRMC. In: Proc of 6th int conf on quantitative evaluation of systems (QEST\u201909). IEEE Press, New York, pp\u00a0167\u2013176"},{"issue":"3","key":"177_CR46","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/s10703-010-0097-6","volume":"36","author":"M Kattenbelt","year":"2010","unstructured":"Kattenbelt M, Kwiatkowska M, Norman G, Parker D (2010) A\u00a0game-based abstraction-refinement framework for Markov decision processes. Form Methods Syst Des 36(3):246\u2013280","journal-title":"Form Methods Syst Des"},{"key":"177_CR47","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov chains","author":"J Kemeny","year":"1976","unstructured":"Kemeny J, Snell J, Knapp A (1976) Denumerable Markov chains, 2nd edn. Springer, Berlin","edition":"2"},{"key":"177_CR48","first-page":"64","volume-title":"Proc of 13th int workshop on verification of infinite-state systems (INFINITY\u201911), EPTCS","author":"C Krause","year":"2011","unstructured":"Krause C, Giese H (2011) Model checking probabilistic real-time properties for service-oriented systems with service level agreements. In: Proc of 13th int workshop on verification of infinite-state systems (INFINITY\u201911), EPTCS, vol\u00a073. Elsevier, Amsterdam, pp\u00a064\u201378"},{"key":"177_CR49","first-page":"157","volume-title":"Proc of 3rd int conf on quantitative evaluation of systems (QEST\u201906)","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska M, Norman G, Parker D (2006) Game-based abstraction for Markov decision processes. In: Proc of 3rd int conf on quantitative evaluation of systems (QEST\u201906). IEEE Press, New York, pp\u00a0157\u2013166"},{"key":"177_CR50","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Proc of 7th int conf on formal modelling and analysis of timed systems (FORMATS\u201909)","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska M, Norman G, Parker D (2009) Stochastic games for verification of probabilistic timed automata. In: Ouaknine J, Vaandrager F (eds) Proc of 7th int conf on formal modelling and analysis of timed systems (FORMATS\u201909). LNCS, vol\u00a05813. Springer, Berlin, pp\u00a0212\u2013227"},{"key":"177_CR51","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Proc of 23rd int conf 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 of 23rd int conf on computer aided verification (CAV\u201911). LNCS, vol\u00a06806. Springer, Berlin, pp\u00a0585\u2013591"},{"key":"177_CR52","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska M, Norman G, Parker D, Sproston J (2006) Performance analysis of probabilistic timed automata using digital clocks. Form Methods Syst Des 29:33\u201378","journal-title":"Form Methods Syst Des"},{"key":"177_CR53","series-title":"LNCS","first-page":"123","volume-title":"Proc of 11th international conference on concurrency theory (CONCUR\u201900)","author":"M Kwiatkowska","year":"2000","unstructured":"Kwiatkowska M, Norman G, Segala R, Sproston J (2000) Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi C (ed) Proc of 11th international conference on concurrency theory (CONCUR\u201900). LNCS, vol\u00a01877. Springer, Berlin, pp\u00a0123\u2013137"},{"key":"177_CR54","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska M, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282:101\u2013150","journal-title":"Theor Comput Sci"},{"issue":"3","key":"177_CR55","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"M Kwiatkowska","year":"2003","unstructured":"Kwiatkowska M, Norman G, Sproston J (2003) Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Form Asp Comput 14(3):295\u2013318","journal-title":"Form Asp Comput"},{"issue":"7","key":"177_CR56","doi-asserted-by":"crossref","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska M, Norman G, Sproston J, Wang F (2007) Symbolic model checking for probabilistic timed automata. Inf Comput 205(7):1027\u20131077","journal-title":"Inf Comput"},{"key":"177_CR57","series-title":"ENTCS","first-page":"113","volume-title":"Proc of second workshop on quantitative aspects of programming languages (QAPL 2004)","author":"R Lanotte","year":"2005","unstructured":"Lanotte R, Maggiolo-Schettini A, Troina A (2005) Automatic analysis of a non-repudiation protocol. In: Proc of second workshop on quantitative aspects of programming languages (QAPL 2004). ENTCS, vol\u00a0112, pp\u00a0113\u2013129"},{"key":"177_CR58","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K Larsen","year":"1991","unstructured":"Larsen K, Skou A (1991) Bisimulation through probabilistic testing. Inf Comput 94:1\u201328","journal-title":"Inf Comput"},{"issue":"2","key":"177_CR59","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1006\/inco.1997.2623","volume":"134","author":"K Larsen","year":"1997","unstructured":"Larsen K, Yi W (1997) Time-abstracted bisimulation: implicit specifications and decidability. Inf Comput 134(2):75\u2013101","journal-title":"Inf Comput"},{"key":"177_CR60","first-page":"33","volume-title":"Proc of 12th int workshop on verification of infinite-state systems (INFINITY\u201910), EPTCS","author":"O Maler","year":"2010","unstructured":"Maler O, Larsen K, Krogh B (2010) On zone-based analysis of duration probabilistic automata. In: Proc of 12th int workshop on verification of infinite-state systems (INFINITY\u201910), EPTCS, vol\u00a039, pp\u00a033\u201346"},{"key":"177_CR61","volume-title":"Proc of 2nd workshop on security in communication networks","author":"O Markowitch","year":"1999","unstructured":"Markowitch O, Roggeman Y (1999) Probabilistic non-repudiation without trusted third party. In: Proc of 2nd workshop on security in communication networks"},{"issue":"2","key":"177_CR62","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala R, Lynch N (1995) Probabilistic simulations for probabilistic processes. Nord J Comput 2(2):250\u2013273","journal-title":"Nord J Comput"},{"key":"177_CR63","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"620","DOI":"10.1007\/978-3-642-04081-8_41","volume-title":"Proc of 20th int conf on concurrency theory (CONCUR 2009)","author":"J Sproston","year":"2009","unstructured":"Sproston J (2009) Strict divergence for probabilistic timed automata. In: Bravetti M, Zavattaro G (eds) Proc of 20th int conf on concurrency theory (CONCUR 2009). LNCS, vol\u00a05710. Springer, Berlin, pp\u00a0620\u2013636"},{"key":"177_CR64","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1109\/QEST.2011.18","volume-title":"Proc of 8th int conf on quantitative evaluation of systems (QEST\u201911)","author":"J Sproston","year":"2011","unstructured":"Sproston J (2011) Discrete-time verification and control for probabilistic rectangular hybrid automata. In: Proc of 8th int conf on quantitative evaluation of systems (QEST\u201911). IEEE Press, New York, pp\u00a079\u201388"},{"key":"177_CR65","unstructured":"Tripakis S (1998) The analysis of timed systems in practice. PhD thesis, Universit\u00e9 Joseph Fourier, Grenoble"},{"key":"177_CR66","series-title":"LNCS","first-page":"299","volume-title":"Proc of 5th int AMAST workshop on real-time and probabilistic systems (ARTS\u201999)","author":"S Tripakis","year":"1999","unstructured":"Tripakis S (1999) Verifying progress in timed systems. In: Katoen JP (ed) Proc of 5th int AMAST workshop on real-time and probabilistic systems (ARTS\u201999). LNCS, vol\u00a01601. Springer, Berlin, pp\u00a0299\u2013314"},{"issue":"3","key":"177_CR67","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/s10703-005-1632-8","volume":"26","author":"S Tripakis","year":"2005","unstructured":"Tripakis S, Yovine S, Bouajjani A (2005) Checking timed B\u00fcchi automata emptiness efficiently. Form Methods Syst Des 26(3):267\u2013292","journal-title":"Form Methods Syst Des"},{"key":"177_CR68","unstructured":"UPPAAL PRO web site. http:\/\/people.cs.aau.dk\/~arild\/uppaal-probabilistic\/"},{"key":"177_CR69","first-page":"205","volume-title":"Proc of 4th workshop on quantitative aspects of programming languages (QAPL 06), ENTCS","author":"M Zhang","year":"2006","unstructured":"Zhang M, Hung DV (2006) Formal analysis of streaming downloading protocol for system upgrading. In: Proc of 4th workshop on quantitative aspects of programming languages (QAPL 06), ENTCS, vol\u00a0164, pp\u00a0205\u2013224"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0177-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0177-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0177-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T18:06:08Z","timestamp":1594749968000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0177-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,12]]},"references-count":69,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["177"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0177-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,12]]}}}