{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:45:08Z","timestamp":1787067908108,"version":"3.56.0"},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540222613","type":"print"},{"value":"9783540277552","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27755-2_3","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T23:48:13Z","timestamp":1284421693000},"page":"87-124","source":"Crossref","is-referenced-by-count":390,"title":["Timed Automata: Semantics, Algorithms and Tools"],"prefix":"10.1007","author":[{"given":"Johan","family":"Bengtsson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/BFb0054177","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Aceto","year":"1998","unstructured":"Aceto, L., Bergueno, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 263. Springer, Heidelberg (1998)"},{"key":"3_CR2","first-page":"414","volume-title":"Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science","author":"R. Alur","year":"1990","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pp. 414\u2013425. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"1","key":"3_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.L.: Model-checking in dense real-time. Journal of Information and Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Journal of Information and Computation"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/BFb0015008","volume-title":"CONCUR \u201994: Concurrency Theory","author":"R. Alur","year":"1994","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 162\u2013177. Springer, Heidelberg (1994)"},{"key":"3_CR5","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.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 322\u2013335. Springer, Heidelberg (1990)"},{"issue":"2","key":"3_CR6","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.L.: A theory of timed automata. Journal of Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Journal of Theoretical Computer Science"},{"issue":"1-2","key":"3_CR7","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0304-3975(97)00173-4","volume":"211","author":"R. Alur","year":"1999","unstructured":"Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theoretical Computer Science\u00a0211(1-2), 253\u2013273 (1999)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"3_CR8","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. Journal of the ACM\u00a041(1), 181\u2013204 (1994)","journal-title":"Journal of the ACM"},{"key":"3_CR9","volume-title":"Proceedings, 17th IEEE Real-Time Systems Symposium","author":"F. Balarin","year":"1996","unstructured":"Balarin, F.: Approximate reachability analysis of timed automata. In: Proceedings, 17th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-44829-2_15","volume-title":"Model Checking Software","author":"G. Behrmann","year":"2003","unstructured":"Behrmann, G., David, A., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 225\u2013229. Springer, Heidelberg (2003)"},{"key":"3_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":"3_CR12","volume-title":"Dynamic Programming","author":"R. Bellman","year":"1957","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)"},{"key":"3_CR13","unstructured":"Bengtsson, J.: Reducing memory usage in symbolic state-space exploration for timed systems. Technical Report 2001-009, Department of Information Technology, Uppsala University (2001)"},{"key":"3_CR14","unstructured":"Bengtsson, J.: Clocks, dbms and states in timed systems. Ph.D. Thesis, ACTA Universitatis Upsaliensis 39, Uppsala University (2002)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/BFb0055643","volume-title":"CONCUR \u201998 Concurrency Theory","author":"J. Bengtsson","year":"1998","unstructured":"Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 485\u2013500. Springer, Heidelberg (1998)"},{"key":"3_CR16","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. Bentsson","year":"2003","unstructured":"Bentsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 491\u2013503. Springer, Heidelberg (2003)"},{"issue":"3","key":"3_CR17","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 timed dependent systems using timed petri nets. IEEE Transactions on Software Engineering\u00a017(3), 259\u2013273 (1991)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR18","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/FI-1998-36233","volume":"36","author":"B. B\u00e9rard","year":"1998","unstructured":"B\u00e9rard, B., Diekert, V., Gastin, P., Petit, A.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae\u00a036, 145\u2013182 (1998)","journal-title":"Fundamenta Informaticae"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"K. Cerans","year":"1992","unstructured":"Cerans, K.: Decidability of bisimulation equivalences for parallel timer processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663. Springer, Heidelberg (1992)"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-49253-4_1","volume-title":"Algebraic Methodology and Software Technology","author":"Z. Chaochen","year":"1999","unstructured":"Chaochen, Z.: Duration calculus, a logical approach to real-time systems. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol.\u00a01548, pp. 1\u20137. Springer, Heidelberg (1999)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"David, A., Behrmann, G., Larsen, K.G., Yi, W.: A tool architecture for the next genreation of UPPAAL. Technical Report 2003-011, Department of Information Technology, Uppsala University (2003)","DOI":"10.1007\/978-3-540-40007-3_22"},{"key":"3_CR22","volume-title":"Proceedings, 17th IEEE Real-Time Systems Symposium","author":"C. Daws","year":"1996","unstructured":"Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: Proceedings, 17th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","first-page":"197","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1989","unstructured":"Dill, D.L.: 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":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-46002-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Fersman","year":"2002","unstructured":"Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: Schedulability and decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 67\u201382. Springer, Heidelberg (2002)"},{"issue":"6","key":"3_CR25","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/367766.368168","volume":"5","author":"R.W. Floyd","year":"1962","unstructured":"Floyd, R.W.: Acm algorithm 97: Shortest path. Communications of the ACM\u00a05(6), 345 (1962)","journal-title":"Communications of the ACM"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pp. 394\u2013406 (1992)","DOI":"10.1109\/LICS.1992.185551"},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Journal of Information and Computation\u00a0111(2), 193\u2013244 (1994)","journal-title":"Journal of Information and Computation"},{"issue":"8","key":"3_CR29","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM\u00a021(8), 666\u2013676 (1978)","journal-title":"Communications of the ACM"},{"key":"3_CR30","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"key":"3_CR31","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/REAL.1997.641265","volume-title":"Proceedings, 18th IEEE Real-Time Systems Symposium","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of realtime systems: Compact data structure and state space reduction. In: Proceedings, 18th IEEE Real-Time Systems Symposium, pp. 14\u201324. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nordic Journal of Computing (1999)","DOI":"10.7146\/brics.v5i46.19491"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Petterson, P., Yi, W.: UPPAAL in a nutshell. Journal on Software Tools for Technology Transfer (1997)","DOI":"10.1007\/s100090050010"},{"key":"3_CR34","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1109\/REAL.1995.495198","volume-title":"Proc. of the 16th IEEE Real-Time Systems Symposium","author":"K.G. Larsen","year":"1995","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Compositional and Symbolic Model- Checking of Real-Time Systems. In: Proc. of the 16th IEEE Real-Time Systems Symposium, December 1995, pp. 76\u201387. IEEE Computer Society Press, Los Alamitos (1995)"},{"issue":"2","key":"3_CR35","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1006\/inco.1997.2623","volume":"134","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Wang, Y.: Time-abstracted bisimulation: Implicit specifications and decidability. Information and Computation\u00a0134(2), 75\u2013101 (1997)","journal-title":"Information and Computation"},{"key":"3_CR36","unstructured":"Larsson, F.: Efficient implementation of model-checkers for networks of timed automata. Licentiate Thesis 2000-003, Department of Information Technology, Uppsala University (2000)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BFb0054178","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Lindahl","year":"1998","unstructured":"Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gear-Box Controller. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 281\u2013297. Springer, Heidelberg (1998)"},{"issue":"3","key":"3_CR38","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/s100090100048","volume":"3","author":"M. Lindahl","year":"2001","unstructured":"Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gearbox Controller. Springer International Journal of Software Tools for Technology Transfer (STTT)\u00a03(3), 353\u2013368 (2001)","journal-title":"Springer International Journal of Software Tools for Technology Transfer (STTT)"},{"key":"3_CR39","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"issue":"1","key":"3_CR40","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1006\/inco.1994.1083","volume":"114","author":"X. Nicollin","year":"1994","unstructured":"Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: Theory and application. Journal of Information and Computation\u00a0114(1), 131\u2013178 (1994)","journal-title":"Journal of Information and Computation"},{"key":"3_CR41","unstructured":"Pettersson, P.: Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice. PhD thesis, Uppsala University (1999)"},{"issue":"1-3","key":"3_CR42","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"G.M. Reed","year":"1988","unstructured":"Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theoretical Computer Science\u00a058(1-3), 249\u2013261 (1988)","journal-title":"Theoretical Computer Science"},{"key":"3_CR43","unstructured":"Rokicki, T.G.: Representing and Modeling Digital Circuits. PhD thesis, Stanford University (1993)"},{"key":"3_CR44","series-title":"Lecture Notes in Computer Science","volume-title":"Correct Hardware Design and Verification Methods","author":"U. Stern","year":"1995","unstructured":"Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987. Springer, Heidelberg (1995)"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/3-540-56922-7_6","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1993","unstructured":"Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 59\u201370. Springer, Heidelberg (1993)"},{"key":"3_CR46","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":"3_CR47","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"W. Yi","year":"1991","unstructured":"Yi, W.: CCS + time = an interleaving model for real time systems. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510. Springer, Heidelberg (1991)"},{"key":"3_CR48","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"W. Yi","year":"1994","unstructured":"Yi, W., Jonsson, B.: Decidability of timed language-inclusion for networks of realtime communicating sequen tial processes. In: Thiagarajan, P.S. (ed.) FSTTCS 1994. LNCS, vol.\u00a0880. Springer, Heidelberg (1994)"},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Yi, W., Petterson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Proceedings, Seventh International Conference on Formal Description Techniques, pp. 223\u2013238 (1994)","DOI":"10.1007\/978-0-387-34878-0_18"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Yovine, S.: Kronos: a verification tool for real-time systems. Journal on Software Tools for Technology Transfer\u00a01 (October 1997)","DOI":"10.1007\/s100090050009"}],"container-title":["Lecture Notes in Computer Science","Lectures on Concurrency and Petri Nets"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27755-2_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T15:33:59Z","timestamp":1636472039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27755-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222613","9783540277552"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}