{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:09:21Z","timestamp":1761610161619,"version":"build-2065373602"},"reference-count":22,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3893,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s1571-0661(04)80406-7","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"104-119","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":5,"title":["Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM"],"prefix":"10.1016","volume":"66","author":[{"given":"Conrado","family":"Daws","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/S1571-0661(04)80406-7_NEWBIB1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","article-title":"Model-checking in dense real-time","volume":"104","author":"Alur","year":"1993","journal-title":"Information and Computation"},{"issue":"2","key":"10.1016\/S1571-0661(04)80406-7_NEWBIB2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/S1571-0661(04)80406-7_NEWBIB3","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","article-title":"Reactive modules","volume":"15","author":"Alur","year":"1999","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB4","doi-asserted-by":"crossref","unstructured":"C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In Proc. CAV'00, LNCS, 2000.","DOI":"10.1007\/10722167_28"},{"issue":"3","key":"10.1016\/S1571-0661(04)80406-7_NEWBIB5","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s004460050046","article-title":"Model checking for a probabilistic branching time logic with fairness","volume":"11","author":"Baier","year":"1998","journal-title":"Distributed Computing"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB6","doi-asserted-by":"crossref","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In P. S. Thiagarajan, editor, Proceedings of FSTTCS'95, volume 1026 of LNCS, pages 499\u2013513. Springer-Verlag, 1995.","DOI":"10.21236\/ADA461346"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB7","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In R. Alur, T. A. Henzinger, and E. D. Sontag, editors, Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science, pages 208\u2013219. Springer-Verlag, 1996.","DOI":"10.1007\/BFb0020947"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB8","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Tripakis. Model\u2014checking of real\u2014time reachability properties using abstractions. In B. Steffen, editor, Proc. TACAS'98, volume 1384 of LNCS, pages 313\u2013329. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0054180"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB9","doi-asserted-by":"crossref","unstructured":"L. de Alfaro. Computing minimum and maximum reachability times in probabilistic systems. In J. Baeten and S. Mauw, editors, Proceedings of CONCUR'99, volume 1664 of LNCS, pages 66\u201381. Springer Verlag, 1999.","DOI":"10.1007\/3-540-48320-9_7"},{"issue":"1+2","key":"10.1016\/S1571-0661(04)80406-7_NEWBIB10","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","article-title":"HyTech: a model checker for hybrid systems","volume":"1","author":"Henzinger","year":"1997","journal-title":"Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB11","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6_4","article-title":"Denumerable Markov Chains","author":"Kemeny","year":"1976"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB12","unstructured":"KRONOS web page. http:\/\/www-verimag.imag.fr\/TEMPORISE\/kronos\/."},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB13","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In J. B. T. Field, P. Harrison and U. Harder, editors, Proc. TOOLS 2002, volume 2324 of LNCS, pages 200\u2013204. Springer, 2002.","DOI":"10.1007\/3-540-46029-2_13"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB14","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In J.-P. Katoen and P. Stevens, editors, Proc. TACAS 2002, volume 2280 of LNCS, pages 52\u201366. Springer, 2002.","DOI":"10.1007\/3-540-46002-0_5"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB15","unstructured":"M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of deadline properties in the IEEE 1394 firewire root contention protocol. In Proc. Int. Workshop on Application of Formal Methods to IEEE 1394 Standard, 2001."},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB16","series-title":"Automatic verification of real-time systems with discrete probability distributions. volume 1601 of LNCS","first-page":"75","author":"Kwiatkowska","year":"1999"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB17","article-title":"Automatic verification of real-time systems with discrete probability distributions","volume":"286","author":"Kwiatkowska","year":"2002","journal-title":"Theoretical Computer Science"},{"issue":"1+2","key":"10.1016\/S1571-0661(04)80406-7_NEWBIB18","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"Uppaal in a nutshell","volume":"1","author":"Larsen","year":"1997","journal-title":"Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB19","unstructured":"PRISM web page. http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/."},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB20","doi-asserted-by":"crossref","unstructured":"D. Simons and M. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Springer International Journal of Software Tools for Technology Transfer, 2001. To appear.","DOI":"10.1007\/s100090100059"},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB21","unstructured":"M. Stoelinga. Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, Univerisity of Nijmegen, 2002."},{"key":"10.1016\/S1571-0661(04)80406-7_NEWBIB22","doi-asserted-by":"crossref","unstructured":"M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings FOCS'85. IEEE Computer Society Press, 1985.","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804067?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804067?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:04:58Z","timestamp":1761609898000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104804067"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S1571066104804067"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80406-7","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80406-7","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}