{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:06:24Z","timestamp":1767999984279,"version":"3.49.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,1]]},"DOI":"10.1023\/a:1008734703554","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"25-68","source":"Crossref","is-referenced-by-count":94,"title":["Analysis of Timed Systems Using Time-Abstracting Bisimulations"],"prefix":"10.1007","volume":"18","author":[{"given":"Stavros","family":"Tripakis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Yovine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"281738_CR1","unstructured":"A. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, \u201cAn implementation of three algorithms for timing verification based on automata emptiness,\u201d in RTSS'92. IEEE, 1992."},{"issue":"1","key":"281738_CR2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D.L. Dill, \u201cModel checking in dense real time,\u201d Information and Computation, Vol. 104, No. 1, pp. 2\u201334, 1993.","journal-title":"Information and Computation"},{"key":"281738_CR3","first-page":"340","volume":"630","author":"R. Alur","year":"1992","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, D.L. Dill, and H. Wong-Toi, \u201cMinimization of timed transition systems,\u201d in 3rd Conference on Concurrency Theory CONCUR '92. Lecture Notes in Computer Science, Springer-Verlag, 1992, Vol. 630, pp. 340\u2013354.","journal-title":"3rd Conference on Concurrency Theory CONCUR '92"},{"key":"281738_CR4","unstructured":"R. Alur and D. Dill, \u201cAutomata for modeling real-time systems,\u201d in 17th ICALP, LNCS, Vol. 443, 1990."},{"key":"281738_CR5","first-page":"1","volume":"600","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport, \u201cAn old-fashioned recipe for real time,\u201d in REX workshop \u201cReal-time: Theory in Practice\u201d. LNCS, Vol. 600, Springer-Verlag, 1991, pp. 1\u201327.","journal-title":"REX workshop \u201cReal-time: Theory in Practice"},{"key":"281738_CR6","unstructured":"Rajeev Alur, \u201cTechniques for automatic verification of real-time systems,\u201d Ph.D. Thesis, Department of Computer Science, Stanford University, 1991."},{"key":"281738_CR7","doi-asserted-by":"crossref","unstructured":"J.B. Burch, E.M. Clarke, D. Dill, L.J. Hwang, and K.L. McMillan, \u201cSymbolic model checking: 1020 states and beyond,\u201d in 5th LICS, IEEE, 1990, pp. 428\u2013439.","DOI":"10.1109\/LICS.1990.113767"},{"key":"281738_CR8","doi-asserted-by":"crossref","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine, \u201cKRONOS: A model-checking tool for real-time systems,\u201d in CAV'98, 1998.","DOI":"10.1007\/BFb0028779"},{"key":"281738_CR9","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"A. Bouajjani, J.C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel, \u201cMinimal state graph generation,\u201d Science of Computer Programming, Vol. 18, pp. 247\u2013269, 1992.","journal-title":"Science of Computer Programming"},{"key":"281738_CR10","doi-asserted-by":"crossref","unstructured":"G. Behrmann, K. Larsen, J. Pearson, C. Weise, and W. Yi, \u201cEfficient timed reachability analysis using clock difference diagrams,\u201d in CAV'99, 1999.","DOI":"10.1007\/3-540-48683-6_30"},{"key":"281738_CR11","unstructured":"S. Bornot, \u201cDe la composition des syst`emes hybrides,\u201d Ph.D. Thesis, Universit\u00b4e Joseph Fourrier de Grenoble, 1998. In French."},{"key":"281738_CR12","doi-asserted-by":"crossref","unstructured":"S. Bornot and J. Sifakis, \u201cRelating time progress and deadlines in hybrid systems,\u201d in InternationalWorkshop, HART'97, Grenoble, France, March 1997. Lecture Notes in Computer Science, Vol. 1201, Spinger-Verlag, pp. 286\u2013300.","DOI":"10.1007\/BFb0014733"},{"key":"281738_CR13","unstructured":"S. Bornot, J. Sifakis, and S. Tripakis, \u201cModeling urgency in timed systems,\u201d in Compositionality, LNCS, Vol. 1536, to appear."},{"key":"281738_CR14","unstructured":"A. Bouajjani, S. Tripakis, and S. Yovine, \u201cOn-the-fly symbolic model checking for real-time systems,\u201d in Proc. of the 18th IEEE Real-Time Systems Symposium, San Francisco, CA, Dec. 1997, pp. 232\u2013243."},{"key":"281738_CR15","unstructured":"J.R. B\u00fcchi, \u201cOn a decision method in restricted second-order arithmetic,\u201d in Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science 1960, Stanford University Press, 1962, pp. 1\u201312."},{"key":"281738_CR16","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, \u201cMemory efficient algorithms for the verification of temporal properties,\u201d Formal Methods in System Design, Vol. 1, pp. 275\u2013288, 1992. A preliminary version appeared in the Proceedings of CAV'90 (also in, LNCS, Springer Verlag).","journal-title":"Formal Methods in System Design"},{"key":"281738_CR17","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume":"407","author":"D.L. Dill","year":"1992","unstructured":"D.L. Dill, \u201cTiming assumptions and verification of finite-state concurrent systems,\u201d in Automatic Verification Methods for Finite State Systems, J. Sifakis (Ed.), Lecture Notes in Computer Science, Vol. 407, Springer-Verlag, 1989, pp. 197\u2013212.","journal-title":"Automatic Verification Methods for Finite State Systems"},{"key":"281738_CR18","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Tripakis, \u201cModel checking of real-time reachability properties using abstractions,\u201d in Tools and Algorithms for the Construction and Analysis of Systems '98, Lisbon, Portugal. LNCS, Vol. 1384, Springer-Verlag, 1998.","DOI":"10.1007\/BFb0054180"},{"key":"281738_CR19","unstructured":"E.A. Emerson and E. Clarke, \u201cDesign and synthesis of synchronization skeletons using branching-time temporal logic,\u201d in Workshop on Logic of Programs. LNCS, Vol. 131, 1981."},{"key":"281738_CR20","doi-asserted-by":"crossref","unstructured":"J.Cl. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis, \u201cAtool box for the verification of lotos programs,\u201d in 14th International Conference on Software Engineering, 1992.","DOI":"10.1145\/143062.143124"},{"key":"281738_CR21","doi-asserted-by":"crossref","unstructured":"J.Cl. Fernandez and L. Mounier, \u201c \u2018On the fly\u2019 verification of behavioural equivalences and preorders,\u201d in Workshop on Computer-Aided Verification, Aalborg University, Denmark. LNCS, Vol. 575, 1991, Springer Verlag.","DOI":"10.1007\/3-540-55179-4_18"},{"key":"281738_CR22","unstructured":"Z. Har'El and R. Kurshan, \u201cAutomatic verification of coordinating systems,\u201d in CAV. LNCS, Vol. 407, 1989."},{"issue":"2","key":"281738_CR23","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, \u201cSymbolic model checking for real-time systems,\u201d Information and Computation, Vol. 111, No. 2, pp. 193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"281738_CR24","unstructured":"G. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991."},{"key":"281738_CR25","first-page":"440","volume":"1427","author":"T.A. Henzinger","year":"1998","unstructured":"T.A. Henzinger, S. Qadeer, and S.K. Rajamani, \u201cYou assume, we guarantee: Methodology and case studies,\u201d in CAV 98: Computer-aided Verification, A.J. Hu and M.Y. Vardi (Eds.), Lecture Notes in Computer Science, Vol. 1427, Springer-Verlag, 1998, pp. 440\u2013451.","journal-title":"CAV 98: Computer-aided Verification"},{"key":"281738_CR26","unstructured":"IEEE. ANSI\/IEEE 802.3, ISO\/DIS 8802\/3. IEEE Computer Society Press, 1985."},{"key":"281738_CR27","unstructured":"H. Lewis, \u201cA logic of concrete time intervals,\u201d in 5th IEEE Symp. LICS, 1990."},{"key":"281738_CR28","doi-asserted-by":"crossref","unstructured":"K. Larsen, F. Larsson, P. Pettersson, and W. Yi, \u201cEfficient verification of real-time systems: Compact data structure and state-space reduction,\u201d in Proceedings of the 18th IEEE Real-Time Systems Symposium, San Francisco, CA, Dec. 1997, pp. 14\u201324.","DOI":"10.1109\/REAL.1997.641265"},{"key":"281738_CR29","doi-asserted-by":"crossref","unstructured":"K. Larsen, P. Petterson, and W. Yi, \u201cUPPAAL in a nutshell,\u201d Software Tools for Technology Transfer, Vol. 1, No. 1\/2, 1997.","DOI":"10.1007\/s100090050010"},{"key":"281738_CR30","doi-asserted-by":"crossref","unstructured":"D. Lee and M. Yannakakis, \u201cOn line minimization of transition systems,\u201d in ACM Symp. on Theory of Computing, 1992.","DOI":"10.1145\/129712.129738"},{"key":"281738_CR31","doi-asserted-by":"crossref","unstructured":"K. Larsen and W. Yi, \u201cTimed abstracted bisimulation: Implicit specification and decidability,\u201d in Proc. MFPS'93, 1993.","DOI":"10.1007\/3-540-58027-1_8"},{"key":"281738_CR32","doi-asserted-by":"crossref","unstructured":"R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, Vol. 92 Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"281738_CR33","unstructured":"L. Mounier, \u201cM\u00b4ethodes de V\u00b4erification de Sp\u00b4ecifications Comportementales: \u00b4etude et mise en oeuvre,\u201d Ph.D. Thesis, Universit\u00b4e Joseph Fourrier de Grenoble, 1993. In French."},{"key":"281738_CR34","series-title":"Technical Report","volume-title":"Back and forth bisimulations","author":"R. De Nicola","year":"1990","unstructured":"R. De Nicola, U. Montanari, and F.W. Vaandrager, \u201cBack and forth bisimulations,\u201d Technical Report, CWI, Netherlands, May 1990."},{"key":"281738_CR35","unstructured":"X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron, \u201cATP: An algebra for timed processes,\u201d in IFIP TC 2, 1990."},{"key":"281738_CR36","volume-title":"Proc. 8th Conference Computer-Aided Verification, CAV'96","author":"A. Pnueli","year":"1996","unstructured":"A. Pnueli and E. Shahar, \u201cA platform for combining deductive and algorithmic verification,\u201d in Proc. 8th Conference Computer-Aided Verification, CAV'96, Rutgers, NJ. LNCS, 1996, Vol. 1102."},{"key":"281738_CR37","doi-asserted-by":"crossref","unstructured":"R. Paige and R. Tarjan, \u201cThree partition refinement algorithms,\u201d SIAM Journal on Computing, Vol. 16, No. 6, 1987.","DOI":"10.1137\/0216062"},{"key":"281738_CR38","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"G.M. Reed","year":"1988","unstructured":"G.M. Reed and A.W. Roscoe, \u201cAtimed model for communicating sequential processes,\u201d Theoretical Computer Science, Vol. 58, pp. 249\u2013261, 1988.","journal-title":"Theoretical Computer Science"},{"key":"281738_CR39","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"R. Spelberg","year":"1998","unstructured":"R. Spelberg, H. Toetenel, and M. Ammerlaan, \u201cPartition refinement in real-time model checking,\u201d in Formal Techniques in Real-Time and Fault-Tolerant Systems, Lyngby, Denmark. LNCS, Vol. 1486, Springer-Verlag, 1998."},{"key":"281738_CR40","doi-asserted-by":"crossref","unstructured":"J. Sifakis and S. Yovine, \u201cCompositional specification of timed systems,\u201d in 13th Annual Symposium on Theoretical Aspects of Computer Science, STACS'96, Grenoble, France, Feb. 1996. Lecture Notes in Computer Science, Vol. 1046, Spinger-Verlag, pp. 347\u2013359.","DOI":"10.1007\/3-540-60922-9_29"},{"key":"281738_CR41","doi-asserted-by":"crossref","unstructured":"S. Tripakis and K. Altisen, \u201cOn-the-fly controller synthesis for discrete and timed systems,\u201d in World Congress on Formal Methods, FM'99, 1999.","DOI":"10.1007\/3-540-48119-2_15"},{"key":"281738_CR42","volume-title":"Computer Networks","author":"A.S. Tanenbaum","year":"1989","unstructured":"A.S. Tanenbaum, Computer Networks, Prentice Hall, Englewood Cliffs, 2nd edn, 1989.","edition":"2nd edn"},{"issue":"2","key":"281738_CR43","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"R. Tarjan, \u201cDepth first search and linear graph algorithms,\u201d SIAM Journal on Computing, Vol. 1, No. 2, pp. 146\u2013170, 1972.","journal-title":"SIAM Journal on Computing"},{"key":"281738_CR44","unstructured":"S. Tripakis, \u201cThe formal analysis of timed systems in practice,\u201d Ph.D. Thesis, Universit\u00b4e Joseph Fourrier de Grenoble, 1998. Available at www-verimag.imag.fr\/PEOPLE\/Stavros.Tripakis."},{"key":"281738_CR45","first-page":"232","volume-title":"Proc. 8th Conference Computer-Aided Verification, CAV'96","author":"S. Tripakis","year":"1996","unstructured":"S. Tripakis and S. Yovine, \u201cAnalysis of timed systems based on time-abstracting bisimulations,\u201d in Proc. 8th Conference Computer-Aided Verification, CAV'96, Rutgers, NJ. LNCS, Vol. 1102, Springer-Verlag, 1996, pp. 232\u2013243."},{"key":"281738_CR46","doi-asserted-by":"crossref","unstructured":"K. \u010cer\u0101ns, \u201cDecidability of bisimulation equivalence for parallel timer processes,\u201d in Proceedings of the Fourth Workshop on Computer-Aided Verification, Lecture Notes in Computer Science, 1992.","DOI":"10.1007\/3-540-56496-9_24"},{"key":"281738_CR47","unstructured":"W. Yi, \u201cReal-time behavior of asynchronous agents,\u201d in Concur'90. LNCS. Vol. 458, 1990."},{"key":"281738_CR48","doi-asserted-by":"crossref","unstructured":"M. Yannakakis and D. Lee, \u201cAn efficient algorithm for minimizing real-time transition systems,\u201d in Fifth Conference on Computer-Aided Verification. Elounda, Greece, June 1993, LNCS, Vol. 697.","DOI":"10.1007\/3-540-56922-7_18"},{"key":"281738_CR49","unstructured":"S. Yovine, \u201cM\u00e9thodes et outils pour la v\u00e9rification symbolique de syst\u00e9mes temporis\u00e9s,\u201d Ph.D. Thesis, Institut National Polytechnique de Grenoble, 1993. In French."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008734703554.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008734703554\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008734703554.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:15:09Z","timestamp":1754421309000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008734703554"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,1]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,1]]}},"alternative-id":["281738"],"URL":"https:\/\/doi.org\/10.1023\/a:1008734703554","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,1]]}}}