{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:37Z","timestamp":1760202637973},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,1,11]],"date-time":"2012-01-11T00:00:00Z","timestamp":1326240000000},"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,2]]},"DOI":"10.1007\/s10703-011-0140-2","type":"journal-article","created":{"date-parts":[[2012,1,10]],"date-time":"2012-01-10T12:43:50Z","timestamp":1326199430000},"page":"41-87","source":"Crossref","is-referenced-by-count":17,"title":["Interrupt Timed Automata: verification and expressiveness"],"prefix":"10.1007","volume":"40","author":[{"given":"B\u00e9atrice","family":"B\u00e9rard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serge","family":"Haddad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathieu","family":"Sassolas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,1,11]]},"reference":[{"key":"140_CR1","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/BFb0054177","volume-title":"Proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems (TACAS\u201998)","author":"L Aceto","year":"1998","unstructured":"Aceto L, Burgue\u00f1o A, Larsen KG (1998) Model checking via reachability testing for timed automata. In: Proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems (TACAS\u201998). Lecture notes in computer science, vol\u00a01384. Springer, London, pp\u00a0263\u2013280"},{"key":"140_CR2","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:183\u2013235","journal-title":"Theor Comput Sci"},{"key":"140_CR3","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 DL (1993) Model-checking in dense real-time. Inf Comput 104:2\u201334","journal-title":"Inf Comput"},{"key":"140_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine\u00a0S (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138:3\u201334","journal-title":"Theor Comput Sci"},{"issue":"1","key":"140_CR5","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur R, Feder T, Henzinger TA (1996) The benefits of relaxing punctuality. J ACM 43(1):116\u2013146","journal-title":"J ACM"},{"issue":"1","key":"140_CR6","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(94)00228-B","volume":"138","author":"E Asarin","year":"1995","unstructured":"Asarin E, Maler O, Pnueli A (1995) Reachability analysis of dynamical systems having piecewise-constant derivatives. Theor Comput Sci 138(1):35\u201365","journal-title":"Theor Comput Sci"},{"issue":"1\u20132","key":"140_CR7","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/j.tcs.2007.03.055","volume":"379","author":"E Asarin","year":"2007","unstructured":"Asarin E, Schneider G, Yovine S (2007) Algorithmic analysis of polygonal hybrid systems, part I: Reachability. Theor Comput Sci 379(1\u20132):231\u2013265","journal-title":"Theor Comput Sci"},{"key":"140_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal methods for the design of real-time systems (SFM-RT\u201904)","author":"G Behrmann","year":"2004","unstructured":"Behrmann G, David A, Larsen KG (2004) A tutorial on uppaal. In: Formal methods for the design of real-time systems (SFM-RT\u201904). Lecture notes in computer science, vol\u00a03185. Springer, Berlin, pp\u00a0200\u2013236"},{"key":"140_CR9","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-642-00596-1_15","volume-title":"Proceedings of the 12th international conference on foundations of software science and computation structures (FoSSaCS\u201909)","author":"B B\u00e9rard","year":"2009","unstructured":"B\u00e9rard B, Haddad S (2009) Interrupt timed automata. In: Proceedings of the 12th international conference on foundations of software science and computation structures (FoSSaCS\u201909). Lecture notes in computer science, vol\u00a05504. York, GB. Springer, Berlin (March 2009), pp\u00a0197\u2013211"},{"issue":"2\u20133","key":"140_CR10","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, Petit A, Diekert V, Gastin P (1998) Characterization of the expressive power of silent transitions in timed automata. Fundam Inform 36(2\u20133):145\u2013182","journal-title":"Fundam Inform"},{"key":"140_CR11","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/TIME.2010.11","volume-title":"Proceedings of the 17th international symposium on temporal representation and reasoning (TIME\u201910)","author":"B B\u00e9rard","year":"2010","unstructured":"B\u00e9rard B, Haddad S, Sassolas M (2010) Real time properties for interrupt timed automata. In: Markey N, Wisjen J (eds) Proceedings of the 17th international symposium on temporal representation and reasoning (TIME\u201910). IEEE Computer Society, Washington (September 2010), pp\u00a069\u201376"},{"issue":"3","key":"140_CR12","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"},{"key":"140_CR13","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"432","DOI":"10.1007\/11590156_35","volume-title":"Proceedings of the 25th conference on foundations of software technology and theoretical computer science (FSTTCS\u201905)","author":"P Bouyer","year":"2005","unstructured":"Bouyer P, Chevalier F, Markey N (2005) On the expressiveness of TPTL and MTL. In: Proceedings of the 25th conference on foundations of software technology and theoretical computer science (FSTTCS\u201905). Lecture notes in computer science, vol\u00a03821. Springer, Berlin (December 2005), pp\u00a0432\u2013443"},{"key":"140_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/978-3-540-85778-5_6","volume-title":"Proceedings of the 6th international conference on formal modelling and analysis of timed systems (FORMATS\u201908)","author":"P Bouyer","year":"2008","unstructured":"Bouyer P, Brihaye Th, Jurdzi\u0144ski M, Lazi\u0107 R, Rutkowski M (2008) Average-price and reachability-price games on hybrid automata with strong resets. In: Cassez F, Jard C (eds) Proceedings of the 6th international conference on formal modelling and analysis of timed systems (FORMATS\u201908), Saint-Malo, France. Lecture notes in computer science, vol\u00a05215. Springer, Berlin (September 2008), pp\u00a063\u201377"},{"key":"140_CR15","first-page":"298","volume-title":"FTRTFT","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: FTRTFT, pp\u00a0298\u2013302"},{"issue":"3","key":"140_CR16","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1016\/j.ic.2005.12.001","volume":"204","author":"T Brihaye","year":"2006","unstructured":"Brihaye T, Bruy\u00e8re V, Raskin JF (2006) On model-checking timed automata with stopwatch observers. Inf Comput 204(3):408\u2013433","journal-title":"Inf Comput"},{"key":"140_CR17","series-title":"Lecture notes in computer science","first-page":"416","volume-title":"Proceedings (part\u00a0II) of the 38th international colloquium on automata, languages and programming (ICALP\u201911)","author":"T Brihaye","year":"2010","unstructured":"Brihaye T, Doyen L, Geeraerts G, Ouaknine J, Raskin JF, Worrell J (2010) On reachability for hybrid automata over bounded time. In: Aceto L, Henzinger M, Sgall J (eds) Proceedings (part\u00a0II) of the 38th international colloquium on automata, languages and programming (ICALP\u201911). Lecture notes in computer science, vol\u00a06756. Springer, Berlin (July 2011), pp\u00a0416\u2013427"},{"key":"140_CR18","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/3-540-44618-4_12","volume-title":"Proceedings of the 11th international conference on concurrency theory (CONCUR\u201900)","author":"F Cassez","year":"2000","unstructured":"Cassez F, Larsen KG (2000) The impressive power of stopwatches. In: Palamidessi C (ed) Proceedings of the 11th international conference on concurrency theory (CONCUR\u201900). Lecture notes in computer science, vol\u00a01877. Springer, Berlin, pp\u00a0138\u2013152"},{"key":"140_CR19","series-title":"Lecture notes in computer science","first-page":"241","volume-title":"Proceedings of the 14th international conference on computer aided verification (CAV\u201902)","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV version 2: An opensource tool for symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification (CAV\u201902). Lecture notes in computer science, vol\u00a02404. Springer, Berlin, pp\u00a0241\u2013268"},{"issue":"4","key":"140_CR20","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/BF00709157","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis C, Yannakakis M (1992) Minimum and maximum delay problems in real-time systems. Form Methods Syst Des 1(4):385\u2013415","journal-title":"Form Methods Syst Des"},{"key":"140_CR21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/BFb0055641","volume-title":"Proceedings of the 9th international conference on concurrency theory (CONCUR\u201998)","author":"F Demichelis","year":"1998","unstructured":"Demichelis F, Zielonka W (1998) Controlled timed automata. In: Sangiorgi D, de\u00a0Simone R (eds) Proceedings of the 9th international conference on concurrency theory (CONCUR\u201998). Lecture notes in computer science, vol\u00a01466. Springer, London, pp\u00a0455\u2013469"},{"key":"140_CR22","first-page":"169","volume-title":"Proc 14th annual ACM symp on theory of computing (Stoc\u201982)","author":"EA Emerson","year":"1982","unstructured":"Emerson EA, Halpern JY (1982) Decision procedures and expressiveness in the temporal logic of branching time. In: Proc 14th annual ACM symp on theory of computing (Stoc\u201982). ACM, New York, pp\u00a0169\u2013180"},{"issue":"8","key":"140_CR23","doi-asserted-by":"crossref","first-page":"1149","DOI":"10.1016\/j.ic.2007.01.009","volume":"205","author":"E Fersman","year":"2007","unstructured":"Fersman E, Krcal P, Pettersson P, Yi W (2007) Task automata: Schedulability, decidability and undecidability. Inf Comput 205(8):1149\u20131172","journal-title":"Inf Comput"},{"issue":"2","key":"140_CR24","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger TA, Nicollin X, Sifakis J, Yovine S (1994) Symbolic model checking for real-time systems. Inf Comput 111(2):193\u2013244","journal-title":"Inf Comput"},{"issue":"1","key":"140_CR25","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger TA, Kopke PW, Puri A, Varaiya P (1998) What\u2019s decidable about hybrid automata? J Comput Syst Sci 57(1):94\u2013124","journal-title":"J Comput Syst Sci"},{"issue":"2","key":"140_CR26","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1006\/inco.1998.2774","volume":"150","author":"Y Kesten","year":"1999","unstructured":"Kesten Y, Pnueli A, Sifakis J, Yovine S (1999) Decidable integration graphs. Inf Comput 150(2):209\u2013243","journal-title":"Inf Comput"},{"key":"140_CR27","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2:255\u2013299","journal-title":"Real-Time Syst"},{"key":"140_CR28","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-48983-5_15","volume-title":"Proceedings of hybrid systems: Computation and control","author":"G Lafferriere","year":"1999","unstructured":"Lafferriere G, Pappas GJ, Yovine S (1999) A new class of decidable hybrid systems. In: Proceedings of hybrid systems: Computation and control. Lecture notes in computer science, vol\u00a01569. Springer, Berlin, pp\u00a0137\u2013151"},{"issue":"3","key":"140_CR29","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere G, Pappas GJ, Yovine S (2001) Symbolic reachability computation for families of linear vector fields. J Symb Comput 32(3):231\u2013253","journal-title":"J Symb Comput"},{"key":"140_CR30","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/BFb0032003","volume-title":"Real-time: theory in practice, REX workshop","author":"O Maler","year":"1992","unstructured":"Maler O, Manna Z, Pnueli A (1992) From timed to hybrid systems. In: Rozenberg G, de\u00a0Roever WP, Huizing C, de\u00a0Bakker JW (eds) Real-time: theory in practice, REX workshop. Lecture notes in computer science, vol\u00a0600. Springer, Berlin, pp\u00a0447\u2013484"},{"key":"140_CR31","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/3-540-58179-0_47","volume-title":"Proceedings of the 6th international conference on computer aided verification (CAV\u201994)","author":"J McManis","year":"1994","unstructured":"McManis J, Varaiya P (1994) Suspension automata: A decidable class of hybrid automata. In: Proceedings of the 6th international conference on computer aided verification (CAV\u201994). Springer, London, pp\u00a0105\u2013117"},{"key":"140_CR32","volume-title":"Computation: Finite and infinite machines","author":"ML Minsky","year":"1967","unstructured":"Minsky ML (1967) Computation: Finite and infinite machines. Prentice-Hall, Inc, Upper Saddle River"},{"key":"140_CR33","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1109\/SFCS.1977.32","volume-title":"Proceedings of the 18th annual symposium on foundations of computer science (FoCS\u201977)","author":"A Pnueli","year":"1977","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th annual symposium on foundations of computer science (FoCS\u201977). IEEE Computer Society, Washington, pp\u00a046\u201357"},{"key":"140_CR34","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of the 5th international symposium on programming","author":"JP Queille","year":"1982","unstructured":"Queille JP, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini M, Montanari U (eds) Proceedings of the 5th international symposium on programming. Lecture notes in computer science, vol\u00a0137. Springer, London, pp\u00a0337\u2013351"},{"key":"140_CR35","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BFb0014711","volume-title":"Hybrid and real-time systems","author":"JF Raskin","year":"1997","unstructured":"Raskin JF, Schobbens PY (1997) State clock logic: A decidable real-time logic. In: Maler O (ed) Hybrid and real-time systems. Lecture notes in computer science, vol\u00a01201. Springer, Berlin, pp\u00a033\u201347"},{"key":"140_CR36","volume-title":"Theory and algorithms for linear optimization. An interior point approach","author":"C Roos","year":"1997","unstructured":"Roos C, Terlaky T, Vial JP (1997) Theory and algorithms for linear optimization. An interior point approach. Wiley-Interscience, New York"},{"key":"140_CR37","volume-title":"Operating systems concepts","author":"A Silberschatz","year":"2008","unstructured":"Silberschatz A, Galvin PB, Gagne G (2008) Operating systems concepts, 8th\u00a0edn. Wiley, New York","edition":"8"},{"key":"140_CR38","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla AP, Clarke EMM (1985) The complexity of propositional linear temporal logics. J ACM 32:733\u2013749","journal-title":"J ACM"},{"key":"140_CR39","doi-asserted-by":"crossref","unstructured":"Zaslavsky T (1975) Facing up to arrangements: Face-count formulas for partitions of space by hyperplanes. AMS Mem 1(154)","DOI":"10.1090\/memo\/0154"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0140-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0140-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0140-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,30]],"date-time":"2020-06-30T15:11:24Z","timestamp":1593529884000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0140-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,11]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["140"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0140-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,11]]}}}