{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T02:06:13Z","timestamp":1790647573186,"version":"4.1.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415901","type":"print"},{"value":"9783319415918","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41591-8_12","type":"book-chapter","created":{"date-parts":[[2016,6,23]],"date-time":"2016-06-23T17:27:27Z","timestamp":1466702847000},"page":"172-187","source":"Crossref","is-referenced-by-count":13,"title":["LTL Parameter Synthesis of Parametric Timed Automata"],"prefix":"10.1007","author":[{"given":"Peter","family":"Bezd\u011bk","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikola","family":"Bene\u0161","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,6,23]]},"reference":[{"key":"12_CR1","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"2","key":"12_CR2","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.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Daws","year":"1998","unstructured":"Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313\u2013329. Springer, Heidelberg (1998)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST, pp. 125\u2013126. IEEE (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, pp. 592\u2013601. ACM (1993)","DOI":"10.1145\/167088.167242"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-46430-1_26","volume-title":"Hybrid Systems: Computation and Control","author":"JS Miller","year":"2000","unstructured":"Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, p. 296. Springer, Heidelberg (2000)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/978-3-662-47666-6_6","volume-title":"Automata, Languages, and Programming","author":"N Bene\u0161","year":"2015","unstructured":"Bene\u0161, N., Bezd\u011bk, P., Larsen, K.G., Srba, J.: Language emptiness of continuous-time parametric timed automata. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 69\u201381. Springer, Heidelberg (2015)"},{"key":"12_CR8","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52","author":"T Hune","year":"2002","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. J. Logic Algebraic Programm. 52, 183\u2013220 (2002)","journal-title":"J. Logic Algebraic Programm."},{"issue":"2","key":"12_CR9","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/s10703-009-0074-0","volume":"35","author":"L Bozzelli","year":"2009","unstructured":"Bozzelli, L., La Torre, S.: Decision problems for lower\/upper bound parametric timed automata. Formal Methods Syst. Des. 35(2), 121\u2013151 (2009)","journal-title":"Formal Methods Syst. Des."},{"issue":"5","key":"12_CR10","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1109\/TSE.2014.2357445","volume":"41","author":"A Jovanovic","year":"2015","unstructured":"Jovanovic, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Trans. Softw. Eng. 41(5), 445\u2013461 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"12_CR11","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.: Checking timed b\u00fcchi automata emptiness efficiently. Formal Methods Syst. Des. 26(3), 267\u2013292 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"issue":"3","key":"12_CR13","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1023\/B:FORM.0000026093.21513.31","volume":"24","author":"P Bouyer","year":"2004","unstructured":"Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods Syst. Des. 24(3), 281\u2013320 (2004)","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"12_CR14","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/s10009-005-0190-0","volume":"8","author":"G Behrmann","year":"2006","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pel\u00e1nek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8(3), 204\u2013215 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-642-04368-0_18","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G Li","year":"2009","unstructured":"Li, G.: Checking timed B\u00fcchi automata emptiness using LU-abstractions. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 228\u2013242. Springer, Heidelberg (2009)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Bezd\u011bk, P., Bene\u0161, N., Barnat, J., \u010cern\u00e1, I.: LTL parameter synthesis of parametric timed automata. CoRR abs\/1409.3696 (2016)","DOI":"10.1007\/978-3-319-41591-8_12"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","first-page":"233","volume-title":"Computer-Aided Verification","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV. LNCS, vol. 531, pp. 233\u2013242. Springer, Heidelberg (1992)"},{"issue":"1\u20132","key":"12_CR18","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Programm. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Programm."},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 53. Springer, Heidelberg (2001)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-3-319-10882-7_4","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2014","author":"P Bezd\u011bk","year":"2014","unstructured":"Bezd\u011bk, P., Bene\u0161, N., Havel, V., Barnat, J., \u010cern\u00e1, I.: On clock-aware LTL properties of timed automata. In: Ciobanu, G., M\u00e9ry, D. (eds.) ICTAC 2014. LNCS, vol. 8687, pp. 43\u201360. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41591-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T22:34:14Z","timestamp":1748990054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41591-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415901","9783319415918"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41591-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}