{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:40:05Z","timestamp":1742755205117,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642290718"},{"type":"electronic","value":"9783642290725"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29072-5_6","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T18:18:02Z","timestamp":1332440282000},"page":"141-159","source":"Crossref","is-referenced-by-count":21,"title":["Bounded Model Checking 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","reference":[{"issue":"3","key":"6_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2006.12.019","volume":"174","author":"E. \u00c1brah\u00e1m","year":"2007","unstructured":"\u00c1brah\u00e1m, E., Herbstritt, M., Becker, B., Steffen, M.: Bounded model checking with parametric data structures. Electr. Notes Theor. Comput. Sci.\u00a0174(3), 3\u201316 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"6_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"6_CR3","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":"5","key":"6_CR4","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"E. Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, E., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. International Journal of Foundations of Computer Science\u00a020(5), 819\u2013836 (2009)","journal-title":"International Journal of Foundations of Computer Science"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: TREX: A Tool for Reachability Analysis of Complex Systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 368\u2013372. Springer, Heidelberg (2001)"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers\u00a058, 118\u2013149 (2003)","journal-title":"Advances in Computers"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Blunno, I., Cortadella, J., Kondratyev, A., Lavagno, L., Lwin, K., Sotiriou, C.P.: Handshake protocols for de-synchronization. In: Proc. of 10th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2004), pp. 149\u2013158 (2004)","DOI":"10.1109\/ASYNC.2004.1299296"},{"issue":"8","key":"6_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. on Computers"},{"issue":"1","key":"6_CR9","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"6_CR10","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":"6_CR11","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1016\/j.ipl.2006.11.018","volume":"102","author":"L. Doyen","year":"2007","unstructured":"Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett.\u00a0102, 208\u2013213 (2007)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"6_CR12","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.: Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Science of Computer Programming"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-78929-1_14","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2008","unstructured":"Frehse, G., Jha, S.K., Krogh, B.H.: A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol.\u00a04981, pp. 187\u2013200. Springer, Heidelberg (2008)"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1109\/92.502196","volume":"4","author":"S.B. Furber","year":"1996","unstructured":"Furber, S.B., Day, P.: Four-phase micropipeline latch control circuits. IEEE Trans. Very Large Scale Integr. Syst.\u00a04, 247\u2013253 (1996)","journal-title":"IEEE Trans. Very Large Scale Integr. Syst."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"T. Henzinger","year":"1997","unstructured":"Henzinger, T., Ho, P., Wong-Toi, H.: HyTech: A Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 460\u2013463. Springer, Heidelberg (1997)"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52-53","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\u00a052-53, 183\u2013220 (2002)","journal-title":"J. Log. Algebr. Program"},{"key":"6_CR17","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":"6_CR18","first-page":"879","volume-title":"Proc. of the 2004 Asia and South Pacific Design Automation Conference, ASP-DAC 2004","author":"R. Li","year":"2004","unstructured":"Li, R., Zhou, D., Du, D.: Satisfiability and integer programming as complementary tools. In: Proc. of the 2004 Asia and South Pacific Design Automation Conference, ASP-DAC 2004, pp. 879\u2013882. IEEE Press, Piscataway (2004)"},{"issue":"1-2","key":"6_CR19","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":"6_CR20","unstructured":"Spelberg, R.L., De Rooij, R.C.H., Toetenel, W.J.: Application of parametric model checking - the root contention protocol using LPMC. In: Proc. of the 7th ASCI Conference, Beekbergen, The Netherlands, pp. 73\u201385 (Febuary 2000)"},{"key":"6_CR21","doi-asserted-by":"crossref","first-page":"115","DOI":"10.3233\/FI-2010-300","volume":"102","author":"M. Srebrny","year":"2010","unstructured":"Srebrny, M., Stepie\u0144, L.: SAT as a programming environment for linear algebra. Fundamenta Informaticae\u00a0102, 115\u2013127 (2010)","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"6_CR22","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s001650300009","volume":"14","author":"M. Stoelinga","year":"2003","unstructured":"Stoelinga, M.: Fun with firewire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Formal Asp. Comput.\u00a014(3), 328\u2013337 (2003)","journal-title":"Formal Asp. Comput."},{"key":"6_CR23","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)"},{"issue":"1","key":"6_CR24","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. Formal Methods in System Design\u00a018(1), 25\u201368 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"1-2","key":"6_CR25","doi-asserted-by":"crossref","first-page":"229","DOI":"10.3233\/FUN-2007-791-211","volume":"79","author":"B. Wo\u017ana","year":"2007","unstructured":"Wo\u017ana, B., Zbrzezny, A.: Bounded model checking for the existential fragment of TCTL_G and diagonal timed automata. Fundamenta Informaticae\u00a079(1-2), 229\u2013256 (2007)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency V"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29072-5_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:25:07Z","timestamp":1742754307000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29072-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642290718","9783642290725"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29072-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}