{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:27:15Z","timestamp":1750746435493,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642182211"},{"type":"electronic","value":"9783642182228"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-18222-8_5","type":"book-chapter","created":{"date-parts":[[2010,12,9]],"date-time":"2010-12-09T15:12:06Z","timestamp":1291907526000},"page":"98-120","source":"Crossref","is-referenced-by-count":5,"title":["Parametric Model Checking with VerICS"],"prefix":"10.1007","author":[{"given":"Micha\u0142","family":"Knapik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"Niewiadomski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agata","family":"P\u00f3\u0142rola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maciej","family":"Szreter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","first-page":"414","volume-title":"Proc. of the 5th Symp. on Logic in Computer Science (LICS 1990)","author":"R. Alur","year":"1990","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model checking for real-time systems. In: Proc. of the 5th Symp. on Logic in Computer Science (LICS 1990), pp. 414\u2013425. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"5_CR2","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/REAL.1992.242667","volume-title":"Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS 1992)","author":"R. Alur","year":"1992","unstructured":"Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS 1992), pp. 157\u2013166. IEEE Computer Society Press, Los Alamitos (1992)"},{"key":"5_CR3","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., Weise, C.: New generation of Uppaal. In: Proc. of the Int. Workshop on Software Tools for Technology Transfer (1998)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA - construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research\u00a042(14) (2004)","DOI":"10.1080\/00207540412331312688"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bruy\u00e9re, V., Dall\u2019Olio, E., Raskin, J.-F.: Durations and parametric model-checking in timed automata. ACM Transactions on Computational Logic\u00a09(2) (2008)","DOI":"10.1145\/1342991.1342996"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/BFb0035390","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Christensen","year":"1997","unstructured":"Christensen, S., J\u00f8rgensen, J., Kristensen, L.: Design\/CPN - a computer tool for coloured Petri nets. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 209\u2013223. Springer, Heidelberg (1997)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An openSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-36577-X_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Dembinski","year":"2003","unstructured":"Dembinski, P., Janowska, A., Janowski, P., Penczek, W., P\u00f3\u0142rola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS: A tool for verifying timed automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 278\u2013283. Springer, Heidelberg (2003)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-36577-X_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Dierks","year":"2003","unstructured":"Dierks, H., Tapken, J.: MOBY\/DC - A tool for model-checking parametric real-time specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 271\u2013277. Springer, Heidelberg (2003)"},{"key":"5_CR10","unstructured":"Diethers, K., Goltz, U., Huhn, M.: Model checking UML statecharts with time. In: Proc. of the Workshop on Critical Systems Development with UML (CSDUML 2002), Technische Universit\u00e4t M\u00fcnchen, pp. 35\u201352 (2002)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Dubrovin, J., Junttila, T.: Symbolic model checking of hierarchical UML state machines. Technical Report HUT-TCS-B23, Helsinki Institute of Technology, Espoo, Finland (2007)","DOI":"10.1109\/ACSD.2008.4574602"},{"key":"5_CR12","first-page":"336","volume-title":"Proc. of the 14th Symp. on Logic in Computer Science (LICS 1999)","author":"E.A. Emerson","year":"1999","unstructured":"Emerson, E.A., Trefler, R.: Parametric quantitative temporal reasoning. In: Proc. of the 14th Symp. on Logic in Computer Science (LICS 1999), July 1999, pp. 336\u2013343. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"5_CR13","volume-title":"The Java Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)","edition":"3"},{"issue":"5","key":"5_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Eng."},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-45319-9_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Hune","year":"2001","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 189\u2013203. Springer, Heidelberg (2001)"},{"key":"5_CR16","unstructured":"Jussila, T., Dubrovin, J., Junttila, T., Latvala, T., Porres, I.: Model checking dynamic and hierarchical UML state machines. In: Proc. of the 3rd Int. Workshop on Model Design and Validation (MoDeVa 2006), pp. 94\u2013110. CEA (2006)"},{"issue":"1-4","key":"5_CR17","doi-asserted-by":"crossref","first-page":"313","DOI":"10.3233\/FUN-2008-851-422","volume":"85","author":"M. Kacprzak","year":"2008","unstructured":"Kacprzak, M., Nabia\u0142ek, W., Niewiadomski, A., Penczek, W., P\u00f3\u0142rola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae\u00a085(1-4), 313\u2013328 (2008)","journal-title":"Fundamenta Informaticae"},{"key":"5_CR18","unstructured":"Kacprzak, M., Nabia\u0142ek, W., Niewiadomski, A., Penczek, W., P\u00f3\u0142rola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS 2008 - a model checker for time Petri nets and high-level languages. In: Proc. of Int. Workshop on Petri Nets and Software Engineering (PNSE 2009), pp. 119\u2013132. University of Hamburg (2009)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","first-page":"42","volume-title":"ToPNoC IV","author":"M. Knapik","year":"2011","unstructured":"Knapik, M., Szreter, M., Penczek, W.: Bounded Parametric Model Checking for Elementary Net Systems. In: Jensen, K., Donatelli, S., Koutny, M. (eds.) ToPNoC IV. LNCS, vol.\u00a06550, pp. 42\u201371. Springer, Heidelberg (2011)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45739-9_23","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A. Knapp","year":"2002","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model checking - timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 395\u2013416. Springer, Heidelberg (2002)"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1109\/ASE.1999.802301","volume-title":"Proc. of the 14th IEEE Int. Conf. on Automated Software Engineering (ASE 1999)","author":"J. Lilius","year":"1999","unstructured":"Lilius, J., Paltor, I.: vUML: A tool for verifying UML models. In: Proc. of the 14th IEEE Int. Conf. on Automated Software Engineering (ASE 1999), pp. 255\u2013258. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-00768-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Lime","year":"2009","unstructured":"Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: A parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 54\u201357. Springer, Heidelberg (2009)"},{"key":"5_CR23","unstructured":"MiniSat (2006), http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat"},{"issue":"1-3","key":"5_CR24","doi-asserted-by":"crossref","first-page":"289","DOI":"10.3233\/FI-2009-0103","volume":"93","author":"A. Niewiadomski","year":"2009","unstructured":"Niewiadomski, A., Penczek, W., Szreter, M.: A new approach to model checking of UML state machines. Fundamenta Informaticae\u00a093(1-3), 289\u2013303 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-11486-1_27","volume-title":"Perspectives of Systems Informatics","author":"A. Niewiadomski","year":"2010","unstructured":"Niewiadomski, A., Penczek, W., Szreter, M.: Towards checking parametric reachability for UML state machines. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol.\u00a05947, pp. 319\u2013330. Springer, Heidelberg (2010)"},{"issue":"4","key":"5_CR26","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1002\/(SICI)1520-6440(199704)80:4<11::AID-ECJC2>3.0.CO;2-7","volume":"80","author":"Y. Okawa","year":"1997","unstructured":"Okawa, Y., Yoneda, T.: Symbolic CTL model checking of time Petri nets. Electronics and Communications in Japan, Scripta Technica\u00a080(4), 11\u201320 (1997)","journal-title":"Electronics and Communications in Japan, Scripta Technica"},{"key":"5_CR27","unstructured":"OMG. Unified Modeling Language (2007), http:\/\/www.omg.org\/spec\/UML\/2.1.2"},{"key":"5_CR28","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":"5_CR29","unstructured":"Penczek, W., P\u00f3\u0142rola, A., Wo\u017ana, B., Zbrzezny, A.: Bounded model checking for reachability testing in time Petri nets. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2004). Informatik-Berichte, vol.\u00a0170(1), pp. 124\u2013135. Humboldt University (2004)"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","first-page":"72","volume-title":"ToPNoC IV","author":"W. Penczek","year":"2011","unstructured":"Penczek, W., P\u00f2\u0142rola, A., Zbrzezny, A.: SAT-Based (Parametric) Reachability for a Class of Distributed Time Petri Nets. In: Jensen, K., Donatelli, S., Koutny, M. (eds.) ToPNoC IV. LNCS, vol.\u00a06550, pp. 72\u201397. Springer, Heidelberg (2011)"},{"issue":"1-2","key":"5_CR31","first-page":"135","volume":"51","author":"W. Penczek","year":"2002","unstructured":"Penczek, W., Wo\u017ana, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae\u00a051(1-2), 135\u2013156 (2002)","journal-title":"Fundamenta Informaticae"},{"issue":"1-4","key":"5_CR32","first-page":"307","volume":"60","author":"A. P\u00f3\u0142rola","year":"2004","unstructured":"P\u00f3\u0142rola, A., Penczek, W.: Minimization algorithms for time Petri nets. Fundamenta Informaticae\u00a060(1-4), 307\u2013331 (2004)","journal-title":"Fundamenta Informaticae"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/BFb0055344","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"R.L. Spelberg","year":"1998","unstructured":"Spelberg, R.L., Toetenel, H., Ammerlaan, M.: Partition refinement in real-time model checking. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol.\u00a01486, pp. 143\u2013157. Springer, Heidelberg (1998)"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-85778-5_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"L.-M. Traonouez","year":"2008","unstructured":"Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of time petri nets with stopwatches using the state-class graph. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol.\u00a05215, pp. 280\u2013294. Springer, Heidelberg (2008)"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/3-540-48321-7_46","volume-title":"Fundamentals of Computation Theory","author":"I.B. Virbitskaite","year":"1999","unstructured":"Virbitskaite, I.B., Pokozy, E.A.: A partial order method for the verification of time petri nets. In: Ciobanu, G., P\u0103un, G. (eds.) FCT 1999. LNCS, vol.\u00a01684, pp. 547\u2013558. Springer, Heidelberg (1999)"},{"issue":"1-3","key":"5_CR36","first-page":"303","volume":"67","author":"A. Zbrzezny","year":"2005","unstructured":"Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae\u00a067(1-3), 303\u2013322 (2005)","journal-title":"Fundamenta Informaticae"},{"issue":"1-4","key":"5_CR37","doi-asserted-by":"crossref","first-page":"513","DOI":"10.3233\/FUN-2008-851-435","volume":"85","author":"A. Zbrzezny","year":"2008","unstructured":"Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae\u00a085(1-4), 513\u2013531 (2008)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency IV"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18222-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T16:09:29Z","timestamp":1740758969000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18222-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642182211","9783642182228"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18222-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}