{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:27:27Z","timestamp":1761596847429},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2004,4,16]],"date-time":"2004-04-16T00:00:00Z","timestamp":1082073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2004,7]]},"DOI":"10.1007\/s10009-003-0135-4","type":"journal-article","created":{"date-parts":[[2004,4,15]],"date-time":"2004-04-15T12:18:38Z","timestamp":1082031518000},"page":"77-97","source":"Crossref","is-referenced-by-count":39,"title":["Efficient verification of timed automata with BDD-like data structures"],"prefix":"10.1007","volume":"6","author":[{"given":"Farn","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,4,16]]},"reference":[{"key":"135_CR1","doi-asserted-by":"crossref","unstructured":"Asarin E, Bozga M, Kerbrat A, Maler O, Pnueli A, Rasse A (1997) Data-structures for the verification of timed automata. In: Proceedings of HART\u201997 (International Workshop on Hybrid And Real-Time Systems) 1997. Lecture notes in computer science, vol 1201. Springer, Berlin Heidelberg New York","DOI":"10.1007\/BFb0014737"},{"key":"135_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Courcoubetis C, Dill DL (1990) Model checking for real-time systems. IEEE LICS (5th International Symposium on Logics in Computer Science), June 1990, Philadelphia, USA, IEEE Computer Society, pp 414\u2013425","DOI":"10.1109\/LICS.1990.113766"},{"key":"135_CR3","doi-asserted-by":"crossref","unstructured":"Balarin F (1996) Approximate reachability analysis of timed automata. IEEE RTSS (17th IEEE Real-Time Sytems Symposium), December 1996, Washington D.C., USA, IEEE Computer Society, pp 52\u201361","DOI":"10.1109\/REAL.1996.563700"},{"key":"135_CR4","first-page":"1020","volume":"checking","author":"Burch","year":"1990","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1990) Symbolic model checking: 1020 states and beyond. IEEE LICS (5th International Symposium on Logics in Computer Science), June 1990, Philadelphia, USA, IEEE Computer Society, pp 428\u2013439","journal-title":"Symbolic model"},{"key":"135_CR5","doi-asserted-by":"crossref","unstructured":"Bozga M, Daws C, Maler O (1998) Kronos: a model-checking tool for real-time systems. In: Proceedings of the 10th conference on computer-aided verification (CAV\u201998), June\/July 1998. Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York","DOI":"10.1007\/BFb0028779"},{"key":"135_CR6","doi-asserted-by":"crossref","unstructured":"Bengtsson J, Larsen K, Larsson F, Pettersson P, Wang Y (1996) UPPAAL \u2013 a tool suite for automatic verification of real-time systems. In: Proceedings of the hybrid control system symposium, 1996. Lecture notes in computer science. Springer, Berlin Heidelberg New York","DOI":"10.1007\/BFb0020949"},{"key":"135_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann G, Larsen KG, Pearson J, Weise C, Wang Y (1999) Efficient timed reachability analysis using clock difference diagrams. In: Proceedings of the conference on computer-aided verification (CAV\u201999), Trento, Italy, July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-48683-6_30"},{"key":"135_CR8","doi-asserted-by":"crossref","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C-35(8)","DOI":"10.1109\/TC.1986.1676819"},{"key":"135_CR9","unstructured":"Dill DL (1989) Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of the conference on computer-aided verification (CAV\u201989), 1989. Lecture notes in computer science, vol 407. Springer, Berlin Heidelberg New York"},{"key":"135_CR10","doi-asserted-by":"crossref","unstructured":"Daws C, Olivero A, Tripakis S, Yovine S (1996) The tool KRONOS. In: Proceedings of the 3rd conference on hybrid systems, 1996. Lecture notes in computer science, vol 1066. Springer, Berlin Heidelberg New York","DOI":"10.1007\/BFb0020947"},{"key":"135_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Nicollin X, Sifakis J, Yovine S (1992) Symbolic model checking for real-time systems. IEEE LICS (7th International Symposium on Logics in Computer Science), Santa Cruz, USA, IEEE Computer Society, June 1992, pp 394\u2013406","DOI":"10.1109\/LICS.1992.185551"},{"key":"135_CR12","unstructured":"Larsen KG, Larsson F, Pettersson P, Wang Y (1998) Efficient verification of real-time systems: compact data-structure and state-space reduction. IEEE RTSS (19th IEEE Real-Time Systems Symposium), Madrid, Spain, IEEE Computer Society, December 1998"},{"key":"135_CR13","doi-asserted-by":"crossref","unstructured":"Moller J, Lichtenberg J, Andersen HR, Hulgaard H (1999) Difference decision diagrams. In: Proceedings of the annual conference of the European Association for Computer Science Logic (CSL), September 1999, Madrid, Spain","DOI":"10.1007\/3-540-48168-0_9"},{"key":"135_CR14","unstructured":"Moller J, Lichtenberg J, Andersen HR, Hulgaard H (1999) Fully symbolic model-checking of timed systems using difference decision diagrams. In: Proceedings of the workshop on symbolic model-checking (SMC), July 1999, Trento, Italy"},{"key":"135_CR15","first-page":"40","volume":"70","author":"Pettersson","year":"2000","unstructured":"Pettersson P, Larsen KG (2000) UPPAAL2k. Bull Eur Assoc Theor Comput Sci 70:40\u201344","journal-title":"Bull Eur Assoc Theor Comput Sci"},{"key":"135_CR16","doi-asserted-by":"crossref","unstructured":"Wang F (2000a) Efficient data-structure for fully symbolic verification of real-time software systems. In: Proceedings of the conference on tools and algorithms for the construction and analysis of systems (TACAS 2000), March 2000, Berlin. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-46419-0_12"},{"key":"135_CR17","unstructured":"Wang F (2000b) Region encoding diagram for fully symbolic verification of real-time systems. In: Proceedings of the the 24th COMPSAC (24th Computer Software and Applications Conference), October 2000, Taipei, Taiwan, ROC. IEEE Computer Society, IEEE Press, New York, pp 509\u2013515"},{"key":"135_CR18","unstructured":"Wang F (2001a) RED: Model-checker for timed automata with clock-restriction diagram. In: Proceedings of the workshop on real-time tools, August 2001. Technical Report 2001-014, ISSN 1404-3203, Department of Information Technology, Uppsala University, Uppsala, Sweden"},{"key":"135_CR19","doi-asserted-by":"crossref","unstructured":"Wang F (2001b) Symbolic verification of complex real-time systems with clock-restriction diagram. In: Proceedings of FORTE\u20192001 (21st IFIP International Conference on Formal Techniques for Networked and Distributed Systems), August 2001, Cheju Island, Korea. Kluwer, Dordrecht, pp 235\u2013250","DOI":"10.1007\/0-306-47003-9_15"},{"key":"135_CR20","unstructured":"Wang F (2003) Symbolic parametric analysis of linear hybrid systems with BDD-like data-structures. ACM CoRR (Computing Research Repository, http:\/\/www.acm.org\/corr\/), user:cs.DS\/0306113"},{"key":"135_CR21","unstructured":"Wang F, Hsiung P-A (2002) Efficient and user-friendly verification. IEEE Trans Comput"},{"key":"135_CR22","doi-asserted-by":"crossref","unstructured":"Wang F, Mok A, Emerson EA (1993) Symbolic model-checking for distributed real-time systems. In: Proceedings of the FME (1st International Symposium of Formal Methods Europe), April 1993, Odense, Denmark. Lecture notes in computer science, vol 670. Springer, Berlin Heidelberg New York, pp 632\u2013651","DOI":"10.1007\/BFb0024671"},{"key":"135_CR23","doi-asserted-by":"crossref","unstructured":"Wang F, Hwang G-D, Yu F (2003a) TCTL inevitability analysis of dense-time systems. In: Proceedings of the 8th conference on implementation and application of automata (CIAA), July 2003, Santa Barbara, CA. Lecture notes in computer science, vol 2759. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45089-0_17"},{"key":"135_CR24","doi-asserted-by":"crossref","unstructured":"Wang F, Hwang G-D, Yu F (2003b) Numerical coverage estimation for the symbolic simulation of real-time systems. To appear in the proceedings of FORTE\u20192003 (23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems), September\u2013October 2003, Berlin. Lecture notes in computer science, vol 2767. Springer, Berlin Heidelberg New York, pp 160\u2013176","DOI":"10.1007\/978-3-540-39979-7_11"},{"key":"135_CR25","doi-asserted-by":"crossref","unstructured":"Yovine S (1997) Kronos: a verification tool for real-time systems. Int J Softw Tools Technol Transfer 1(1\/2)","DOI":"10.1007\/s100090050009"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0135-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0135-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0135-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,1]],"date-time":"2020-04-01T00:34:29Z","timestamp":1585701269000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0135-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4,16]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["135"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0135-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4,16]]}}}