{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T00:10:02Z","timestamp":1748823002529,"version":"3.41.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319301648"},{"type":"electronic","value":"9783319301655"}],"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-30165-5_1","type":"book-chapter","created":{"date-parts":[[2016,3,25]],"date-time":"2016-03-25T10:53:13Z","timestamp":1458903193000},"page":"3-21","source":"Crossref","is-referenced-by-count":2,"title":["SMT-Based Parameter Synthesis for Parametric Timed Automata"],"prefix":"10.1007","author":[{"given":"Micha\u0142","family":"Knapik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,26]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T., Vardi, M.: Parametric real-time reasoning. In: Proceedings of the 25th Annual Symposium on Theory of Computing, pp. 592\u2013601. ACM (1993)","DOI":"10.1145\/167088.167242"},{"issue":"5","key":"1_CR2","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"\u00c9 Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, \u00c9., Chatain, T., Fribourg, L., Encrenaz, E.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819\u2013836 (2009)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"1_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Technical report. Department of Computer Science, The University of Iowa, available at www.SMT-LIB.org (2010)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Proceedings of the 19th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4590, pp. 298\u2013302. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Bozzelli, L., La Torre, S.: Decision problems for lower\/upper bound parametric timed automata. Form. Methods Syst. Des. 35(2), 121\u2013151 (2009). http:\/\/dx.doi.org\/10.1007\/s10703-009-0074-0","DOI":"10.1007\/s10703-009-0074-0"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Satisfiability modulo theories: an appetizer. Formal Methods: Foundations and Applications. In: 12th Brazilian Symposium on Formal Methods, (SBMF), Revised Selected Papers. Lecture Notes in Computer Science, vol. 5902, pp. 23\u201336. Springer (2009)","DOI":"10.1007\/978-3-642-10452-7_3"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52\u201353","author":"T Hune","year":"2002","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52\u201353, 183\u2013220 (2002)","journal-title":"J. Log. Algebr. Program."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Jovanovic, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 7795, pp. 401\u2013415. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_28"},{"key":"1_CR9","unstructured":"Knapik, M.: https:\/\/michalknapik.github.io\/PTA2SMT"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-29072-5_6","volume":"5","author":"M Knapik","year":"2012","unstructured":"Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. Trans. Petri Nets Models Concurr. 5, 141\u2013159 (2012)","journal-title":"Trans. Petri Nets Models Concurr."},{"key":"1_CR11","unstructured":"Knapik, M., Penczek, W.: SMT-based parameter synthesis for L\/U automata. In: Proceedings of the International Workshop on Petri Nets and Software Engineering, vol. 851, pp. 77\u201392. CEUR, Hamburg, 25\u201326 June 2012"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Knapik, M., Penczek, W.: Parameter synthesis for timed Kripke structures. Fundam. Inform. 133(2\u20133), 211\u2013226 (2014). http:\/\/dx.doi.org\/10.3233\/FI-2014-1072","DOI":"10.3233\/FI-2014-1072"},{"issue":"1\u20132","key":"1_CR13","doi-asserted-by":"crossref","first-page":"9","DOI":"10.3233\/FI-2010-272","volume":"101","author":"M Knapik","year":"2010","unstructured":"Knapik, M., Penczek, W., Szreter, M., P\u00f3lrola, A.: Bounded parametric verification for distributed time petri nets with discrete-time semantics. Fundam. Inform. 101(1\u20132), 9\u201327 (2010)","journal-title":"Fundam. Inform."},{"key":"1_CR14","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/978-3-642-18222-8_3","volume":"4","author":"M Knapik","year":"2010","unstructured":"Knapik, M., Szreter, M., Penczek, W.: Bounded parametric model checking for elementary net systems. Trans. Petri Nets Models Concurr. 4, 42\u201371 (2010)","journal-title":"Trans. Petri Nets Models Concurr."},{"issue":"1\u20132","key":"1_CR15","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR16","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/978-3-642-18222-8_4","volume":"4","author":"W Penczek","year":"2010","unstructured":"Penczek, W., P\u00f3lrola, A., Zbrzezny, A.: SAT-based (parametric) reachability for a class of distributed time petri nets. Trans. Petri Nets Models Concurr. 4, 72\u201397 (2010)","journal-title":"Trans. Petri Nets Models Concurr."},{"issue":"1\u20134","key":"1_CR17","doi-asserted-by":"crossref","first-page":"425","DOI":"10.3233\/FUN-2008-851-429","volume":"85","author":"W Penczek","year":"2008","unstructured":"Penczek, W., Szreter, M.: SAT-based unbounded model checking of timed automata. Fundam. Inform. 85(1\u20134), 425\u2013440 (2008)","journal-title":"Fundam. Inform."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Spelberg, R.F.L., Toetenel, W.J.: Splitting trees and partition refinement in real-time model checking. In: 35th Hawaii International Conference on System Sciences (HICSS-35 2002), CD-ROM\/Abstracts Proceedings, Big Island, HI, USA. p. 278, IEEE Computer Society, 7\u201310 January 2002. http:\/\/dx.doi.org\/10.1109\/HICSS.2002.994478","DOI":"10.1109\/HICSS.2002.994478"},{"issue":"1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1023\/A:1008734703554","volume":"18","author":"S Tripakis","year":"2001","unstructured":"Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Form. Methods Syst. Design 18(1), 25\u201368 (2001)","journal-title":"Form. Methods Syst. Design"},{"issue":"1","key":"1_CR20","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/A:1008782501688","volume":"17","author":"F Wang","year":"2000","unstructured":"Wang, F.: Parametric analysis of computer systems. Form. Methods Syst. Design 17(1), 39\u201360 (2000)","journal-title":"Form. Methods Syst. Design"},{"issue":"1\u20133","key":"1_CR21","first-page":"303","volume":"67","author":"A Zbrzezny","year":"2005","unstructured":"Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundam. Inform. 67(1\u20133), 303\u2013322 (2005)","journal-title":"Fundam. Inform."}],"container-title":["Studies in Computational Intelligence","Challenging Problems and Solutions in Intelligent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30165-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T23:45:54Z","timestamp":1748821554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30165-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319301648","9783319301655"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30165-5_1","relation":{},"ISSN":["1860-949X","1860-9503"],"issn-type":[{"type":"print","value":"1860-949X"},{"type":"electronic","value":"1860-9503"}],"subject":[],"published":{"date-parts":[[2016]]}}}