{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:03:07Z","timestamp":1776304987171,"version":"3.50.1"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T00:00:00Z","timestamp":1149638400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,7]]},"DOI":"10.1007\/s10703-006-0005-2","type":"journal-article","created":{"date-parts":[[2006,6,6]],"date-time":"2006-06-06T20:15:56Z","timestamp":1149624956000},"page":"33-78","source":"Crossref","is-referenced-by-count":134,"title":["Performance analysis of probabilistic timed automata using digital clocks"],"prefix":"10.1007","volume":"29","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","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":[[2006,6,7]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill, \u201cModel-checking in dense real-time,\u201d Inform. Comp., Vol. 104, No. 1, pp. 2\u201334, 1993.","DOI":"10.1006\/inco.1993.1024"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and D. Dill, \u201cA theory of timed automata,\u201d Theor. Comp. Sci., Vol. 126, pp. 183\u2013235, 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger, \u201cReactive modules,\u201d Formal Meth. in Sys. Desi., Vol. 15, No. 1, pp. 7\u201348, 1999.","DOI":"10.1023\/A:1008739929481"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur, A. Itai, R. Kurshan, and M. Yannakakis, \u201cTiming verification by successive approximation,\u201d Inform. Comp., Vol. 18, No. 1, pp. 142\u2013157, 1995.","DOI":"10.1006\/inco.1995.1059"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"R. Alur, S. La Torre, and G. Pappas, \u201cOptimal paths in weighted timed automata. in Benedetto and Sangiovanni-Vincentelli [11], pp. 49\u201362.","DOI":"10.1007\/3-540-45351-2_8"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"S. Andova, H. Hermanns, and J.-P. Katoen, \u201cDiscrete-time rewards model-checked,\u201d in K. Larsen and P. Niebert (Eds.), Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03), Vol. 2791 of LNCS, Springer-Verlag, 2003, pp. 88\u2013104","DOI":"10.1007\/978-3-540-40903-8_8"},{"key":"5_CR7","unstructured":"E. Asarin, O. Maler, and A. Pnueli, \u201cOn discretization of delays in timed automata and digital circuits,\u201d in R. de Simone and D. Sangiorgi (Eds.), Proc. 9th Int. Conf. Concurrency Theory (CONCUR'98), Vol. 1466 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 470\u2013484."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"C. Baier and M. Kwiatkowska, \u201cModel checking for a probabilistic branching time logic with fairness,\u201d Distr. Comp., Vol. 11, pp. 125\u2013155, 1998.","DOI":"10.1007\/s004460050046"},{"key":"5_CR9","unstructured":"G. Behrmann, A. Fehnker, T. Hune, K. Larsen, P. Pettersson, and J. Romijn, \u201cEfficient guiding towards cost-optimality in UPPAAL,\u201d in T. Margaria and W. Yi (Eds.), Proc. 7th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), Vol. 2031 of Lecture Notes in Computer Science, Springer-Verlag, 2001, pp. 174\u2013188."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"G. Behrmann, A. Fehnker, T. Hune, K. Larsen, P. Pettersson, J. Romijn, and F. Vaandrager, \u201cMinimum-cost reachability for linearly priced timed automata in Benedetto and Sangiovanni-Vincentelli [11], pp. 147\u2013162.","DOI":"10.1007\/3-540-45351-2_15"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"M.D. Benedetto and A. Sangiovanni-Vincentelli (Eds). in Proc. 4th Int. Workshop on Hybrid Systems: Computation and Control (HSCC'01), Vol. 2034 of Lecture Notes in Computer Science. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45351-2"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"D. Bertsekas and J. Tsitsiklis, \u201cAn analysis of stochastic shortest path problems,\u201d Math. Oper. Res., Vol. 16, No. 3, pp. 580\u2013595, 1991.","DOI":"10.1287\/moor.16.3.580"},{"key":"5_CR13","unstructured":"D. Beyer, \u201cImprovements in BDD-based reachability analysis of timed automata,\u201d in J. Oliveira and P. Zave (Eds.), Proc. Symp. Formal Methods Europe (FME'01), Vol. 2021 of Lecture Notes in Computer Science, Springer-Verlag, 2001, pp. 318\u2013343."},{"key":"5_CR14","unstructured":"D. Beyer and A. Noack, \u201cEfficient verification of timed automata using BDDs,\u201d in S. Gnesi and U. Ultes-Nitsche (Eds.), Proc. Formal Methods for Industrial Critical Systems (FMICS'01), 2001, pp. 95\u2013113."},{"key":"5_CR15","unstructured":"A. Bianco and L. de Alfaro, \u201cModel checking of probabilistic and nondeterministic systems,\u201d in P. Thiagarajan (Ed.), Proc. Foundations of Software Technology and Theoretical Computer Science, Vol. 1026 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 499\u2013513."},{"key":"5_CR16","unstructured":"P. Billingsley, Probability and Measure. John Wiley and Sons: New York, 1979."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"H. Bohnenkamp, P. v. d. Stok, H. Hermanns, and F. Vaandrager, \u201cCost-optimisation of the IPv4 zeroconf protocol,\u201d in Proc. Int. Performance and Dependability Symposium (IPDS'03), pp. 531\u2012540. IEEE Computer Society Press, 2003.","DOI":"10.1109\/DSN.2003.1209963"},{"key":"5_CR18","unstructured":"S. Cheshire, B. Adoba, and E. Guttman, \u201cDynamic configuration of IPv4 link-local addresses (draft August 2002). Zeroconf Working Group of the Internet Engineering Task Force (www.zeroconf.org)."},{"key":"5_CR19","unstructured":"E. Clarke, M. Fujita, P. McGeer, K. McMillan, J. Yang, and X. Zhao, \u201cMulti-terminal binary decision diagrams: An efficient data structure for matrix representation,\u201d in Proc. Int.Workshop on Logic Synthesis (IWLS'93), pp. 1\u201315, 1993. Also available in Form. Meth. in Syst. Des., Vol. 10, No. 2\/3, 1997, pp. 149\u2013169."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"C. Daws, M. Kwiatkowska, and G. Norman, \u201cAutomatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM,\u201d Inte. J. Soft. Tools Technol. Trans. (STTT), Vol. 5, No. 2\u20133, pp. 221\u2013236, 2004.","DOI":"10.1007\/s10009-003-0118-5"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Yovine, \u201cTwo examples of verification of multirate timed automata with KRONOS,\u201d in Proc. IEEE Real-Time Systems Symposium (RTSS'95), IEEE Computer Society Press, 1995, pp. 66\u201375.","DOI":"10.1109\/REAL.1995.495197"},{"key":"5_CR22","unstructured":"L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997."},{"key":"5_CR23","unstructured":"L. de Alfaro, \u201cComputing minimum and maximum reachability times in probabilistic systems,\u201d in J. Baeten and S. Mauw (Eds.), Proc. 10th Int. Conf. Concurrency Theory (CONCUR'99), Vol. 1664 of Lecture Notes in Computer Science, Springer-Verlag, 1999, pp. 66\u201381."},{"key":"5_CR24","unstructured":"C. Derman, Finite-State Markovian Decision Processes. Academic Press: New York, 1970."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"A. G\u00f6ll\u00fc, A. Puri, and P. Varaiya, \u201cDiscretization of timed automata,\u201d in Proc. 33rd IEEE Conf. Decision and Control, IEEE Computer Society Press, 1994, pp. 957\u2013958.","DOI":"10.1109\/CDC.1994.410933"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"P. Halmos. Measure Theory. Springer-Verlag, New York, 1950.","DOI":"10.1007\/978-1-4684-9440-2"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"H. Hansson and B. Jonsson, \u201cA logic for reasoning about time and reliability,\u201d Form. Asp. Comp., Vol. 6, No. 4, pp. 512\u2013535, 1994.","DOI":"10.1007\/BF01211866"},{"key":"5_CR28","unstructured":"T. Henzinger, The Temporal Specification and Verification of Real-time Systems. PhD thesis, Stanford University, 1991."},{"key":"5_CR29","unstructured":"T. Henzinger, P.-H. Ho, and H. Wong-Toi, \u201cA user guide to HYTECH,\u201d in E. Brinksma, R. Cleaveland, and K. Larsen (Eds.), in Proc. 1st Int. Conf. Tools and Algorithms for Construction and Analysis of Systems (TACAS'95), Vol. 1019 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 41\u201371."},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"T. Henzinger, Z. Manna, and A. Pnueli, \u201cWhat good are digital clocks?,\u201d in W. Kuich (Ed.), Proc. 19th Int. Colloquium on Automata, Languages and Programming (ICALP'92), Vol. 623 of Lecture Notes in Computer Science, Springer-Verlag, 1992, pp. 545\u2013558.","DOI":"10.1007\/3-540-55719-9_103"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, \u201cSymbolic model checking for realtime systems,\u201d Inform. Comp., Vol. 111, No. 2, pp. 193\u2013244, 1994.","DOI":"10.1006\/inco.1994.1045"},{"key":"5_CR32","unstructured":"IEEE 1394-1995. High Performance Serial Bus Standard. 1995."},{"key":"5_CR33","unstructured":"IEEE 802.11, Wireless LANMedium Access Control (MAC) and Physical Layer (PHY) Specifications Standard. 1997."},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains, Springer-Verlag: New York, 2nd edn. 1976.","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker, \u201cPRISM 2.0: A tool for probabilistic model checking,\u201d in Proc. 1st International Conference on Quantitative Evaluation of Systems (QEST'04), IEEE Computer Society Press, 2004, pp. 322\u2013323.","DOI":"10.1109\/QEST.2004.1348048"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker, \u201cProbabilistic symbolic model checking with PRISM: A hybrid approach,\u201d Int. J. Soft. Tools Technol. Tran. (STTT), Vol. 6, No. 2, pp. 128\u2013142, 2004.","DOI":"10.1007\/s10009-004-0140-2"},{"key":"5_CR37","unstructured":"M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston, \u201cPerformance analysis of probabilistic timed automata using digital clocks,\u201d in K. Larsen and P. Niebert (Eds.), Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03), Vol. 2791 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 105\u2013120."},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, \u201cAutomatic verification of real-time systems with discrete probability distributions,\u201d Theor. Comp. Sci., Vol. 282, pp. 101\u2013150, 2002.","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"5_CR39","unstructured":"M. Kwiatkowska, G. Norman, and J. Sproston, \u201cSymbolic computation of maximal probabilistic reachability,\u201d in K. Larsen and M. Nielsen (Eds.), Proc. 13th Int. Conf. Concurrency Theory (CONCUR'01), Vol. 2154 of Lecture Notes in Computer Science, Springer-Verlag, 2001, pp. 169\u2013183."},{"key":"5_CR40","unstructured":"M. Kwiatkowska, G. Norman, and J. Sproston, \u201cProbabilistic model checking of the IEEE802.11 wireless local area network protocol,\u201d in H. Hermanns and R. Segala (Eds.), Proc. 2nd Joint Int. Workshop Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBM 4'02), Vol. 2399 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pp. 169\u2013187."},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, and J. Sproston, \u201cProbabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol,\u201d Form. Asp. Comp., Vol. 14, pp. 295\u2013318, 2003.","DOI":"10.1007\/s001650300007"},{"key":"5_CR42","unstructured":"M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang, \u201cSymbolic model checking for probabilistic timed automata,\u201d in Y. Lakhnech and S. Yovine (Eds.), Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), Vol. 3253 of LNCS, Springer, 2004, pp. 293\u2013308."},{"key":"5_CR43","unstructured":"K. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune, P. Pettersson, and J. Romijn, \u201cAs cheap as possible: Efficient cost-optimal reachability for priced timed automata,\u201d in G. Berry, H. Comon, and A. Finkel (Eds.), in Proc. 13th Int. Conf. Computer Aided Verification (CAV'01), Vol. 2102 of Lect. Notes in Comp. Sci., Springer-Verlag, 2001, pp. 493\u2013505."},{"key":"5_CR44","doi-asserted-by":"crossref","unstructured":"K. Larsen, P. Pettersson, and W. Yi, \u201cUPPAAL in a nutshell,\u201d Soft. Tools Technolo. Tran., Vol. 1, No. 1\u20132, pp. 134\u2013152, 1997.","DOI":"10.1007\/s100090050010"},{"key":"5_CR45","unstructured":"J. Ouaknine, \u201cDigitisation and full abstraction for dense-time model checking,\u201d in J.-P. Katoen and P. Stevens (Eds.), Proc. 8th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02), Vol. 2280 of Lect. Notes in Comp. Sci., Springer-Verlag, 2002, pp. 37\u201351."},{"key":"5_CR46","unstructured":"D. Parker. Implementation of Symbolic Model Checking for Probabilistic Sys. PhD thesis, University of Birmingham, 2002."},{"key":"5_CR47","unstructured":"PRISM web page. www.cs.bham.ac.uk\/~dxp\/prism."},{"key":"5_CR48","unstructured":"UPPAAL web page. www.uppaal.com."},{"key":"5_CR49","unstructured":"A. Schrijver. Theory of Linear and Integer Programming. J.Wiley and Sons: New York, 1986."},{"key":"5_CR50","unstructured":"R. Segala. Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995."},{"key":"5_CR51","unstructured":"R. Segala and N.A. Lynch, \u201cProbabilistic simulations for probabilistic processes,\u201d Nordic J. Comp., Vol. 2, No. 2, pp. 250\u2013273, 1995."},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"D. Simons and M.I.A. Stoelinga, \u201cMechanical verification of the IEEE 1394a root contention protocol using UPPAAL2k,\u201d Soft. Tools Technolo. Trans., Vo l. 3, No. 4, pp. 469\u2013485, 2001.","DOI":"10.1007\/s100090100059"},{"key":"5_CR53","unstructured":"M. Stoelinga. Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, University of Nijmegen, the Netherlands, 2002."},{"key":"5_CR54","unstructured":"M. Zhang and F. Vaandrager, \u201cAnalysis of a protocol for dynamic configuration of IPv4 link local addresses using UPPAAL,\u201d Technical Report, NIII-R04XX, University of Nijmegen, 2004."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0005-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0005-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0005-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T06:30:43Z","timestamp":1736404243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0005-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6,7]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,7]]}},"alternative-id":["5"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0005-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,6,7]]}}}