{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:31:12Z","timestamp":1762101072290},"publisher-location":"Berlin, Heidelberg","reference-count":93,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540222361"},{"type":"electronic","value":"9783540277934"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27793-4_4","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T22:49:31Z","timestamp":1283726971000},"page":"37-76","source":"Crossref","is-referenced-by-count":24,"title":["Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata"],"prefix":"10.1007","author":[{"given":"Wojciech","family":"Penczek","sequence":"first","affiliation":[]},{"given":"Agata","family":"P\u00f3\u0142rola","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-45740-2_5","volume-title":"Applications and Theory of Petri Nets 2001","author":"P.A. Abdulla","year":"2001","unstructured":"Abdulla, P.A., Nyl\u00e9n, A.: Timed Petri Nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol.\u00a02075, pp. 53\u201370. Springer, Heidelberg (2001)"},{"key":"4_CR2","first-page":"414","volume-title":"Proc. of LICS 1990","author":"R. Alur","year":"1990","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model checking for real-time systems. In: Proc. of LICS 1990, pp. 414\u2013425. IEEE, Los Alamitos (1990)"},{"issue":"1","key":"4_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real-time. Information and Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"4_CR4","first-page":"157","volume-title":"Proc. of 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 RTSS 1992, pp. 157\u2013166. IEEE Comp. Soc. Press, Los Alamitos (1992)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/BFb0084802","volume-title":"CONCUR \u201992","author":"R. Alur","year":"1992","unstructured":"Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: Minimization of timed transition systems. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 340\u2013354. Springer, Heidelberg (1992)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modelling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 322\u2013335. Springer, Heidelberg (1990)"},{"issue":"3","key":"4_CR7","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"Alur, R., Henzinger, T., Ho, P.: Automatic symbolic verification of embedded systems. IEEE Trans. on Software Eng.\u00a022(3), 181\u2013201 (1996)","journal-title":"IEEE Trans. on Software Eng."},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0020948","volume-title":"Hybrid Systems III","author":"R. Alur","year":"1996","unstructured":"Alur, R., Kurshan, R.: Timing analysis in COSPAN. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 220\u2013231. Springer, Heidelberg (1996)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"Hybrid and Real-Time Systems","author":"E. Asarin","year":"1997","unstructured":"Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Datastructures for the verification of Timed Automata. In: Maler, O. (ed.) HART 1997. LNCS, vol.\u00a01201, pp. 346\u2013360. Springer, Heidelberg (1997)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-36135-9_16","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 243\u2013259. Springer, Heidelberg (2002)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using Clock Difference Diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 341\u2013353. Springer, Heidelberg (1999)"},{"key":"4_CR12","unstructured":"Bengtsson, J.: Clocks, DBMs and States in Timed Systems. PhD thesis, Dept. of Information Technology, Uppsala University (2002)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-39893-6_28","volume-title":"Formal Methods and Software Engineering","author":"J. Bengtsson","year":"2003","unstructured":"Bengtsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis in Timed Automata. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 491\u2013503. Springer, Heidelberg (2003)"},{"issue":"3","key":"4_CR14","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using Time Petri Nets. IEEE Trans. on Software Eng.\u00a017(3), 259\u2013273 (1991)","journal-title":"IEEE Trans. on Software Eng."},{"key":"4_CR15","unstructured":"Berthomieu, B., Menasche, M.: An enumerative approach for analyzing Time Petri Nets. In: Proc. of the IFIP 9th World Computer Congress, September 1983. Information Processing, vol.\u00a09, pp. 41\u201346. North Holland\/IFIP (1983)"},{"key":"4_CR16","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 (2004) (to appear)","DOI":"10.1080\/00207540412331312688"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-36577-X_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Berthomieu","year":"2003","unstructured":"Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of Time Petri Nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 442\u2013457. Springer, Heidelberg (2003)"},{"key":"4_CR18","unstructured":"Beyer, D.: Rabbit: Verification of real-time systems. In: Proc. of the Workshop on Real-Time Tools (RT-TOOLS 2001), pp. 13\u201321 (2001)"},{"key":"4_CR19","unstructured":"Bobbio, A., Horv\u00e1th, A.: Model checking time Petri nets using NuSMV. In: Proc. of the 5th Int. Workshop on Performability Modeling of Computer and Communication Systems (PMCCS5), September 2001, pp. 100\u2013104 (2001)"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"Bouajjani, A., Fernandez, J.-C., Halbwachs, N., Raymond, P., Ratel, C.: Minimal state graph generation. Science of Computer Programming\u00a018, 247\u2013269 (1992)","journal-title":"Science of Computer Programming"},{"key":"4_CR21","first-page":"232","volume-title":"Proc. of RTSS 1997","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model checking for real-time systems. In: Proc. of RTSS 1997, pp. 232\u2013243. IEEE Comp. Soc. Press, Los Alamitos (1997)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Boucheneb, H., Berthelot, G.: Towards a simplified building of Time Petri Nets reachability graph. In: Proc. of the 5th Int. Workshop on Petri Nets and Performance Models, October 1993, pp. 46\u201355 (1993)","DOI":"10.1109\/PNPM.1993.393436"},{"key":"4_CR23","unstructured":"Bowden, F.: Modelling time in Petri nets. In: Proc. of the 2nd Australia-Japan Workshop on Stochastic Models (STOMOD 1996) (July 1996)"},{"issue":"8","key":"4_CR24","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 Transaction on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transaction on Computers"},{"key":"4_CR25","unstructured":"Cassez, F., Roux, O.H.: Traduction structurelle des R\u00e9seaux de Petri Temporels vers le Automates Temporis\u00e9s. In: Proc. of 4ieme Colloque Francophone sur la Mod\u00e9lisation des Syst\u00e9mes R\u00e9actifs (MSR 2003). Hermes Science (October 2003)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-44988-4_8","volume-title":"Application and Theory of Petri Nets 2000","author":"G. Ciardo","year":"2000","unstructured":"Ciardo, G., L\u00fcttgen, G., Simniceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 103\u2013122. Springer, Heidelberg (2000)"},{"issue":"5","key":"4_CR27","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1109\/TSE.1983.235261","volume":"SE-9","author":"J. Coolahan","year":"1983","unstructured":"Coolahan, J., Roussopoulos, N.: Timing requirements for time-driven systems using augmented Petri nets. IEEE Trans. on Software Eng.\u00a0SE-9(5), 603\u2013616 (1983)","journal-title":"IEEE Trans. on Software Eng."},{"key":"4_CR28","unstructured":"Cort\u00e9s, L.A., Eles, P., Peng, Z.: Verification of real-time embedded systems using Petri net models and Timed Automata. In: Proc. of the 8th Int. Conf. on Real-Time Computing Systems and Applications (RTCSA 2002), March 2002, pp. 191\u2013199 (2002)"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-48068-4_8","volume-title":"Application and Theory of Petri Nets 2002","author":"J.-M. Couvreur","year":"2002","unstructured":"Couvreur, J.-M., Encrenaz, E., Paviot-Adet, E., Pointrenaud, D., Wacrenier, P.-A.: Data Decision Diagrams for Petri net analysis. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol.\u00a02360, pp. 101\u2013120. Springer, Heidelberg (2002)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Daws","year":"1998","unstructured":"Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 313\u2013329. Springer, Heidelberg (1998)"},{"key":"4_CR31","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. Dembi\u0144ski","year":"2003","unstructured":"Dembi\u0144ski, 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)"},{"issue":"1-2","key":"4_CR32","first-page":"59","volume":"51","author":"P. Dembi\u0144ski","year":"2002","unstructured":"Dembi\u0144ski, P., Penczek, W., P\u00f3\u0142rola, A.: Verification of Timed Automata based on similarity. Fundamenta Informaticae\u00a051(1-2), 59\u201389 (2002)","journal-title":"Fundamenta Informaticae"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","first-page":"281","volume-title":"Proc. of ICALP 1998","author":"M. Dickhofer","year":"1998","unstructured":"Dickhofer, M., Wilke, T.: Timed Alternating Tree Automata: The automatatheoretic solution to the TCTL model checking problem. In: Proc. of ICALP 1998. LNCS, vol.\u00a01664, pp. 281\u2013290. Springer, Heidelberg (1998)"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","first-page":"197","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D. Dill","year":"1989","unstructured":"Dill, D.: Timing assumptions and verification of finite state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1989)"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40903-8_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G. Gardey","year":"2004","unstructured":"Gardey, G., Roux, O.H., Roux, O.F.: Using zone graph method for computing the state space of a Time Petri Net. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791. Springer, Heidelberg (2004)"},{"key":"4_CR36","series-title":"IFIP Conference Proceedings","first-page":"31","volume-title":"Proc. of DIPES 2002","author":"Z. Gu","year":"2002","unstructured":"Gu, Z., Shin, K.: Analysis of event-driven real-time systems with Time Petri Nets. In: Proc. of DIPES 2002. IFIP Conference Proceedings, vol.\u00a0219, pp. 31\u201340. Kluwer, Dordrecht (2002)"},{"key":"4_CR37","unstructured":"Haar, S., Kaiser, L., Simonot-Lion, F., Toussaint, J.: On equivalence between Timed State Machines and Time Petri Nets. Technical Report RR-4049, INRIA Rh\u00f4ne-Alpes, 655, avenue de l\u2019Europe, 38330 Montbonnot-St-Martin (November 2000)"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1007\/3-540-56863-8_52","volume-title":"Application and Theory of Petri Nets 1993","author":"H.-M. Hanisch","year":"1993","unstructured":"Hanisch, H.-M.: Analysis of place\/transition nets with timed arcs and its application to batch process control. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol.\u00a0691, pp. 282\u2013299. Springer, Heidelberg (1993)"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"T. Henzinger","year":"1995","unstructured":"Henzinger, T., Ho, P.: HyTech: The Cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 265\u2013293. Springer, Heidelberg (1995)"},{"issue":"2","key":"4_CR40","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. Henzinger","year":"1994","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation\u00a0111(2), 193\u2013224 (1994)","journal-title":"Information and Computation"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/BFb0054163","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Huhn","year":"1998","unstructured":"Huhn, M., Niebert, P., Wallner, F.: Verification based on local states. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 36\u201351. Springer, Heidelberg (1998)"},{"key":"4_CR42","series-title":"Lecture Notes in Computer Science","first-page":"923","volume-title":"Computer Aided Verification","author":"H. Hulgaard","year":"1995","unstructured":"Hulgaard, H., Burns, S.M.: Efficient timing analysis of a class of Petri Nets. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 923\u2013936. Springer, Heidelberg (1995)"},{"key":"4_CR43","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0304-3975(84)90014-8","volume":"29","author":"R. Janicki","year":"1984","unstructured":"Janicki, R.: Nets, sequential components and concurrency relations. Theoretical Computer Science\u00a029, 87\u2013121 (1984)","journal-title":"Theoretical Computer Science"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Kang, I., Lee, I.: An efficient state space generation for the analysis of real-time systems. In: Proc. of Int. Symposium on Software Testing and Analysis (1996)","DOI":"10.1145\/229000.226297"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","first-page":"514","volume-title":"CONCUR \u201996: Concurrency Theory","author":"O. Kupferman","year":"1996","unstructured":"Kupferman, O., Henzinger, T.A., Vardi, M.Y.: A space-efficient on-the-fly algorithm for real-time model checking. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 514\u2013529. Springer, Heidelberg (1996)"},{"key":"4_CR46","first-page":"14","volume-title":"Proc. of RTSS 1997","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of realtime systems: Compact data structures and state-space reduction. In: Proc. of RTSS 1997, pp. 14\u201324. IEEE Comp. Soc. Press, Los Alamitos (1997)"},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Lee, D., Yannakakis, M.: On-line minimization of transition systems. In: Proc. of the 24th ACM Symp. on the Theory of Computing, May 1992, pp. 264\u2013274 (1992)","DOI":"10.1145\/129712.129738"},{"key":"4_CR48","series-title":"ENTCS","volume-title":"Proc. of MFCS Workshop on Concurrency, Brno 1998","author":"J. Lilius","year":"1999","unstructured":"Lilius, J.: Efficient state space search for Time Petri Nets. In: Proc. of MFCS Workshop on Concurrency, Brno 1998. ENTCS, vol.\u00a018. Elsevier Science Publishers, Amsterdam (1999)"},{"key":"4_CR49","volume-title":"Proc. of the 10th Int. Workshop on Petri Nets and Performance Models (PNPM 2003)","author":"D. Lime","year":"2003","unstructured":"Lime, D., Roux, O.H.: State class timed automaton of a time Petri net. In: Proc. of the 10th Int. Workshop on Petri Nets and Performance Models (PNPM 2003), September 2003. IEEE Comp. Soc. Press, Los Alamitos (2003)"},{"key":"4_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"issue":"9","key":"4_CR51","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","volume":"24","author":"P. Merlin","year":"1976","unstructured":"Merlin, P., Farber, D.J.: Recoverability of communication protocols \u2013 implication of a theoretical study. IEEE Trans. on Communications\u00a024(9), 1036\u20131043 (1976)","journal-title":"IEEE Trans. on Communications"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-48745-X_2","volume-title":"Application and Theory of Petri Nets 1999","author":"A. Miner","year":"1999","unstructured":"Miner, A., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol.\u00a01639, pp. 6\u201325. Springer, Heidelberg (1999)"},{"key":"4_CR53","volume-title":"Proc. of the 2nd IEEE Int. Conf. on Systems, Man and Cybernetics (SMC 2002)","author":"P. Molinaro","year":"2002","unstructured":"Molinaro, P., Roux, D., Delfieu, O.: Improving the calculus of the marking graph of Petri net with BDD like structure. In: Proc. of the 2nd IEEE Int. Conf. on Systems, Man and Cybernetics (SMC 2002), October 2002. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"4_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-48168-0_9","volume-title":"Computer Science Logic","author":"J. M\u00f8ller","year":"1999","unstructured":"M\u00f8ller, J., Lichtenberg, J., Andersen, H., Hulgaard, H.: Difference Decision Diagrams. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 111\u2013125. Springer, Heidelberg (1999)"},{"key":"4_CR55","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, J., Lichtenberg, J., Andersen, H., Hulgaard, H.: Fully symbolic model checking of timed systems using Difference Decision Diagrams. In: Proc. of FLoC 1999. ENTCS, vol.\u00a023(2) (1999)","DOI":"10.1007\/3-540-48168-0_9"},{"key":"4_CR56","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. of the 38th Design Automation Conference (DAC 2001), June 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"4_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-45739-9_15","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"P. Niebert","year":"2002","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of Timed Automata via satisfiability checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 226\u2013243. Springer, Heidelberg (2002)"},{"issue":"4","key":"4_CR58","doi-asserted-by":"crossref","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"},{"issue":"6","key":"4_CR59","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM Journal on Computing\u00a016(6), 973\u2013989 (1987)","journal-title":"SIAM Journal on Computing"},{"key":"4_CR60","unstructured":"Pastor, E., Cortadella, J., Roig, O.: Symbolic Petri net analysis using boolean manipulation. Technical Report RR-97-08, UP\/DAC, Univerisitat Polit\u00e9cnica de Catalunya (February 1997)"},{"key":"4_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-45740-2_19","volume-title":"Applications and Theory of Petri Nets 2001","author":"W. Penczek","year":"2001","unstructured":"Penczek, W., P\u00f3\u0142rola, A.: Abstractions and partial order reductions for checking branching properties of Time Petri Nets. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol.\u00a02075, pp. 323\u2013342. Springer, Heidelberg (2001)"},{"issue":"1-2","key":"4_CR62","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":"4_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45739-9_17","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"W. Penczek","year":"2002","unstructured":"Penczek, W., Wo\u017ana, B., Zbrzezny, A.: Towards bounded model checking for the universal fragment of TCTL. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 265\u2013288. Springer, Heidelberg (2002)"},{"key":"4_CR64","unstructured":"P\u00f3\u0142rola, A., Penczek, W.: Minimization algorithms for Time Petri Nets. Fundamenta Informaticae (2004) (to appear)"},{"issue":"2","key":"4_CR65","first-page":"203","volume":"55","author":"A. P\u00f3\u0142rola","year":"2003","unstructured":"P\u00f3\u0142rola, A., Penczek, W., Szreter, M.: Reachability analysis for Timed Automata using partitioning algorithms. Fundamenta Informaticae\u00a055(2), 203\u2013221 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"4_CR66","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A. P\u00f3\u0142rola","year":"2004","unstructured":"P\u00f3\u0142rola, A., Penczek, W., Szreter, M.: Towards efficient partition refinement for checking reachability in Timed Automata. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791. Springer, Heidelberg (2004)"},{"key":"4_CR67","unstructured":"Popova, L., Marek, S.: TINA - a tool for analyzing paths in TPNs. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2002). Informatik-Berichte, vol.\u00a0110, pp. 195\u2013196. Humboldt University (1998)"},{"key":"4_CR68","unstructured":"Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Technical Report MAC-TR-120, Massachusets Institute of Technology (February 1974)"},{"key":"4_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-44919-1_28","volume-title":"Applications and Theory of Petri Nets 2003","author":"A. Ratzer","year":"2003","unstructured":"Ratzer, A., Wells, L., Lassen, H., Laursen, M., Qvortrup, J., Stissing, M., Westergaard, M., Christensen, S., Jensen, K.: CPN Tools for editing, simulating, and analyzing Coloured Petri Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol.\u00a02679, pp. 450\u2013462. Springer, Heidelberg (2003)"},{"key":"4_CR70","unstructured":"Romeo: A tool for Time Petri Net analysis (2000), http:\/\/www.irccyn.ec-nantes.fr\/irccyn\/d\/en\/equipes\/TempsReel\/logs"},{"key":"4_CR71","unstructured":"Samolej, S., Szmuc, T.: Modelowanie system\u00f3w czasu rzeczywistego z zastosowaniem czasowych sieci Petriego. In: Mat. IX Konf. Systemy Czasu Rzeczywistego (SCR 2002), Instytut Informatyki Politechniki \u015ala\u0327skiej, pp. 45\u201354 (2002) (in Polish)"},{"issue":"5-6","key":"4_CR72","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF02998492","volume":"49","author":"P. S\u00e9nac","year":"1994","unstructured":"S\u00e9nac, P., Diaz, M., de Saqui Sannes, P.: Toward a formal specification of multimedia scenarios. Annals of Telecommunications\u00a049(5-6), 297\u2013314 (1994)","journal-title":"Annals of Telecommunications"},{"key":"4_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-45069-6_16","volume-title":"Computer Aided Verification","author":"S. Seshia","year":"2003","unstructured":"Seshia, S., Bryant, R.: Unbounded, fully symbolic model checking of Timed Automata using boolean methods. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 154\u2013166. Springer, Heidelberg (2003)"},{"key":"4_CR74","series-title":"Lecture Notes in Computer Science","first-page":"347","volume-title":"STACS 96","author":"J. Sifakis","year":"1996","unstructured":"Sifakis, J., Yovine, S.: Compositional specification of timed systems. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol.\u00a01046, pp. 347\u2013359. Springer, Heidelberg (1996)"},{"key":"4_CR75","series-title":"ENTCS","volume-title":"Proc. of MTCS 2002","author":"M. Sorea","year":"2002","unstructured":"Sorea, M.: Bounded model checking for Timed Automata. In: Proc. of MTCS 2002. ENTCS, vol.\u00a068(5). Elsevier Science Publishers, Amsterdam (2002)"},{"key":"4_CR76","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":"4_CR77","series-title":"Lecture Notes in Computer Science","first-page":"756","volume-title":"Proc. of DATE 1999","author":"K. Strehl","year":"1999","unstructured":"Strehl, K., Thiele, L.: Interval diagram techniques for symbolic model checking of Petri nets. In: Proc. of DATE 1999. LNCS, pp. 756\u2013757. IEEE Comp. Soc. Press, Los Alamitos (1999)"},{"key":"4_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S., Bryant, R.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 209\u2013222. Springer, Heidelberg (2002)"},{"issue":"1","key":"4_CR79","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","key":"4_CR80","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/32.341845","volume":"21","author":"J. Tsai","year":"1995","unstructured":"Tsai, J., Yang, S., Chang, Y.: Timing constraint Petri nets and their application to schedulability analysis of real-time system specifications. IEEE Trans. on Software Eng.\u00a021(1), 32\u201349 (1995)","journal-title":"IEEE Trans. on Software Eng."},{"key":"4_CR81","series-title":"Lecture Notes in Computer Science","first-page":"452","volume-title":"Application and Theory of Petri Nets 1993","author":"W. Aalst van der","year":"1993","unstructured":"van der Aalst, W.: Interval timed coloured Petri nets and their analysis. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol.\u00a0691, pp. 452\u2013472. Springer, Heidelberg (1993)"},{"key":"4_CR82","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":"B. Virbitskaite","year":"1999","unstructured":"Virbitskaite, 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)"},{"key":"4_CR83","first-page":"149","volume-title":"Proc. of the 3rd IFIP Workshop on Protocol Specification, Testing, and Verification","author":"B. Walter","year":"1983","unstructured":"Walter, B.: Timed Petri nets for modelling and analysing protocols with real-time characteristics. In: Proc. of the 3rd IFIP Workshop on Protocol Specification, Testing, and Verification, pp. 149\u2013159. North Holland, Amsterdam (1983)"},{"key":"4_CR84","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/CMPSAC.2000.884774","volume-title":"Proc. of the 24th Int. Computer Software and Applications Conf. (COMPSAC 2000)","author":"F. Wang","year":"2000","unstructured":"Wang, F.: Region Encoding Diagram for fully symbolic verification of real-time systems. In: Proc. of the 24th Int. Computer Software and Applications Conf. (COMPSAC 2000), October 2000, pp. 509\u2013515. IEEE Comp. Soc. Press, Los Alamitos (2000)"},{"key":"4_CR85","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-36384-X_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F. Wang","year":"2003","unstructured":"Wang, F.: Verification of Timed Automata with BDD-like data structures. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 189\u2013205. Springer, Heidelberg (2003)"},{"issue":"2","key":"4_CR86","first-page":"223","volume":"55","author":"B. Wo\u017ana","year":"2003","unstructured":"Wo\u017ana, B., Zbrzezny, A., Penczek, W.: Checking reachability properties for Timed Automata via SAT. Fundamenta Informaticae\u00a055(2), 223\u2013241 (2003)","journal-title":"Fundamenta Informaticae"},{"key":"4_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/3-540-56922-7_18","volume-title":"Computer Aided Verification","author":"M. Yannakakis","year":"1993","unstructured":"Yannakakis, M., Lee, D.: An efficient algorithm for minimizing real-time transition systems. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 210\u2013224. Springer, Heidelberg (1993)"},{"key":"4_CR88","series-title":"IFIP Conference Proceedings","first-page":"243","volume-title":"Proc. of the 7th IFIP WG6.1 Int. Conf. on Formal Description Techniques (FORTE 1994)","author":"W. Yi","year":"1994","unstructured":"Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Proc. of the 7th IFIP WG6.1 Int. Conf. on Formal Description Techniques (FORTE 1994). IFIP Conference Proceedings, vol.\u00a06, pp. 243\u2013258. Chapman & Hall, Boca Raton (1994)"},{"key":"4_CR89","first-page":"1","volume":"3","author":"T. Yoneda","year":"1998","unstructured":"Yoneda, T., Ryuba, H.: CTL model checking of Time Petri Nets using geometric regions. IEICE Trans. Inf. and Syst.\u00a03, 1\u201310 (1998)","journal-title":"IEICE Trans. Inf. and Syst."},{"issue":"2","key":"4_CR90","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1023\/A:1008682131325","volume":"11","author":"T. Yoneda","year":"1997","unstructured":"Yoneda, T., Schlingloff, B.H.: Efficient verification of parallel real-time systems. Formal Methods in System Design\u00a011(2), 197\u2013215 (1997)","journal-title":"Formal Methods in System Design"},{"issue":"1\/2","key":"4_CR91","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: KRONOS: A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer\u00a01(1\/2), 123\u2013133 (1997)","journal-title":"Springer International Journal of Software Tools for Technology Transfer"},{"key":"4_CR92","unstructured":"Zbrzezny, A.: Improvements in SAT-based reachability analysis for Timed Automata. Fundamenta Informaticae (2004) (to appear)"},{"key":"4_CR93","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proc. of Int. Conf. on Computer-Aided Design (ICCAD 2001), pp. 279\u2013285 (2001)"}],"container-title":["Lecture Notes in Computer Science","Applications and Theory of Petri Nets 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27793-4_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,8]],"date-time":"2021-11-08T18:02:47Z","timestamp":1636394567000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27793-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222361","9783540277934"],"references-count":93,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27793-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}