{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T00:47:31Z","timestamp":1704242851796},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,12,24]],"date-time":"2011-12-24T00:00:00Z","timestamp":1324684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10703-011-0133-1","type":"journal-article","created":{"date-parts":[[2011,12,23]],"date-time":"2011-12-23T15:30:26Z","timestamp":1324654226000},"page":"122-146","source":"Crossref","is-referenced-by-count":13,"title":["Efficient emptiness check for timed B\u00fcchi automata"],"prefix":"10.1007","volume":"40","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Herbreteau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B.","family":"Srivathsan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,12,24]]},"reference":[{"issue":"2","key":"133_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"133_CR2","series-title":"Lecture notes in computer science","first-page":"1","volume-title":"Formal methods for the design of real-time systems, international school on formal methods for the design of computer, communication and software systems, SFM-RT 2004, Bertinoro, Italy, September 13\u201318, 2004, Revised Lectures","author":"R Alur","year":"2004","unstructured":"Alur R, Madhusudan P (2004) Decision problems for timed automata: A survey. In: Bernardo M, Corradini F (eds) Formal methods for the design of real-time systems, international school on formal methods for the design of computer, communication and software systems, SFM-RT 2004, Bertinoro, Italy, September 13\u201318, 2004, Revised Lectures. Lecture notes in computer science, vol\u00a03185. Springer, Berlin, pp\u00a01\u201324"},{"issue":"3","key":"133_CR3","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/s10009-005-0190-0","volume":"8","author":"G Behrmann","year":"2006","unstructured":"Behrmann G, Bouyer P, Larsen KG, Pelanek R (2006) Lower and upper bounds in zone-based abstractions of timed automata. Int J Softw Tools Technol Transf 8(3):204\u2013215","journal-title":"Int J Softw Tools Technol Transf"},{"key":"133_CR4","first-page":"125","volume-title":"Third international conference on the quantitative evaluation of systems (QEST 2006)","author":"G Behrmann","year":"2006","unstructured":"Behrmann G, David A, Larsen KG, Haakansson J, Pettersson P, Yi W, Hendriks M (2006) Uppaal 4.0. In: Third international conference on the quantitative evaluation of systems (QEST 2006), 11\u201314 September 2006, Riverside, California, USA. IEEE Computer Society, Los Alamitos, pp\u00a0125\u2013126"},{"issue":"14","key":"133_CR5","doi-asserted-by":"crossref","first-page":"2773","DOI":"10.1080\/00207540410001705220","volume":"42","author":"B B\u00e9rard","year":"2004","unstructured":"B\u00e9rard B, Bouyer B, Petit A (2004) Analysing the pgm protocol with UPPAAL. Int J Prod Res 42(14):2773\u20132791","journal-title":"Int J Prod Res"},{"key":"133_CR6","first-page":"41","volume-title":"IFIP Congress","author":"B Berthomieu","year":"1983","unstructured":"Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time petri nets. In: IFIP Congress, pp\u00a041\u201346"},{"key":"133_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"620","DOI":"10.1007\/3-540-36494-3_54","volume-title":"STACS 2003, 20th annual symposium on theoretical aspects of computer science, Proceedings","author":"P Bouyer","year":"2003","unstructured":"Bouyer P (2003) Untameable timed automata! In: Alt H, Habib M (eds) STACS 2003, 20th annual symposium on theoretical aspects of computer science, Proceedings, Berlin, Germany, February 27\u2013March 1, 2003. Lecture notes in computer science, vol\u00a02607. Springer, Berlin, pp\u00a0620\u2013631"},{"issue":"3","key":"133_CR8","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1023\/B:FORM.0000026093.21513.31","volume":"24","author":"P Bouyer","year":"2004","unstructured":"Bouyer P (2004) Forward analysis of updatable timed automata. Form Methods Syst Des 24(3):281\u2013320","journal-title":"Form Methods Syst Des"},{"issue":"4","key":"133_CR9","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1007\/s00165-006-0010-7","volume":"18","author":"H Bowman","year":"2006","unstructured":"Bowman H, G\u00f3mez R (2006) How to stop time stopping. Form Asp Comput 18(4):459\u2013493","journal-title":"Form Asp Comput"},{"key":"133_CR10","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Computer aided verification, 10th international conference, CAV \u201998 Proceedings","author":"M Bozga","year":"1998","unstructured":"Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) Kronos: a model-checking tool for real-time systems. In: Hu AJ, Vardi MY (eds) Computer aided verification, 10th international conference, CAV \u201998 Proceedings, Vancouver, BC, Canada, June 28\u2013July\u00a02, 1998. Lecture notes in computer science, vol\u00a01427. Springer, Berlin, pp\u00a0546\u2013550"},{"key":"133_CR11","first-page":"1708","volume-title":"FM\u201999\u2014formal methods, world congress on formal methods in the development of computing systems, Proceedings","author":"J-M Couvreur","year":"1999","unstructured":"Couvreur J-M (1999) On-the-fly verification of linear temporal logic. In: FM\u201999\u2014formal methods, world congress on formal methods in the development of computing systems, Proceedings, vol\u00a0I. Toulouse, France, September 20\u201324, 1999, p\u00a01708"},{"key":"133_CR12","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/11537328_15","volume-title":"Model checking software, 12th international SPIN workshop, Proceedings","author":"J-M Couvreur","year":"2005","unstructured":"Couvreur J-M, Duret-Lutz A, Poitrenaud D (2005) On-the-fly emptiness checks for generalized B\u00fcchi automata. In: Godefroid P (ed) Model checking software, 12th international SPIN workshop, Proceedings, San Francisco, CA, USA, August 22\u201324, 2005. Lecture notes in computer science, vol\u00a03639. Springer, Berlin, pp\u00a0169\u2013184"},{"key":"133_CR13","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Tools and algorithms for construction and analysis of systems, 4th international conference, TACAS\u00a0\u201998, held as part of the European joint conferences on the theory and practice of software, ETAPS\u201998, Proceedings","author":"C Daws","year":"1998","unstructured":"Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: Steffen B (ed) Tools and algorithms for construction and analysis of systems, 4th international conference, TACAS\u00a0\u201998, held as part of the European joint conferences on the theory and practice of software, ETAPS\u201998, Proceedings, Lisbon, Portugal, March 28\u2013April 4, 1998. Lecture notes in computer science, vol\u00a01384, pp\u00a0313\u2013329"},{"key":"133_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic verification methods for finite state systems, international workshop, Proceedings","author":"DL Dill","year":"1990","unstructured":"Dill DL (1990) Timing assumptions and verification of finite-state concurrent systems. In: Sifakis J (ed) Automatic verification methods for finite state systems, international workshop, Proceedings, Grenoble, France, June 12\u201314, 1989. Lecture notes in computer science, vol\u00a0407. Springer, Berlin, pp\u00a0197\u2013212"},{"key":"133_CR15","unstructured":"Gaiser A, Schwoon S (2009) Comparison of algorithms for checking emptiness on B\u00fcchi automata. In: Hilen\u00fd\u00a0P, Maty\u00e1s\u00a0V, Vojnar\u00a0T (eds) Annual doctoral workshop on mathematical and engineering methods in computer science, MEMICS 2009, November 13\u201315, Prestige Hotel, Znojmo, Czech Republic, OASICS, vol\u00a013. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, Germany, 2009, pp\u00a069\u201377"},{"key":"133_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/978-3-540-75454-1_15","volume-title":"Formal modeling and analysis of timed systems, 5th international conference, FORMATS 2007, Proceedings","author":"R G\u00f3mez","year":"2007","unstructured":"G\u00f3mez R, Bowman H (2007) Efficient detection of Zeno runs in timed automata. In: Raskin J-F, Thiagarajan PS (eds) Formal modeling and analysis of timed systems, 5th international conference, FORMATS 2007, Proceedings, Salzburg, Austria, October 3\u20135, 2007. Lecture notes in computer science, vol\u00a04763. Springer, Berlin, pp\u00a0195\u2013210"},{"key":"133_CR17","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/REAL.1997.641264","volume-title":"Proceedings of the 18th IEEE real-time systems symposium (RTSS\u00a0\u201997)","author":"K Havelund","year":"1997","unstructured":"Havelund K, Skou A, Larsen KG, Lund K (1997) Formal modeling and analysis of an audio\/video protocol: An industrial case study using UPPAAL. In: Proceedings of the 18th IEEE real-time systems symposium (RTSS\u00a0\u201997), December 3\u20135, 1997, San Francisco, CA, USA. IEEE Computer Society, Los Alamitos, pp\u00a02\u201313"},{"key":"133_CR18","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/978-3-642-15643-4_17","volume-title":"Automated technology for verification and analysis: 8th international symposium, ATVA 2010, Proceedings","author":"F Herbreteau","year":"2010","unstructured":"Herbreteau F, Srivathsan B (2010) Efficient on-the-fly emptiness check for timed B\u00fcchi automata. In: Bouajjani A, Chin W-N (eds) Automated technology for verification and analysis: 8th international symposium, ATVA 2010, Proceedings, Singapore, September 21\u201324, 2010. Lecture notes in computer science, vol\u00a06252. Springer, Berlin, pp\u00a0218\u2013232"},{"key":"133_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-23217-6_7","volume-title":"Concurrency theory, 22nd international conference, CONCUR 2011, Proceedings","author":"F Herbreteau","year":"2011","unstructured":"Herbreteau F, Srivathsan B (2011) Coarse abstractions make Zeno behaviors difficult to detect. In: Katoen J-P, K\u00f6nig B (eds) Concurrency theory, 22nd international conference, CONCUR 2011, Proceedings, Aachen, Germany, September 6\u20139, 2011. Lecture notes in computer science, vol\u00a06901. Springer, Berlin, pp\u00a092\u2013107"},{"key":"133_CR20","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/978-3-540-75454-1_17","volume-title":"Formal modeling and analysis of timed systems, 5th international conference, FORMATS 2007, Proceedings","author":"JJ Jessen","year":"2007","unstructured":"Jessen JJ, Rasmussen JI, Larsen KG, David A (2007) Guided controller synthesis for climate controller using UPPAAL TiGA. In: Raskin J-F, Thiagarajan PS (eds) Formal modeling and analysis of timed systems, 5th international conference, FORMATS 2007, Proceedings, Salzburg, Austria, October 3\u20135, 2007. Lecture notes in computer science, vol\u00a04763. Springer, Berlin, pp\u00a0227\u2013240"},{"key":"133_CR21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-642-04368-0_18","volume-title":"Formal modeling and analysis of timed systems, 7th international conference, FORMATS 2009, Proceedings","author":"G Li","year":"2009","unstructured":"Li G (2009) Checking timed B\u00fcchi automata emptiness using LU-abstractions. In: Ouaknine J, Vaandrager F (eds) Formal modeling and analysis of timed systems, 7th international conference, FORMATS 2009, Proceedings, Budapest, Hungary, September 14\u201316, 2009. Lecture notes in computer science, vol\u00a05813. Springer, Berlin, pp\u00a0228\u2013242"},{"key":"133_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-540-31980-1_12","volume-title":"Tools and algorithms for the construction and analysis of systems, 11th international conference, TACAS 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Proceedings","author":"S Schwoon","year":"2005","unstructured":"Schwoon S, Esparza J (2005) A note on on-the-fly verification algorithms. In: Halbwachs N, Zuck LD (eds) Tools and algorithms for the construction and analysis of systems, 11th international conference, TACAS 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Proceedings, Edinburgh, UK, April 4\u20138, 2005. Lecture notes in computer science, vol\u00a03440, pp\u00a0174\u2013190"},{"key":"133_CR23","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal methods for real-time and probabilistic systems, 5th international AMAST workshop, ARTS\u201999, Proceedings","author":"S Tripakis","year":"1999","unstructured":"Tripakis S (1999) Verifying progress in timed systems. In: Katoen J-P (ed) Formal methods for real-time and probabilistic systems, 5th international AMAST workshop, ARTS\u201999, Proceedings, Bamberg, Germany, May 26\u201328, 1999. Lecture notes in computer science, vol\u00a01601. Springer, Berlin, pp\u00a0299\u2013314"},{"key":"133_CR24","doi-asserted-by":"crossref","unstructured":"Tripakis S (2009) Checking timed B\u00fcchi emptiness on simulation graphs. ACM Trans Comput Logic, 10(3)","DOI":"10.1145\/1507244.1507245"},{"issue":"3","key":"133_CR25","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/s10703-005-1632-8","volume":"26","author":"S Tripakis","year":"2005","unstructured":"Tripakis S, Yovine S, Bouajjani A (2005) Checking timed B\u00fcchi automata emptiness efficiently. Form Methods Syst Des 26(3):267\u2013292","journal-title":"Form Methods Syst Des"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0133-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0133-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0133-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,21]],"date-time":"2019-06-21T09:06:34Z","timestamp":1561107994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0133-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,24]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["133"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0133-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12,24]]}}}