{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,11]],"date-time":"2024-08-11T09:07:27Z","timestamp":1723367247889},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,8,6]],"date-time":"2014-08-06T00:00:00Z","timestamp":1407283200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,12]]},"DOI":"10.1007\/s10703-014-0212-1","type":"journal-article","created":{"date-parts":[[2014,8,5]],"date-time":"2014-08-05T16:32:31Z","timestamp":1407256351000},"page":"330-380","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["On regions and zones for event-clock automata"],"prefix":"10.1007","volume":"45","author":[{"given":"Gilles","family":"Geeraerts","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nathalie","family":"Sznajder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,8,6]]},"reference":[{"key":"212_CR1","doi-asserted-by":"crossref","unstructured":"Alur R (1999) Timed automata. In: Proceedings of CAV\u201999, vol 1633. Lecture notes in computer science. Springer, Berlin, pp 8\u201322","DOI":"10.1007\/3-540-48683-6_3"},{"key":"212_CR2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill D (1993) Model-checking in dense real-time. Inf Comput 104:2\u201334","journal-title":"Inf Comput"},{"issue":"2","key":"212_CR3","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 D (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013236","journal-title":"Theor Comput Sci"},{"issue":"1\u20132","key":"212_CR4","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0304-3975(97)00173-4","volume":"211","author":"R Alur","year":"1999","unstructured":"Alur R, Fix L, Henzinger TA (1999) Event-clock automata: a determinizable class of timed automata. Theor Comput Sci 211(1\u20132):253\u2013273","journal-title":"Theor Comput Sci"},{"key":"212_CR5","unstructured":"Behrmann G, David A, Larsen KG, H\u00e5kansson J, Pettersson P, Yi W, Hendriks M (2006) Uppaal 4.0. In: Proceedings of QEST\u201906. IEEE Computer Society, New York, pp 125\u2013126"},{"key":"212_CR6","volume-title":"Dynamic programming","author":"R Bellman","year":"1957","unstructured":"Bellman R (1957) Dynamic programming. Princeton university press, Princeton"},{"key":"212_CR7","doi-asserted-by":"crossref","unstructured":"Bengtsson J, Griffioen WOD, Kristoffersen KJ, Larsen KG, Larsson F, Pettersson P, Yi W (2002) Automated verification of an audio-control protocol using Uppaal. J Log Algebr Program 52\u201353:163\u2013181","DOI":"10.1016\/S1567-8326(02)00036-X"},{"key":"212_CR8","unstructured":"Bouyer P (2002) Mod\u00e8les et algorithmes pour la v\u00e9rification des syst\u00e8mes temporis\u00e9s. Th\u00e8se de doctorat, Laboratoire Sp\u00e9cification et V\u00e9rification. ENS Cachan, France"},{"key":"212_CR9","unstructured":"Bouyer P (2002) Timed automata may cause some troubles. In Research Report LSV-02-9, LSV, ENS DE CACHAN. http:\/\/www.lsv.enscachan.fr\/Publis\/RAPPORTS_LSV\/PS\/rrlsv-2002-9.rr.ps"},{"issue":"3","key":"212_CR10","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. Formal Methods Syst Des 24(3):281\u2013320","journal-title":"Formal Methods Syst Des"},{"key":"212_CR11","doi-asserted-by":"crossref","unstructured":"Bouyer P, Laroussinie F, Reynier P-A (2005) Diagonal constraints in timed automata: Forward analysis of timed systems. In: Pettersson P, Yi W (eds) Formal modeling and analysis of timed systems, vol 3829. Lecture notes in computer science. Springer, Berlin, pp 112\u2013126","DOI":"10.1007\/11603009_10"},{"key":"212_CR12","doi-asserted-by":"crossref","unstructured":"Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) Kronos: A model-checking tool for real-time systems. In: Proceedings of CAV\u201998, vol 1427. Lecture notes in computer science. Springer, Berlin, pp 546\u2013550","DOI":"10.1007\/BFb0028779"},{"key":"212_CR13","unstructured":"Cerans K (1993) Decidability of bisimulation equivalences for parallel timer processes. In: Proceedings of the fourth international workshop on computer aided verification, CAV \u201992, London. Springer, Berlin, pp 302\u2013315"},{"key":"212_CR14","doi-asserted-by":"crossref","unstructured":"Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In Steffen B (ed) Proceedings of TACAS\u201998, vol 1384. Lecture notes in computer science. Springer, Berlin, pp 313\u2013329","DOI":"10.1007\/BFb0054180"},{"key":"212_CR15","doi-asserted-by":"crossref","unstructured":"Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: TACAS. Springer, Berlin, pp 313\u2013329","DOI":"10.1007\/BFb0054180"},{"key":"212_CR16","doi-asserted-by":"crossref","unstructured":"Di Giampaolo B, Geeraerts G, Raskin J, Sznajder N (2010) Safraless procedures for timed specifications. In: Proceedings of FORMATS\u201910, vol 6246. Lecture notes in computer science. Springer, Berlin, pp 2\u201322","DOI":"10.1007\/978-3-642-15297-9_2"},{"key":"212_CR17","unstructured":"Diekert V, Gastin P, Petit A (1997) Removing epsilon-transitions in timed automata. In: STACS 97, 14th Annual Symposium on theoretical aspects of computer science, vol 1200. Lecture notes in computer science. Springer, Berlin, pp 583\u2013594"},{"key":"212_CR18","doi-asserted-by":"crossref","unstructured":"Dill DL (1989) Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of automatic verification methods for finite state systems, vol 407. Lecture notes in computer science. Springer, Berlin, pp 197\u2013212","DOI":"10.1007\/3-540-52148-8_17"},{"key":"212_CR19","doi-asserted-by":"crossref","unstructured":"Dima C (1999) Kleene theorems for event-clock automata. In: Proceedings of FCT\u201999, volume 1684 of Lecture Notes in computer science. Springer, Berlin, pp 215\u2013225","DOI":"10.1007\/3-540-48321-7_17"},{"key":"212_CR20","doi-asserted-by":"crossref","unstructured":"D\u2019Souza D, Tabareau N (2004) On timed automata with input-determined guards. In Proccedings of FORMATS\/FTRTFT\u201904, vol 3253. Lecture notes in computer science. Springer, Berlin, pp 68\u201383","DOI":"10.1007\/978-3-540-30206-3_7"},{"key":"212_CR21","doi-asserted-by":"crossref","unstructured":"Geeraerts G, Raskin J-F, Sznajder N (2011) Event-clock automata : from theory to practice. In: Fahrenberg U, Tripakis S (eds) Proceedings of the 9th international conference on formal modelling and analysis of timed systems (FORMATS\u201911), vol 6919. Lecture notes in computer science. Springer, Berlin, pp 209\u2013224","DOI":"10.1007\/978-3-642-24310-3_15"},{"key":"212_CR22","doi-asserted-by":"crossref","unstructured":"Lindahl M, Pettersson P, Yi W (1998) Formal design and analysis of a gear-box controller. In: Proceedings of the 4th workshop on tools and algorithms for the construction and analysis of systems. vol 1384 .Lecture notes in computer science. Springer, Berlin, pp 281\u2013297","DOI":"10.1007\/BFb0054178"},{"key":"212_CR23","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2006) The octagon abstract domain. Higher-Order Symbol Comput 19(1):31\u2013100, 2006. http:\/\/www.di.ens.fr\/~mine\/publi\/article-mine-HOSC06.pdf","DOI":"10.1007\/s10990-006-8609-1"},{"key":"212_CR24","doi-asserted-by":"crossref","unstructured":"Pettersson, P, Yi W editors. Formal Modeling and Analysis of Timed Systems. In: Proceedings of the third international conference, FORMATS 2005, Uppsala, September 26\u201328, 2005, vol 3829. Lecture notes in computer science. Springer, Berlin","DOI":"10.1007\/11603009"},{"issue":"3","key":"212_CR25","first-page":"247","volume":"34","author":"J-F Raskin","year":"1998","unstructured":"Raskin J-F, Schobbens P-Y (1998) The logic of event clocks: decidability, complexity and expressiveness. Automatica 34(3):247\u2013282","journal-title":"Automatica"},{"key":"212_CR26","unstructured":"Sorea M (2001) Tempo: a model-checker for event-recording automata. In: Proceedings of RT-TOOLS\u201901, Aalborg"},{"key":"212_CR27","unstructured":"Tang N, Ogawa M (2009) Event-clock visibly pushdown automata. In: Proceedings of SOFSEM\u201909, vol 5404. Lecture notes in computer science. Springer, Berlin, pp 558\u2013569"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0212-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0212-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0212-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,22]],"date-time":"2020-08-22T22:55:53Z","timestamp":1598136953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0212-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,6]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["212"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0212-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,6]]}}}