{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T20:10:07Z","timestamp":1746389407519,"version":"3.40.4"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319113128"},{"type":"electronic","value":"9783319113135"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-11313-5_22","type":"book-chapter","created":{"date-parts":[[2014,9,23]],"date-time":"2014-09-23T23:05:40Z","timestamp":1411513540000},"page":"231-242","source":"Crossref","is-referenced-by-count":1,"title":["Fixed-Point Methods in Parametric Model Checking"],"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","reference":[{"issue":"3","key":"22_CR1","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1145\/377978.377990","volume":"2","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Torre, S.L., Peled, D.: Parametric Temporal Logic for \u201cModel Measuring\u201d. ACM Trans. Comput. Log.\u00a02(3), 388\u2013407 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T., Vardi, M.: Parametric real-time reasoning. In: Proc. of the 25th Ann. Symp. on Theory of Computing (STOC 1993), pp. 592\u2013601. ACM (1993)","DOI":"10.1145\/167088.167242"},{"issue":"1","key":"22_CR3","doi-asserted-by":"crossref","first-page":"19","DOI":"10.3233\/FI-2011-576","volume":"112","author":"F. Belardinelli","year":"2011","unstructured":"Belardinelli, F., Jones, A.V., Lomuscio, A.: Model checking temporal-epistemic logic using alternating tree automata. Fundam. Inform.\u00a0112(1), 19\u201337 (2011)","journal-title":"Fundam. Inform."},{"issue":"2","key":"22_CR4","doi-asserted-by":"publisher","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. Form. Methods Syst. Des.\u00a035(2), 121\u2013151 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1007\/3-540-36494-3_60","volume-title":"STACS 2003","author":"V. Bruy\u00e8re","year":"2003","unstructured":"Bruy\u00e8re, V., Dall\u2019Olio, E., Raskin, J.F.: Durations, parametric model-checking in timed automata with presburger arithmetic. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 687\u2013698. Springer, Heidelberg (2003)"},{"issue":"2","key":"22_CR6","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1990)","journal-title":"Information and Computation"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69850-0_1","volume-title":"25 Years of Model Checking","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp. 1\u201326. Springer, Heidelberg (2008)"},{"key":"22_CR8","first-page":"321","volume-title":"Proc. of the 33rd Int. Conf. on Software Engineering, ICSE 2011","author":"A. Classen","year":"2011","unstructured":"Classen, A., Heymans, P., Schobbens, P.Y., Legay, A.: Symbolic model checking of software product lines. In: Proc. of the 33rd Int. Conf. on Software Engineering, ICSE 2011, pp. 321\u2013330. ACM, New York (2011)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Trefler, R.: Parametric quantitative temporal reasoning. In: Proc. of the 14th Symp. on Logic in Computer Science (LICS 1999), pp. 336\u2013343. IEEE Computer Society (July 1999)","DOI":"10.1109\/LICS.1999.782628"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Ghallab, M., Nau, D.S., Traverso, P.: Automated planning - theory and practice. Elsevier (2004)","DOI":"10.1016\/B978-155860856-6\/50021-1"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-13089-2_21","volume-title":"Language and Automata Theory and Applications","author":"B. Di Giampaolo","year":"2010","unstructured":"Di Giampaolo, B., La Torre, S., Napoli, M.: Parametric metric interval temporal logic. In: Dediu, A.-H., Fernau, H., Mart\u00edn-Vide, C. (eds.) LATA 2010. LNCS, vol.\u00a06031, pp. 249\u2013260. Springer, Heidelberg (2010)"},{"issue":"1","key":"22_CR12","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1109\/52.108773","volume":"9","author":"G.J. Holzmann","year":"1992","unstructured":"Holzmann, G.J.: Protocol design: Redefining the state of the art. IEEE Software\u00a09(1), 17\u201322 (1992)","journal-title":"IEEE Software"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Transactions on Petri Nets and Other Models of Concurrency IV","year":"2010","unstructured":"Jensen, K., Donatelli, S., Koutny, M. (eds.): Transactions on Petri Nets and Other Models of Concurrency IV. LNCS, vol.\u00a06550. Springer, Heidelberg (2010)"},{"key":"22_CR14","unstructured":"Jones, A.V., Knapik, M., Penczek, W., Lomuscio, A.: Parametric computation tree logic with knowledge. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2011), pp. 286\u2013300. Bia\u0142ystok University of Technology (2011)"},{"key":"22_CR15","unstructured":"Knapik, M., https:\/\/michalknapik.github.io\/spatula"},{"issue":"1-2","key":"22_CR16","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.\u00a0101(1-2), 9\u201327 (2010)","journal-title":"Fundam. Inform."},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Knapik, M., M\u0119ski, A., Penczek, W.: Action synthesis for branching time logic: Theory and applications. In: Proc. of the 14th Int. Conf. on Application of Concurrency to System Design. IEEE Computer Society (to appear, 2014)","DOI":"10.1109\/ACSD.2014.22"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Knapik, M., Szreter, M., Penczek, W.: Bounded parametric model checking for elementary net systems. In: T. Petri Nets and Other Models of Concurrency [13], pp. 42\u201371","DOI":"10.1007\/978-3-642-18222-8_3"},{"issue":"5","key":"22_CR19","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1145\/55483.55496","volume":"17","author":"F.J. Lin","year":"1987","unstructured":"Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: The state space explosion problem and relief strategies. SIGCOMM Comput. Commun. Rev.\u00a017(5), 126\u2013135 (1987)","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"22_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-74128-2_8","volume-title":"Model Checking and Artificial Intelligence","author":"C. Pecheur","year":"2007","unstructured":"Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol.\u00a04428, pp. 113\u2013128. Springer, Heidelberg (2007)"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All From One, One For All: On Model Checking Using Representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Penczek, W., P\u00f3lrola, A., Zbrzezny, A.: Sat-based (parametric) reachability for a class of distributed time petri nets. In: T. Petri Nets and Other Models of Concurrency [13], pp. 72\u201397","DOI":"10.1007\/978-3-642-18222-8_4"},{"key":"22_CR23","unstructured":"Somenzi, F.: CUDD: CU decision diagram package - release 2.3.1., http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cuddIntro.html"},{"issue":"2","key":"22_CR24","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1006\/inco.1996.0086","volume":"130","author":"F. Wang","year":"1996","unstructured":"Wang, F.: Parametric timing analysis for real-time systems. Inf. Comput.\u00a0130(2), 131\u2013150 (1996)","journal-title":"Inf. Comput."},{"issue":"1","key":"22_CR25","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. Formal Methods in System Design\u00a017(1), 39\u201360 (2000)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"22_CR26","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/1047659.1040334","volume":"40","author":"Y. Xie","year":"2005","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. SIGPLAN Not.\u00a040(1), 351\u2013363 (2005)","journal-title":"SIGPLAN Not."}],"container-title":["Advances in Intelligent Systems and Computing","Intelligent Systems'2014"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11313-5_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T19:43:04Z","timestamp":1746387784000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-11313-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319113128","9783319113135"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11313-5_22","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"type":"print","value":"2194-5357"},{"type":"electronic","value":"2194-5365"}],"subject":[],"published":{"date-parts":[[2015]]}}}