{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T05:40:10Z","timestamp":1740807610125,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"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_3","type":"book-chapter","created":{"date-parts":[[2010,12,9]],"date-time":"2010-12-09T15:12:06Z","timestamp":1291907526000},"page":"42-71","source":"Crossref","is-referenced-by-count":3,"title":["Bounded Parametric Model Checking for Elementary Net Systems"],"prefix":"10.1007","author":[{"given":"Micha\u0142","family":"Knapik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maciej","family":"Szreter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","first-page":"592","volume-title":"Proc. of the 25th Ann. Symp. on Theory of Computing (STOC 1993)","author":"R. Alur","year":"1993","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, New York (1993)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-36577-X_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Benedetti","year":"2003","unstructured":"Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 18\u201333. Springer, Heidelberg (2003)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. of the ACM\/IEEE Design Automation Conference (DAC 1999), pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"issue":"2","key":"3_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1342991.1342996","volume":"9","author":"V. Bruy\u00e9re","year":"2008","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), 1\u201321 (2008)","journal-title":"ACM Transactions on Computational Logic"},{"key":"3_CR6","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), pp. 336\u2013343. IEEE Computer Society Press, Los Alamitos (July 1999)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/3-540-44685-0_15","volume-title":"CONCUR 2001 - Concurrency Theory","author":"K. Heljanko","year":"2001","unstructured":"Heljanko, K.: Bounded reachability checking with process semantics. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 218\u2013232. Springer, Heidelberg (2001)"},{"key":"3_CR8","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":"3_CR9","unstructured":"MiniSat (2006), http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9409","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. 9409\u20139423. Springer, Heidelberg (1993)"},{"issue":"1-2","key":"3_CR11","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"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-24597-1_9","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"V. Bruy\u00e8re","year":"2003","unstructured":"Bruy\u00e8re, V., Raskin, J.-F.: Real-time model-checking: Parameters everywhere. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 100\u2013111. Springer, Heidelberg (2003)"},{"key":"3_CR13","unstructured":"Wo\u017ana, B.: ACTL* properties and bounded model checking. In: Czaja, L. (ed.) Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2003), vol.\u00a02, pp. 591\u2013605. Warsaw University (2003)"},{"issue":"1-4","key":"3_CR14","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_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T16:09:21Z","timestamp":1740758961000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18222-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642182211","9783642182228"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18222-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}