{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:35:57Z","timestamp":1784241357658,"version":"3.55.0"},"reference-count":28,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4034,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["The Journal of Logic and Algebraic Programming"],"published-print":{"date-parts":[[2002,7]]},"DOI":"10.1016\/s1567-8326(02)00037-1","type":"journal-article","created":{"date-parts":[[2002,10,8]],"date-time":"2002-10-08T16:46:42Z","timestamp":1034095602000},"page":"183-220","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":110,"special_numbering":"C","title":["Linear parametric model checking of timed automata"],"prefix":"10.1016","volume":"52-53","author":[{"given":"Thomas","family":"Hune","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Judi","family":"Romijn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mari\u00eblle","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/S1567-8326(02)00037-1_BIB1","series-title":"Proceedings of the 12th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1855","first-page":"419","article-title":"Symbolic techniques for parametric reasoning about counter and clock systems","author":"Annichini","year":"2000"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB2","series-title":"Proceedings of the International Conference on Computer Aided Verification (CAV\u201901), Paris, France, Lecture Notes in Computer Science, vol. 1855","article-title":"TReX: a tool for reachability analysis of complex systems","author":"Annichini","year":"2001"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB3","series-title":"Proceedings of the 17th ICALP, Warwick, Lecture Notes in Computer Science, vol. 443","first-page":"322","article-title":"Automata for modeling real-time systems","author":"Alur","year":"1990"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB4","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":"Theoret. Comput. Sci."},{"key":"10.1016\/S1567-8326(02)00037-1_BIB5","series-title":"in: Proceedings of the 25th Annual Symposium on Theory of Computing","first-page":"592","article-title":"Parametric real-time reasoning","author":"Alur","year":"1993"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB6","series-title":"Proceedings REX Workshop on Real-Time: Theory in Practice, Mook, The Netherlands, June 1991, Lecture Notes in Computer Science, vol. 600","first-page":"1","article-title":"An old-fashioned recipe for real time","author":"Abadi","year":"1992"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB7","unstructured":"R. Alur, Timed automata, in: NATO-ASI Summer School on Verification of Digital and Hybrid Systems, Springer, Berlin, 1998, to appear"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB8","series-title":"Proceedings of the 10th International Conference on Computer Aided Verification, Vancouver, BC, Canada, Lecture Notes in Computer Science, vol. 1427","first-page":"546","article-title":"Kronos: A model-checking tool for real-time systems","author":"Bozga","year":"1998"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB9","unstructured":"G. Bandini, R.L. Lutje Spelberg, R.C.H. de Rooij, W.J. Toetenel, Application of Parametric Model Checking\u2014The Root Contention Protocol using {LPMC}, in: Proceedings of the 34th Hawaii International Conference on System Sciences (HICCS\u201901), 2001"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB10","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB11","series-title":"Introduction to Algorithms","author":"Cormen","year":"1991"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB12","unstructured":"A. Collomb\u2013Annichini, M. Sighireanu, Parameterized reachability analysis of the IEEE 1394 Root Contention Protocol using TReX, in: P. Pettersson, S. Yovine (Eds.), Proceedings of the Workshop on Real-Time Tools (RT-TOOLS\u20192001), 2001"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB13","series-title":"Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, Lecture Notes in Computer Science, vol. 407","first-page":"197","article-title":"Timing assumptions and verification of finite-state concurrent systems","author":"Dill","year":"1990"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB14","series-title":"Proceedings of the Third Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Enschede, The Netherlands, Lecture Notes in Computer Science, vol. 1217","first-page":"416","article-title":"The bounded retransmission protocol must be on time!","author":"D\u2019Argenio","year":"1997"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB15","series-title":"Proceedings of the 9th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 1254","first-page":"460","article-title":"HyTech: A model checker for hybrid systems","author":"Henzinger","year":"1997"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB16","series-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Genova, Italy, Lecture Notes in Computer Science, vol. 2031","first-page":"189","article-title":"Linear parametric model checking of timed automata","author":"Hune","year":"2001"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB17","unstructured":"IEEE Computer Society. IEEE Standard for a High Performance Serial Bus. Std 1394\u20131995, August 1996"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB18","series-title":"Proceedings TAPSOFT\u201997: Theory and Practice of Software Development, Lille, France, Lecture Notes in Computer Science, vol. 1214","first-page":"565","article-title":"A compositional proof of a real-time mutual exclusion protocol","author":"Kristoffersen","year":"1997"},{"issue":"1","key":"10.1016\/S1567-8326(02)00037-1_BIB19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/7351.7352","article-title":"A fast mutual exclusion algorithm","volume":"5","author":"Lamport","year":"1987","journal-title":"ACM Trans. Comput. Syst."},{"key":"10.1016\/S1567-8326(02)00037-1_BIB20","series-title":"in: Proceedings of the 18th IEEE Real-Time Systems Symposium","first-page":"14","article-title":"Efficient verification of real-time systems: Compact data structures and state-space reduction","author":"Larsen","year":"1997"},{"issue":"1\u20132","key":"10.1016\/S1567-8326(02)00037-1_BIB21","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":"Int. J. Software Tools Technol. Transfer"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB22","series-title":"Proceedings of the Fifth International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT\u201998), Lyngby, Denmark, Lecture Notes in Computer Science, vol. 1486","first-page":"143","article-title":"Partition refinement in real-time model checking","author":"Lutje Spelberg","year":"1998"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB23","series-title":"Distributed Algorithms","author":"Lynch","year":"1996"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB24","series-title":"Proceedings CONCUR 91, Amsterdam, Lecture Notes in Computer Science, vol. 527","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-54430-5_103","article-title":"Time constrained automata","author":"Merritt","year":"1991"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB25","doi-asserted-by":"crossref","unstructured":"D.P.L. Simons, M.I.A. Stoelinga, Mechanical verification of the IEEE 1394a Root Contention Protocol using Uppaal2k. Springer International Journal on Software Tools for Technology Transfer (STTT) 3 (2001) 469\u2013485","DOI":"10.1007\/s100090100059"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB26","doi-asserted-by":"crossref","unstructured":"M.I.A. Stoelinga, Fun with FireWire: a comparative study of formal verification methods applied to the IEEE 1394 Root Contention Protocol, Formal Aspects of Computing, to appear (2002)","DOI":"10.1007\/s001650300009"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB27","series-title":"Proceedings of the 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, Bamberg, Germany, Lecture Notes in Computer Science, vol. 1601","first-page":"53","article-title":"Root contention in IEEE 1394","author":"Stoelinga","year":"1999"},{"key":"10.1016\/S1567-8326(02)00037-1_BIB28","series-title":"Lectures on Embedded Systems, Lecture Notes in Computer Science, vol. 1494","first-page":"114","article-title":"Model checking timed automata","author":"Yovine","year":"1998"}],"container-title":["The Journal of Logic and Algebraic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1567832602000371?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1567832602000371?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T18:34:29Z","timestamp":1761590069000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1567832602000371"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,7]]},"references-count":28,"alternative-id":["S1567832602000371"],"URL":"https:\/\/doi.org\/10.1016\/s1567-8326(02)00037-1","relation":{},"ISSN":["1567-8326"],"issn-type":[{"value":"1567-8326","type":"print"}],"subject":[],"published":{"date-parts":[[2002,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Linear parametric model checking of timed automata","name":"articletitle","label":"Article Title"},{"value":"The Journal of Logic and Algebraic Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1567-8326(02)00037-1","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 Inc.","name":"copyright","label":"Copyright"}]}}