{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,14]],"date-time":"2025-04-14T04:26:20Z","timestamp":1744604780593},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418658"},{"type":"electronic","value":"9783540453192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_14","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:50:47Z","timestamp":1184601047000},"page":"189-203","source":"Crossref","is-referenced-by-count":25,"title":["Linear Parametric Model Checking of Timed Automata"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Hune","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Judi","family":"Romijn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mari\u00ebelle","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, and M.Y. Vardi. Parametric real-time reasoning. In Proc. 25th Annual Symp. on Theory of Computing, pages 592\u2013601. ACM Press, 1993.","DOI":"10.1145\/167088.167242"},{"key":"14_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/10722167_32","volume-title":"Proc. 12th Int. Conference on Computer Aided Verification","author":"A. Annichini","year":"2000","unstructured":"A. Annichini, E. Asarin, and A. Bouajjani. Symbolic techniques for parametric reasoning about counter and clock systems. In Proc. 12th Int. Conference on Computer Aided Verification, LNCS 1855, pages 419\u2013434. Springer-Verlag, 2000."},{"key":"14_CR4","unstructured":"G. Bandini, R. Lutje Spelberg, and H. Toetenel. Parametric verification of the IEEE 1394a root contention protocol using LPMC. http:\/\/tvs.twi.tudelft.nl\/ , July 2000. Submitted."},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Proc. 10th Int. Conference on Computer Aided Verification","author":"M. Bozga","year":"1998","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A Model-Checking Tool for Real-Time Systems. In Proc. 10th Int. Conference on Computer Aided Verification, LNCS 1427, pages 546\u2013550. Springer-Verlag, June\/July 1998."},{"key":"14_CR6","unstructured":"T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. McGraw-Hill, Inc., 1991."},{"key":"14_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/BFb0035403","volume-title":"Proc. Third Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"P.R. D\u2019Argenio","year":"1997","unstructured":"P.R. D\u2019Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In Proc. Third Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1217, pages 416\u2013431. Springer-Verlag, April 1997."},{"key":"14_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Proc. Int. Workshop on Automatic Verification Methods for Finite State Systems","author":"D. Dill","year":"1990","unstructured":"D. Dill. Timing assumptions and verification of finite-state concurrent systems. In Proc. Int. Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, pages 197\u2013212. Springer-Verlag, 1990."},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Proc. 9th Int. Conference on Computer Aided Verification","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A Model Checker for Hybrid Systems. In Proc. 9th Int. Conference on Computer Aided Verification, LNCS 1254, pages 460\u2013463. Springer-Verlag, 1997."},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"T.S. Hune, J.M.T. Romijn, M.I.A. Stoelinga, and F.W. Vaandrager. Linear parametric model checking of timed automata. Report CSI-R0102, CSI, University of Nijmegen, January 2001.","DOI":"10.7146\/brics.v8i5.20459"},{"issue":"1\u20132","key":"14_CR11","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1\u20132):134\u2013152, October 1997.","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"14_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/BFb0055344","volume-title":"Proc. FTRTFT\u201998","author":"R.F. Lutje Spelberg","year":"1998","unstructured":"R.F. Lutje Spelberg, W.J. Toetenel, and M. Ammerlaan. Partition refinement in real-time model checking. In Proc. FTRTFT\u201998, LNCS 1486, pages 143\u2013157. Springer-Verlag, 1998."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"D.P.L. Simons and M.I.A. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Technical Report CSI-R0009, CSI, University of Nijmegen, May 2000. Conditionally accepted for STTT.","DOI":"10.1007\/s100090100059"},{"key":"14_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-48778-6_4","volume-title":"Proc. 5th Int. AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems","author":"M.I.A. Stoelinga","year":"1999","unstructured":"M.I.A. Stoelinga and F.W. Vaandrager. Root contention in IEEE 1394. In Proc. 5th Int. AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601, pages 53\u201374. Springer-Verlag, 1999."},{"key":"14_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-65193-4_20","volume-title":"Lectures on Embedded Systems","author":"S. Yovine","year":"1998","unstructured":"S. Yovine. Model checking timed automata. In Lectures on Embedded Systems, LNCS 1494, pages 114\u2013152. Springer-Verlag, October 1998."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45319-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T01:32:28Z","timestamp":1587778348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}