{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:20:28Z","timestamp":1778498428760,"version":"3.51.4"},"publisher-location":"Cham","reference-count":159,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_29","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"1001-1046","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Model Checking Real-Time Systems"],"prefix":"10.1007","author":[{"given":"Patricia","family":"Bouyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uli","family":"Fahrenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Markey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"2","key":"29_CR1","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1016\/j.tcs.2005.11.018","volume":"354","author":"Y. Abdedda\u00efm","year":"2006","unstructured":"Abdedda\u00efm, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272\u2013300 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/3-540-44585-4_46","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"Y. Abdedda\u00efm","year":"2001","unstructured":"Abdedda\u00efm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a0478\u2013492. Springer, Heidelberg (2001)"},{"key":"29_CR3","series-title":"LNCS","first-page":"113","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Y. Abdedda\u00efm","year":"2002","unstructured":"Abdedda\u00efm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Katoen, J.-P., Stevens, P. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02280, pp.\u00a0113\u2013126. Springer, Heidelberg (2002)"},{"key":"29_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"1089","DOI":"10.1007\/11523468_88","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"P.A. Abdulla","year":"2005","unstructured":"Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a03580, pp.\u00a01089\u20131101. Springer, Heidelberg (2005)"},{"key":"29_CR5","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-540-69166-2_13","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"X. Allamigeon","year":"2008","unstructured":"Allamigeon, X., Gaubert, S., Goubault, \u00c9.: Inferring min and max invariants using max-plus polyhedra. In: Alpuente, M., Vidal, G. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a05079, pp.\u00a0189\u2013204. Springer, Heidelberg (2008)"},{"key":"29_CR6","first-page":"154","volume-title":"Symposium on Real-Time Systems (RTSS)","author":"K. Altisen","year":"1999","unstructured":"Altisen, K., G\u00f6\u00dfler, G., Pnueli, A., Sifakis, J., Tripakis, S., Yovine, S.: A framework for scheduler synthesis. In: Symposium on Real-Time Systems (RTSS), pp.\u00a0154\u2013163. IEEE, Piscataway (1999)"},{"key":"29_CR7","unstructured":"Alur, R.: Techniques for automatic verification of real-time systems. PhD thesis, Stanford University (1991)"},{"key":"29_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-540-27836-8_13","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"R. Alur","year":"2004","unstructured":"Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a03142, pp.\u00a0122\u2013133. Springer, Heidelberg (2004)"},{"issue":"1","key":"29_CR9","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.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"29_CR10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-540-48654-1_16","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"R. Alur","year":"1994","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a0836, pp.\u00a0162\u2013177. Springer, Heidelberg (1994)"},{"issue":"2","key":"29_CR11","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1023\/A:1008626013578","volume":"11","author":"R. Alur","year":"1997","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A.: Computing accumulated delays in real time systems. Form. Methods Syst. Des. 11(2), 137\u2013155 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"29_CR12","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems (HSCC)","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems (HSCC). LNCS, vol.\u00a0736, pp.\u00a0209\u2013229. Springer, Heidelberg (1993)"},{"issue":"2","key":"29_CR13","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.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"29_CR14","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, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"29_CR15","series-title":"LNCS","first-page":"1","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Alur","year":"1994","unstructured":"Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. In: Dill, D.L. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0818, pp.\u00a01\u201313. Springer, Heidelberg (1994)"},{"issue":"1\u20132","key":"29_CR16","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, T.A.: Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211(1\u20132), 253\u2013273 (1999)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"29_CR17","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35\u201377 (1993)","journal-title":"Inf. Comput."},{"issue":"1","key":"29_CR18","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181\u2013203 (1994)","journal-title":"J. ACM"},{"key":"29_CR19","first-page":"592","volume-title":"Symposium on the Theory of Computing (STOC)","author":"R. Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) Symposium on the Theory of Computing (STOC), pp.\u00a0592\u2013601. ACM, New York (1993)"},{"key":"29_CR20","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","volume-title":"Int. Workshop on Hybrid Systems: Computation and Control (HSCC)","author":"R. Alur","year":"2001","unstructured":"Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Domenica Di Benedetto, M., Sangiovani-Vincentelli, A.L. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol.\u00a02034, pp.\u00a049\u201362. Springer, Heidelberg (2001)"},{"key":"29_CR21","series-title":"LNCS","first-page":"460","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"T. Amnell","year":"2002","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Times\u2014a tool for modelling and implementation of embedded systems. In: Katoen, J.-P., Stevens, P. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02280, pp.\u00a0460\u2013464. Springer, Heidelberg (2002)"},{"key":"29_CR22","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/349360.351127","volume-title":"Workshop on Formal Methods in Software Practice (FMSP)","author":"M. Archer","year":"2000","unstructured":"Archer, M., Heitmeyer, C.L., Riccobene, E.: Using TAME to prove invariants of automata models: two case studies. In: Per, M., Heimdahl, E. (eds.) Workshop on Formal Methods in Software Practice (FMSP), pp.\u00a025\u201336. ACM, New York (2000)"},{"issue":"4","key":"29_CR23","doi-asserted-by":"crossref","first-page":"445","DOI":"10.3233\/FI-1980-3405","volume":"3","author":"A. Arnold","year":"1980","unstructured":"Arnold, A., Nivat, M.: The metric space of infinite trees. Algebraic and topological properties. Fundam. Inform. 3(4), 445\u2013476 (1980)","journal-title":"Fundam. Inform."},{"key":"29_CR24","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"International Workshop on Hybrid and Real-Time Systems (HART)","author":"E. Asarin","year":"1997","unstructured":"Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data-structures for the verification of timed automata. In: Maler, O. (ed.) International Workshop on Hybrid and Real-Time Systems (HART). LNCS, vol.\u00a01201, pp.\u00a0346\u2013360. Springer, Heidelberg (1997)"},{"key":"29_CR25","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-48983-5_6","volume-title":"Int. Workshop on Hybrid Systems: Computation and Control (HSCC)","author":"E. Asarin","year":"1999","unstructured":"Asarin, E., Maler, O.: As soon as possible: time optimal control for timed automata. In: Vaandrager, F., van Schuppen, J.H. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol.\u00a01569, pp.\u00a019\u201330. Springer, Heidelberg (1999)"},{"key":"29_CR26","series-title":"LNCS","first-page":"1","volume-title":"Hybrid Systems II (HSCC)","author":"E. Asarin","year":"1995","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems II (HSCC). LNCS, vol.\u00a0999, pp.\u00a01\u201320. Springer, Heidelberg (1995)"},{"key":"29_CR27","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/BFb0055642","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"E. Asarin","year":"1998","unstructured":"Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01466, pp.\u00a0470\u2013484. Springer, Heidelberg (1998)"},{"key":"29_CR28","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-3-642-02930-1_4","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"C. Baier","year":"2009","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: Albers, S., Alberto, M., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a05557, pp.\u00a043\u201354. Springer, Heidelberg (2009)"},{"key":"29_CR29","series-title":"LNCS","first-page":"254","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"G. Behrmann","year":"2003","unstructured":"Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02619, pp.\u00a0254\u2013270. Springer, Heidelberg (2003)"},{"key":"29_CR30","series-title":"LNCS","first-page":"312","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pel\u00e1nek, R.: Lower and upper bounds in zone-based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02988, pp.\u00a0312\u2013326. Springer, Heidelberg (2004)"},{"issue":"3","key":"29_CR31","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, K.G., Pel\u00e1nek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8(3), 204\u2013215 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"29_CR32","series-title":"LNCS","first-page":"174","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in Uppaal. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02031, pp.\u00a0174\u2013188. Springer, Heidelberg (2001)"},{"key":"29_CR33","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Int. Workshop on Hybrid Systems: Computation and Control (HSCC)","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Domenica Di Benedetto, M., Sangiovani-Vincentelli, A.L. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol.\u00a02034, pp.\u00a0147\u2013161. Springer, Heidelberg (2001)"},{"key":"29_CR34","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01633, pp.\u00a0341\u2013353. Springer, Heidelberg (1999)"},{"key":"29_CR35","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/978-3-540-45069-6_40","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"G. Behrmann","year":"2003","unstructured":"Behrmann, G., Larsen, K.G., Pel\u00e1nek, R.: To store or not to store. In: Hunt, W.A. Jr, Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02725, pp.\u00a0433\u2013445. Springer, Heidelberg (2003)"},{"key":"29_CR36","series-title":"LNCS","first-page":"465","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"R. Ben Salah","year":"2006","unstructured":"Ben Salah, R., Bozga, M., Maler, O.: On interleaving in timed automata. In: Baier, C., Hermanns, H. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a04137, pp.\u00a0465\u2013476. Springer, Heidelberg (2006)"},{"key":"29_CR37","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/BFb0055643","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"J. Bengtsson","year":"1998","unstructured":"Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01466, pp.\u00a0485\u2013500. Springer, Heidelberg (1998)"},{"key":"29_CR38","series-title":"LNCS","first-page":"491","volume-title":"International Conference on Formal Engineering Methods (ICFEM)","author":"J. Bengtsson","year":"2003","unstructured":"Bengtsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) International Conference on Formal Engineering Methods (ICFEM). LNCS, vol.\u00a02885, pp.\u00a0491\u2013503. Springer, Heidelberg (2003)"},{"key":"29_CR39","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J. Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a02098, pp.\u00a087\u2013124. Springer, Heidelberg (2004)"},{"issue":"2\u20133","key":"29_CR40","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., Diekert, V., Gastin, P., Petit, A.: Characterization of the expressive power of silent transitions in timed automata. Fundam. Inform. 36(2\u20133), 145\u2013182 (1998)","journal-title":"Fundam. Inform."},{"issue":"1\u20132","key":"29_CR41","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0020-0190(00)00075-2","volume":"75","author":"B. B\u00e9rard","year":"2000","unstructured":"B\u00e9rard, B., Dufour, C.: Timed automata and additive clock constraints. Inf. Process. Lett. 75(1\u20132), 1\u20137 (2000)","journal-title":"Inf. Process. Lett."},{"key":"29_CR42","series-title":"LNCS","first-page":"257","volume-title":"Symposium on Theoretical Aspects of Computer Science (STACS)","author":"B. B\u00e9rard","year":"1996","unstructured":"B\u00e9rard, B., Gastin, P., Petit, A.: Timed automata with non-observable actions: expressive power and refinement. In: Puech, C., Reischuk, R. (eds.) Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a01046, pp.\u00a0257\u2013268. Springer, Heidelberg (1996)"},{"key":"29_CR43","first-page":"41","volume-title":"IFIP World Computer Congress (WCC)","author":"B. Berthomieu","year":"1983","unstructured":"Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: Mason, R.E.A. (ed.) IFIP World Computer Congress (WCC), pp.\u00a041\u201346. North-Holland\/IFIP, Amsterdam (1983)"},{"key":"29_CR44","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-540-45069-6_13","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Beyer","year":"2003","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: a tool for BDD-based verification of real-time systems. In: Hunt, W.A. Jr, Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02725, pp.\u00a0122\u2013125. Springer, Heidelberg (2003)"},{"key":"29_CR45","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1145\/1434790.1434807","volume-title":"International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES)","author":"T. B\u00f8gholm","year":"2008","unstructured":"B\u00f8gholm, T., Kragh-Hansen, H., Olsen, P., Thomsen, B., Larsen, K.G.: Model-based schedulability analysis of safety critical hard real-time Java programs. In: Bollella, G., Locke, C.D. (eds.) International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES), vol.\u00a0343, pp.\u00a0106\u2013114. ACM, New York (2008)"},{"key":"29_CR46","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-49213-5_5","volume-title":"International Symposium on Compositionality: The Significant Difference (COMPOS)","author":"S. Bornot","year":"1998","unstructured":"Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) International Symposium on Compositionality: The Significant Difference (COMPOS). LNCS, vol.\u00a01536, pp.\u00a0103\u2013129. Springer, Heidelberg (1998)"},{"key":"29_CR47","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/REAL.1997.641266","volume-title":"Symposium on Real-Time Systems (RTSS)","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model checking for real-time systems. In: Symposium on Real-Time Systems (RTSS), pp.\u00a025\u201335. IEEE, Piscataway (1997)"},{"key":"29_CR48","series-title":"LNCS","first-page":"620","volume-title":"Symposium on Theoretical Aspects of Computer Science (STACS)","author":"P. Bouyer","year":"2003","unstructured":"Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a02607, pp.\u00a0620\u2013631. Springer, Heidelberg (2003)"},{"issue":"5","key":"29_CR49","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1016\/j.ipl.2006.01.012","volume":"98","author":"P. Bouyer","year":"2006","unstructured":"Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Inf. Process. Lett. 98(5), 188\u2013194 (2006)","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"29_CR50","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/s10703-007-0043-4","volume":"32","author":"P. Bouyer","year":"2008","unstructured":"Bouyer, P., Brinksma, E., Larsen, K.G.: Staying alive as cheaply as possible. Form. Methods Syst. Des. 32(1), 2\u201323 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"29_CR51","series-title":"LNCS","first-page":"148","volume-title":"Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"P. Bouyer","year":"2004","unstructured":"Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal strategies in priced timed game automata. In: Kamal, L., Mahajan, M. (eds.) Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol.\u00a03328, pp.\u00a0148\u2013160. Springer, Heidelberg (2004)"},{"issue":"2","key":"29_CR52","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/j.ic.2009.10.004","volume":"208","author":"P. Bouyer","year":"2010","unstructured":"Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97\u2013116 (2010)","journal-title":"Inf. Comput."},{"issue":"2\u20133","key":"29_CR53","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/j.tcs.2004.04.003","volume":"321","author":"P. Bouyer","year":"2004","unstructured":"Bouyer, P., Dufour, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2\u20133), 291\u2013345 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR54","first-page":"61","volume-title":"Int. Workshop on Hybrid Systems: Computation and Control (HSCC)","author":"P. Bouyer","year":"2010","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Timed automata with observers under energy constraints. In: Johansson, K.H., Yi, W. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC), pp.\u00a061\u201370. ACM, New York (2010)"},{"key":"29_CR55","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-540-85778-5_4","volume-title":"International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS)","author":"P. Bouyer","year":"2008","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol.\u00a05215, pp.\u00a033\u201347. Springer, Heidelberg (2008)"},{"issue":"1\u20132","key":"29_CR56","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-2009-0063","volume":"92","author":"P. Bouyer","year":"2009","unstructured":"Bouyer, P., Haddad, S., Reynier, P.-A.: Undecidability results for timed automata with silent transitions. Fundam. Inform. 92(1\u20132), 1\u201325 (2009)","journal-title":"Fundam. Inform."},{"issue":"2","key":"29_CR57","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-4(2:9)2008","volume":"4","author":"P. Bouyer","year":"2008","unstructured":"Bouyer, P., Larsen, K.G., Markey, N.: Model checking one-clock priced timed automata. Log. Methods Comput. Sci. 4(2), 1\u201328 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"29_CR58","first-page":"128","volume-title":"Int. Conf. on Quantitative Evaluation of Systems (QEST)","author":"P. Bouyer","year":"2012","unstructured":"Bouyer, P., Larsen, K.G., Markey, N.: Lower-bound constrained runs in weighted timed automata. In: Int. Conf. on Quantitative Evaluation of Systems (QEST), pp.\u00a0128\u2013137. IEEE, Piscataway (2012)"},{"key":"29_CR59","series-title":"LNCS","first-page":"345","volume-title":"Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"P. Bouyer","year":"2006","unstructured":"Bouyer, P., Larsen, K.G., Markey, N., Rasmussen, J.I.: Almost optimal strategies in one-clock priced timed automata. In: Arun-Kumar, S., Garg, N. (eds.) Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol.\u00a04337, pp.\u00a0345\u2013356. Springer, Heidelberg (2006)"},{"key":"29_CR60","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"47","volume-title":"Workshop on Theory and Practice of Timed Systems (TPTS)","author":"M. Bozga","year":"2002","unstructured":"Bozga, M., Jianmin, H., Maler, O., Yovine, S.: Verification of asynchronous circuits using timed automata. In: Asarin, E., Maler, O., Yovine, S. (eds.) Workshop on Theory and Practice of Timed Systems (TPTS). Electronic Notes in Theoretical Computer Science, vol.\u00a065, pp.\u00a047\u201359. Elsevier, Amsterdam (2002)"},{"issue":"1\u20132","key":"29_CR61","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jlap.2008.05.002","volume":"77","author":"A.W. Brekling","year":"2008","unstructured":"Brekling, A.W., Hansen, M.R., Madsen, J.: Models and formal verification of multiprocessor system-on-chips. J. Log. Algebraic Program. 77(1\u20132), 1\u201319 (2008)","journal-title":"J. Log. Algebraic Program."},{"key":"29_CR62","unstructured":"Brenguier, R.: Nash equilibria in concurrent games\u2014application to timed games. PhD thesis, Lab. Sp\u00e9cification & V\u00e9rification, ENS Cachan, France (2012)"},{"key":"29_CR63","series-title":"LNCS","first-page":"277","volume-title":"Joint Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT)","author":"T. Brihaye","year":"2004","unstructured":"Brihaye, T., Bruy\u00e8re, V., Raskin, J.-F.: Model-checking for weighted timed automata. In: Lakhnech, Y., Yovine, S. (eds.) Joint Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). LNCS, vol.\u00a03253, pp.\u00a0277\u2013292. Springer, Heidelberg (2004)"},{"key":"29_CR64","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/11603009_5","volume-title":"International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS)","author":"T. Brihaye","year":"2005","unstructured":"Brihaye, T., Bruy\u00e8re, V., Raskin, J.-F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol.\u00a03829, pp.\u00a049\u201364. Springer, Heidelberg (2005)"},{"key":"29_CR65","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"825","DOI":"10.1007\/978-3-540-73420-8_71","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"T. Brihaye","year":"2007","unstructured":"Brihaye, T., Henzinger, T.A., Prabhu, V.S., Raskin, J.-F.: Minimum-time reachability in timed games. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a04596, pp.\u00a0825\u2013837. Springer, Heidelberg (2007)"},{"key":"29_CR66","series-title":"LNCS","first-page":"445","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"T. Brihaye","year":"2007","unstructured":"Brihaye, T., Laroussinie, F., Markey, N., Oreiby, G.: Timed concurrent game structures. In: Caires, L., Vasconcelos, V.T. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a04703, pp.\u00a0445\u2013459. Springer, Heidelberg (2007)"},{"key":"29_CR67","first-page":"199","volume":"43","author":"J.A. Brzozowski","year":"1991","unstructured":"Brzozowski, J.A., Seger, C.-J.H.: Advances in asynchronous circuit theory part II: bounded inertial delay models, MOS circuits, design techniques. Bull. Eur. Assoc. Theor. Comput. Sci. 43, 199\u2013263 (1991)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"key":"29_CR68","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-642-04761-9_7","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"J. Byg","year":"2009","unstructured":"Byg, J., J\u00f8rgensen, K.Y., Srba, J.: TAPAAL: editor, simulator and verifier of timed-arc Petri nets. In: Liu, Z., Ravn, A.P. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a05799, pp.\u00a084\u201389. Springer, Heidelberg (2009)"},{"key":"29_CR69","series-title":"LNCS","first-page":"66","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"F. Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a03653, pp.\u00a066\u201380. Springer, Heidelberg (2005)"},{"key":"29_CR70","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/978-3-540-75596-8_15","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"F. Cassez","year":"2007","unstructured":"Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: Namjoshi, K., Yoneda, T., Higashino, T., Okamura, Y. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a04762, pp.\u00a0192\u2013206. Springer, Heidelberg (2007)"},{"key":"29_CR71","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/978-3-642-00602-9_7","volume-title":"Int. Workshop on Hybrid Systems: Computation and Control (HSCC)","author":"F. Cassez","year":"2009","unstructured":"Cassez, F., Jensen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic synthesis of robust and optimal controllers\u2014an industrial case study. In: Majumdar, R., Tabuada, P. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol.\u00a05469, pp.\u00a090\u2013104. Springer, Heidelberg (2009)"},{"key":"29_CR72","series-title":"LNCS","first-page":"138","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"F. Cassez","year":"2000","unstructured":"Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01877, pp.\u00a0138\u2013152. Springer, Heidelberg (2000)"},{"key":"29_CR73","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-56496-9_24","volume-title":"Intl. Workshop on Computer-Aided Verification (CAV)","author":"K. \u010cer\u0101ns","year":"1993","unstructured":"\u010cer\u0101ns, K.: Decidability of bisimulation equivalences for parallel timer processes. In: von Bochmann, G., Probst, D.K. (eds.) Intl. Workshop on Computer-Aided Verification (CAV). LNCS, vol.\u00a0663, pp.\u00a0302\u2013315. Springer, Heidelberg (1993)"},{"key":"29_CR74","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/978-3-540-45212-6_9","volume-title":"Int. Conf. on Embedded Software (EMSOFT)","author":"A. Chakrabarti","year":"2003","unstructured":"Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) Int. Conf. on Embedded Software (EMSOFT). LNCS, vol.\u00a02855, pp.\u00a0117\u2013133. Springer, Heidelberg (2003)"},{"issue":"2","key":"29_CR75","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"29_CR76","series-title":"LNCS","first-page":"263","volume-title":"Joint Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT)","author":"S. Cotton","year":"2004","unstructured":"Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some progress in satisfiability checking for difference logic. In: Lakhnech, Y., Yovine, S. (eds.) Joint Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). LNCS, vol.\u00a03253, pp.\u00a0263\u2013276. Springer, Heidelberg (2004)"},{"key":"29_CR77","series-title":"LNCS","first-page":"170","volume-title":"International Conference on Theory and Applications of Satisfiability Testing (SAT)","author":"S. Cotton","year":"2006","unstructured":"Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) International Conference on Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a04121, pp.\u00a0170\u2013183. Springer, Heidelberg (2006)"},{"key":"29_CR78","series-title":"LNCS","first-page":"293","volume-title":"International Symposium on Leveraging Applications of Formal Methods (ISoLA)","author":"A. David","year":"2012","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M.: Schedulability of Herschel-Planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) International Symposium on Leveraging Applications of Formal Methods (ISoLA). LNCS, vol.\u00a07610, pp.\u00a0293\u2013307. Springer, Heidelberg (2012)"},{"key":"29_CR79","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06806, pp.\u00a0349\u2013355. Springer, Heidelberg (2011)"},{"key":"29_CR80","series-title":"Computational Analysis, Synthesis, and Design of Dynamic Systems","volume-title":"Model-Based Design for Embedded Systems","author":"A. David","year":"2009","unstructured":"David, A., Larsen, K.G., Rasmussen, J.I., Skou, A.: Model-based design for embedded systems. In: Nicolescu, G., Mosterman, P.J. (eds.) Model-Based Design for Embedded Systems. Computational Analysis, Synthesis, and Design of Dynamic Systems. CRC Press, Boca Raton (2009)"},{"key":"29_CR81","series-title":"LNCS","first-page":"313","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"C. Daws","year":"1998","unstructured":"Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01384, pp.\u00a0313\u2013329. Springer, Heidelberg (1998)"},{"key":"29_CR82","series-title":"LNCS","first-page":"142","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R., Lugiez, D. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a02761, pp.\u00a0142\u2013156. Springer, Heidelberg (2003)"},{"issue":"1\u20133","key":"29_CR83","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s10703-008-0056-7","volume":"33","author":"M. De Wulf","year":"2008","unstructured":"De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Form. Methods Syst. Des. 33(1\u20133), 45\u201384 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"29_CR84","series-title":"LNCS","first-page":"278","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"P. Dembinski","year":"2003","unstructured":"Dembinski, P., Janowska, A., Janowski, P., Penczek, W., P\u00f3lrola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: Verics: a tool for verifying timed automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02619, pp.\u00a0278\u2013283. Springer, Heidelberg (2003)"},{"issue":"1","key":"29_CR85","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/S0304-3975(00)00089-X","volume":"253","author":"H. Dierks","year":"2001","unstructured":"Dierks, H.: PLC-automata: a new class of implementable real-time automata. Theor. Comput. Sci. 253(1), 61\u201393 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR86","volume-title":"ICAPS Workshop on Verification and Validation of Model-Based Planning and Schedulin Systems (VV&PS)","author":"H. Dierks","year":"2005","unstructured":"Dierks, H.: Finding optimal plans for domains with continuous effects with UPPAAL Cora. In: ICAPS Workshop on Verification and Validation of Model-Based Planning and Schedulin Systems (VV&PS) (2005)"},{"key":"29_CR87","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"International Workshop on Automatic Verification Methods for Finite State Systems (AVMFSS)","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) International Workshop on Automatic Verification Methods for Finite State Systems (AVMFSS). LNCS, vol.\u00a0407, pp.\u00a0197\u2013212. Springer, Heidelberg (1990)"},{"key":"29_CR88","first-page":"360","volume-title":"Symposium on Real-Time Systems (RTSS)","author":"R. Ehlers","year":"2010","unstructured":"Ehlers, R., Fass, D., Gerke, M., Peter, H.-J.: Fully symbolic timed model checking using constraint matrix diagrams. In: Symposium on Real-Time Systems (RTSS), pp.\u00a0360\u2013371. IEEE, Piscataway (2010)"},{"key":"29_CR89","first-page":"167","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"M. Faella","year":"2002","unstructured":"Faella, M., La Torre, S., Murano, A.: Dense real-time games. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0167\u2013176. IEEE, Piscataway (2002)"},{"issue":"2","key":"29_CR90","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/j.tcs.2005.11.019","volume":"354","author":"E. Fersman","year":"2006","unstructured":"Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci. 354(2), 301\u2013317 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR91","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/11513988_41","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"G. Gardey","year":"2005","unstructured":"Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: a tool for analyzing time Petri nets. In: Etessami, K., Rajamani, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03576, pp.\u00a0418\u2013423. Springer, Heidelberg (2005)"},{"key":"29_CR92","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/BFb0014736","volume-title":"International Workshop on Hybrid and Real-Time Systems (HART)","author":"V. Gupta","year":"1997","unstructured":"Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) International Workshop on Hybrid and Real-Time Systems (HART). LNCS, vol.\u00a01201, pp.\u00a0331\u2013345. Springer, Heidelberg (1997)"},{"key":"29_CR93","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/978-3-540-75221-9_13","volume-title":"Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\u00f8rner and Zhou Chaochen on the Occasion of Their 70th Birthdays","author":"M.R. Hansen","year":"2007","unstructured":"Hansen, M.R., Madsen, J., Brekling, A.W.: Semantics and verification of a language for modelling hardware architectures. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\u00f8rner and Zhou Chaochen on the Occasion of Their 70th Birthdays. LNCS, vol.\u00a04700, pp.\u00a0300\u2013319. Springer, Heidelberg (2007)"},{"key":"29_CR94","series-title":"LNCS","first-page":"531","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"T.D. Hansen","year":"2013","unstructured":"Hansen, T.D., Ibsen-Jensen, R., Miltersen, P.B.: A faster algorithm for solving one-clock priced timed games. In: D\u2019Argenio, P.R., Melgratt, H.C. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a08052, pp.\u00a0531\u2013545. Springer, Heidelberg (2013)"},{"key":"29_CR95","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/REAL.1997.641264","volume-title":"Symposium on Real-Time Systems (RTSS)","author":"K. Havelund","year":"1997","unstructured":"Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modelling and analysis of an audio\/video protocol: an industrial case study using Uppaal. In: Symposium on Real-Time Systems (RTSS), pp.\u00a02\u201313. IEEE, Piscataway (1997)"},{"key":"29_CR96","series-title":"Lecture Notes in Computer Science","volume-title":"Int. Workshop on Formal Modelling and Analysis of Timed Systems (FORMATS)","author":"M. Hendriks","year":"2003","unstructured":"Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.: Adding symmetry reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) Int. Workshop on Formal Modelling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol.\u00a02791. Springer, Heidelberg (2003)"},{"issue":"6","key":"29_CR97","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1007\/s10009-006-0025-7","volume":"8","author":"M. Hendriks","year":"2006","unstructured":"Hendriks, M., van den Nieuwelaar, B., Vaandrager, F.: Model checker aided design of a controller for a wafer scanner. Int. J. Softw. Tools Technol. Transf. 8(6), 633\u2013647 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"29_CR98","first-page":"278","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0278\u2013292. IEEE, Piscataway (1996)"},{"key":"29_CR99","series-title":"LNCS","first-page":"41","volume-title":"Intl. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: A user guide to HyTech. In: Brinksma, E., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) Intl. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01019, pp.\u00a041\u201371. Springer, Heidelberg (1995)"},{"issue":"1","key":"29_CR100","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What is decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"29_CR101","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/3-540-60084-1_93","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Kopke, P.W., Wong-Toi, H.: The expressive power of clocks. In: F\u00fcl\u00f6p, Z., Gecseg, F. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0944, pp.\u00a0417\u2013428. Springer, Heidelberg (1995)"},{"key":"29_CR102","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0623, pp.\u00a0545\u2013558. Springer, Heidelberg (1992)"},{"issue":"2","key":"29_CR103","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real time systems. Inf. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"29_CR104","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1007\/BFb0055086","volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a01443, pp.\u00a0580\u2013591. Springer, Heidelberg (1998)"},{"issue":"6","key":"29_CR105","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1016\/S0020-0190(97)00217-2","volume":"65","author":"P. Herrmann","year":"1998","unstructured":"Herrmann, P.: Timed automata and recognizability. Inf. Process. Lett. 65(6), 313\u2013318 (1998)","journal-title":"Inf. Process. Lett."},{"key":"29_CR106","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52\u201353","author":"T. Hune","year":"2002","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. J. Log. Algebraic Program. 52\u201353, 183\u2013220 (2002)","journal-title":"J. Log. Algebraic Program."},{"key":"29_CR107","series-title":"LNCS","first-page":"163","volume-title":"Symposium on Logical Foundations of Computer Science","author":"H. H\u00fcttel","year":"1989","unstructured":"H\u00fcttel, H., Larsen, K.G.: The use of static constructs in a modal process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Symposium on Logical Foundations of Computer Science. LNCS, vol.\u00a0363, pp.\u00a0163\u2013180. Springer, Heidelberg (1989)"},{"key":"29_CR108","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1007\/978-3-540-85778-5_13","volume-title":"International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS)","author":"G. Igna","year":"2008","unstructured":"Igna, G., Kannan, V., Yang, Y., Basten, T., Geilen, M.C.W., Vaandrager, F., Voorhoeve, M., de Smet, S., Somers, L.J.: Formal modeling and scheduling of datapaths of digital document printers. In: Cassez, F., Jard, C. (eds.) International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol.\u00a05215, pp.\u00a0170\u2013187. Springer, Heidelberg (2008)"},{"issue":"5","key":"29_CR109","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1016\/j.jlap.2009.02.009","volume":"78","author":"M.M. Jaghoori","year":"2009","unstructured":"Jaghoori, M.M., de Boer, F.S., Chothia, T., Sirjani, M.: Schedulability of asynchronous real-time concurrent objects. J. Log. Algebraic Program. 78(5), 402\u2013416 (2009)","journal-title":"J. Log. Algebraic Program."},{"key":"29_CR110","series-title":"LNCS","first-page":"227","volume-title":"International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS)","author":"J.J. Jensen","year":"2007","unstructured":"Jensen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided controller synthesis for climate controller using UPPAAL Tiga. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol.\u00a04763, pp.\u00a0227\u2013240. Springer, Heidelberg (2007)"},{"key":"29_CR111","series-title":"Electronic Proceedings in Theoretical Computer Science","first-page":"141","volume-title":"Conference on Systems Software Verification (SSV)","author":"K.Y. J\u00f8rgensen","year":"2012","unstructured":"J\u00f8rgensen, K.Y., Larsen, K.G., Srba, J.: Time-darts: a data structure for verification of closed timed automata. In: Conference on Systems Software Verification (SSV). Electronic Proceedings in Theoretical Computer Science, vol.\u00a0102, pp.\u00a0141\u2013155 (2012)"},{"key":"29_CR112","series-title":"LNCS","first-page":"116","volume-title":"International Conference on Formal Engineering Methods (ICFEM)","author":"J. Julliand","year":"2007","unstructured":"Julliand, J., Mountassir, H., Oudot, \u00c9.: VeSTA: a tool to verify the correct integration of a component in a composite timed system. In: Butler, M.J., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) International Conference on Formal Engineering Methods (ICFEM). LNCS, vol.\u00a04789, pp.\u00a0116\u2013135. Springer, Heidelberg (2007)"},{"key":"29_CR113","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/978-3-642-28332-1_31","volume-title":"Intl. Conf. on Language and Automata Theory and Applications (LATA)","author":"M. Klimo\u0161","year":"2012","unstructured":"Klimo\u0161, M., Larsen, K.G., \u0160tefa\u0148\u00e1k, F., Thaarup, J.: Nash equilibria in concurrent priced games. In: Dediu, A.H., Mart\u00edn-Vide, C. (eds.) Intl. Conf. on Language and Automata Theory and Applications (LATA). LNCS, vol.\u00a07183, pp.\u00a0363\u2013376. Springer, Heidelberg (2012)"},{"key":"29_CR114","series-title":"LNCS","first-page":"679","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Kupferschmid","year":"2007","unstructured":"Kupferschmid, S., Dr\u00e4ger, K., Hoffmann, J., Finkbeiner, B., Dierks, H., Podelski, A., Behrmann, G.: Uppaal\/DMC\u2014abstraction-based heuristics for directed model checking. In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04424, pp.\u00a0679\u2013682. Springer, Heidelberg (2007)"},{"key":"29_CR115","series-title":"LNCS","first-page":"203","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Kupferschmid","year":"2008","unstructured":"Kupferschmid, S., Hoffmann, J., Larsen, K.G.: Fast directed model checking via Russian doll abstraction. In: Ramakrishnan, C.R., Rehof, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04963, pp.\u00a0203\u2013217. Springer, Heidelberg (2008)"},{"key":"29_CR116","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1007\/978-3-540-70545-1_53","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Kupferschmid","year":"2008","unstructured":"Kupferschmid, S., Wehrle, M., Nebel, B., Podelski, A.: Faster than Uppaal? In: Gupta, A., Malik, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05123, pp.\u00a0552\u2013555. Springer, Heidelberg (2008)"},{"key":"29_CR117","series-title":"LNCS","first-page":"139","volume-title":"Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"S. La Torre","year":"2000","unstructured":"La Torre, S., Napoli, M.: A decidable dense branching-time temporal logic. In: Kapoor, S., Prasad, S. (eds.) Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol.\u00a01974, pp.\u00a0139\u2013150. Springer, Heidelberg (2000)"},{"issue":"2","key":"29_CR118","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s002360100067","volume":"38","author":"S. La Torre","year":"2001","unstructured":"La Torre, S., Napoli, M.: Timed tree automata with an application to temporal logic. Acta Inform. 38(2), 89\u2013116 (2001)","journal-title":"Acta Inform."},{"key":"29_CR119","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K.G. Larsen","year":"2001","unstructured":"Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a0493\u2013505. Springer, Heidelberg (2001)"},{"key":"29_CR120","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/REAL.1997.641265","volume-title":"Symposium on Real-Time Systems (RTSS)","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: Symposium on Real-Time Systems (RTSS), pp.\u00a014\u201324. IEEE, Piscataway (1997)"},{"issue":"3","key":"29_CR121","first-page":"271","volume":"6","author":"K.G. Larsen","year":"1999","unstructured":"Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nord. J. Comput. 6(3), 271\u2013298 (1999)","journal-title":"Nord. J. Comput."},{"issue":"1\u20132","key":"29_CR122","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2\u20133","key":"29_CR123","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/j.tcs.2007.09.021","volume":"390","author":"K.G. Larsen","year":"2008","unstructured":"Larsen, K.G., Rasmussen, J.I.: Optimal conditional reachability for multi-priced timed automata. Theor. Comput. Sci. 390(2\u20133), 197\u2013213 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"29_CR124","doi-asserted-by":"crossref","first-page":"10:1","DOI":"10.1145\/1342991.1342994","volume":"9","author":"S. Lasota","year":"2008","unstructured":"Lasota, S., Walukiewicz, I.: Alternating timed automata. ACM Trans. Comput. Log. 9(2), 10:1\u201310:27 (2008)","journal-title":"ACM Trans. Comput. Log."},{"key":"29_CR125","series-title":"LNCS","first-page":"296","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"D. Lugiez","year":"2004","unstructured":"Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02988, pp.\u00a0296\u2013311. Springer, Heidelberg (2004)"},{"issue":"1","key":"29_CR126","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/j.tcs.2005.07.023","volume":"345","author":"D. Lugiez","year":"2005","unstructured":"Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theor. Comput. Sci. 345(1), 27\u201359 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR127","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1109\/EMRTS.1999.777456","volume-title":"Euromicro Conference on Real-Time Systems (ECRTS)","author":"A. Mader","year":"1999","unstructured":"Mader, A., Wupper, H.: Timed automaton models for simple programmable logic controllers. In: Euromicro Conference on Real-Time Systems (ECRTS), pp.\u00a0106\u2013113. IEEE, Piscataway (1999)"},{"key":"29_CR128","series-title":"LNCS","first-page":"229","volume-title":"Symposium on Theoretical Aspects of Computer Science (STACS)","author":"O. Maler","year":"1995","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: Mayr, E.W., Puech, C. (eds.) Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a0900, pp.\u00a0229\u2013242. Springer, Heidelberg (1995)"},{"key":"29_CR129","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-46430-1_26","volume-title":"Int. Workshop on Hybrid Systems: Computation and Control (HSCC)","author":"J.S. Miller","year":"2000","unstructured":"Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Lynch, N., Krogh, B.H. (eds.) Int. Workshop on Hybrid Systems: Computation and Control (HSCC). LNCS, vol.\u00a01790, pp.\u00a0296\u2013310. Springer, Heidelberg (2000)"},{"key":"29_CR130","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"key":"29_CR131","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-48320-9_30","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"M. Minea","year":"1999","unstructured":"Minea, M.: Partial order reduction for model checking of timed automata. In: Baeten, J.C.M., Mauw, S. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01664, pp.\u00a0431\u2013446. Springer, Heidelberg (1999)"},{"key":"29_CR132","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-48168-0_9","volume-title":"International Workshop on Computer Science Logic (CSL)","author":"J.B. M\u00f8ller","year":"1999","unstructured":"M\u00f8ller, J.B., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference decision diagrams. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) International Workshop on Computer Science Logic (CSL). LNCS, vol.\u00a01862, pp.\u00a0111\u2013125. Springer, Heidelberg (1999)"},{"key":"29_CR133","series-title":"LNCS","first-page":"496","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"J. Ouaknine","year":"2009","unstructured":"Ouaknine, J., Rabinovich, A., Worrell, J.: Time-bounded verification. In: Bravetti, M., Zavattaro, G. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a05710, pp.\u00a0496\u2013510. Springer, Heidelberg (2009)"},{"key":"29_CR134","first-page":"54","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"J. Ouaknine","year":"2004","unstructured":"Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: closing a decidability gap. In: Symp. on Logic in Computer Science (LICS), pp.\u00a054\u201363. IEEE, Piscataway (2004)"},{"key":"29_CR135","first-page":"188","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"J. Ouaknine","year":"2005","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0188\u2013197. IEEE, Piscataway (2005)"},{"key":"29_CR136","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/11690634_15","volume-title":"International Conference on Foundations of Software Science and Computation Structure (FoSSaCS","author":"J. Ouaknine","year":"2006","unstructured":"Ouaknine, J., Worrell, J.: On metric temporal logic and faulty Turing machines. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) International Conference on Foundations of Software Science and Computation Structure (FoSSaCS. LNCS, vol.\u00a03921, pp.\u00a0217\u2013230. Springer, Heidelberg (2006)"},{"issue":"1","key":"29_CR137","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-3(1:8)2007","volume":"3","author":"J. Ouaknine","year":"2007","unstructured":"Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Log. Methods Comput. Sci. 3(1), 1\u201327 (2007)","journal-title":"Log. Methods Comput. Sci."},{"key":"29_CR138","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"GI-Conference on Theoretical Computer Science (TCS)","author":"D.M.R. Park","year":"1981","unstructured":"Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-Conference on Theoretical Computer Science (TCS). LNCS, vol.\u00a0104, pp.\u00a0167\u2013183. Springer, Heidelberg (1981)"},{"key":"29_CR139","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/BFb0055349","volume-title":"Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT)","author":"A. Puri","year":"1998","unstructured":"Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). LNCS, vol.\u00a01486, pp.\u00a0210\u2013227. Springer, Heidelberg (1998)"},{"issue":"3","key":"29_CR140","first-page":"247","volume":"4","author":"J.-F. Raskin","year":"1999","unstructured":"Raskin, J.-F., Schobbens, P.-Y.: The logic of event-clocks: decidability, complexity and expressiveness. J. Autom. Lang. Comb. 4(3), 247\u2013286 (1999)","journal-title":"J. Autom. Lang. Comb."},{"key":"29_CR141","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/3-540-60472-3_21","volume-title":"Hybrid Systems II (HSCC)","author":"O.F. Roux","year":"1995","unstructured":"Roux, O.F., Rusu, V.: Deciding time-bounded properties for ELECTRE reactive programs with stopwatch automata. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems II (HSCC). LNCS, vol.\u00a0999, pp.\u00a0405\u2013416. Springer, Heidelberg (1995)"},{"key":"29_CR142","series-title":"Electronic Proceedings in Theoretical Computer Science","volume-title":"Workshop on Quantitative Aspects of Programming Languages (QAPL)","author":"M. Rutkowski","year":"2011","unstructured":"Rutkowski, M.: Two-player reachability-price games on single-clock timed automata. In: Workshop on Quantitative Aspects of Programming Languages (QAPL). Electronic Proceedings in Theoretical Computer Science, vol.\u00a057 (2011)"},{"key":"29_CR143","unstructured":"Sankur, O.: Robustness in timed automata: analysis, synthesis, implementation. PhD thesis, Lab. Sp\u00e9cification & V\u00e9rification, ENS Cachan, France (2013)"},{"key":"29_CR144","series-title":"Electronic Proceedings in Theoretical Computer Science","first-page":"41","volume-title":"Workshop on Quantitative Formal Methods: Theory and Applications (QFM)","author":"M. Schuts","year":"2009","unstructured":"Schuts, M., Zhu, Y., Heidarian, F., Vaandrager, F.: Modelling clock synchronization in the Chess gMAC WSN protocol. In: Andova, S., McIver, A.K., D\u2019Argenio, P.R., Cuijpers, P.J.L., Markovski, J., Morgan, C.C., N\u00fa\u00f1ez, M. (eds.) Workshop on Quantitative Formal Methods: Theory and Applications (QFM). Electronic Proceedings in Theoretical Computer Science, vol.\u00a013, pp.\u00a041\u201354 (2009)"},{"key":"29_CR145","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BFb0055360","volume-title":"Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT)","author":"J. Tapken","year":"1998","unstructured":"Tapken, J., Dierks, H.: MOBY\/PLC\u2014graphical development of PLC-automata. In: Ravn, A.P., Rischel, H. (eds.) Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). LNCS, vol.\u00a01486, pp.\u00a0311\u2013314. Springer, Heidelberg (1998)"},{"key":"29_CR146","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/3-540-45828-X_10","volume-title":"Int. Conf. on Embedded Software (EMSOFT)","author":"S. Tripakis","year":"2002","unstructured":"Tripakis, S.: Description and schedulability analysis of the software architecture of an automated vehicle control system. In: Sangiovani-Vincentelli, A.L., Sifakis, J. (eds.) Int. Conf. on Embedded Software (EMSOFT). LNCS, vol.\u00a02491, pp.\u00a0123\u2013137. Springer, Heidelberg (2002)"},{"issue":"3","key":"29_CR147","doi-asserted-by":"crossref","first-page":"15:1","DOI":"10.1145\/1507244.1507245","volume":"10","author":"S. Tripakis","year":"2009","unstructured":"Tripakis, S.: Checking timed B\u00fcchi automata emptiness on simulation graphs. ACM Trans. Comput. Log. 10(3), 15:1\u201315:19 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"29_CR148","series-title":"LNCS","first-page":"233","volume-title":"World Congress on Formal Methods (FM)","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S., Altisen, K.: On-the-fly controller synthesis for discrete and dense-time systems. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) World Congress on Formal Methods (FM). LNCS, vol.\u00a01708, pp.\u00a0233\u2013252. Springer, Heidelberg (1999)"},{"issue":"1","key":"29_CR149","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1023\/A:1008734703554","volume":"18","author":"S. Tripakis","year":"2001","unstructured":"Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Form. Methods Syst. Des. 18(1), 25\u201368 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"29_CR150","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"277","volume-title":"International Workshop on Runtime Verification (RV)","author":"S. Tripakis","year":"2001","unstructured":"Tripakis, S., Yovine, S.: Timing analysis and code generation of vehicle control software using Taxys. In: Havelund, K., Ro\u015fu, G. (eds.) International Workshop on Runtime Verification (RV). Electronic Notes in Theoretical Computer Science, vol.\u00a055, pp.\u00a0277\u2013286. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"29_CR151","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.: Checking timed B\u00fcchi automata emptiness efficiently. Form. Methods Syst. Des. 26(3), 267\u2013292 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"29_CR152","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/978-3-540-27815-3_41","volume-title":"International Conference on Algebraic Methodology and Software Technology (AMAST)","author":"F. Wang","year":"2004","unstructured":"Wang, F.: Model-checking distributed real-time systems with states, events, and multiple fairness assumptions. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) International Conference on Algebraic Methodology and Software Technology (AMAST). LNCS, vol.\u00a03116, pp.\u00a0553\u2013567. Springer, Heidelberg (2004)"},{"key":"29_CR153","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.tcs.2012.09.019","volume":"467","author":"F. Wang","year":"2013","unstructured":"Wang, F.: Efficient model-checking of dense-time systems with time-convexity analysis. Theor. Comput. Sci. 467, 89\u2013108 (2013)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"29_CR154","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1109\/TSE.2006.71","volume":"32","author":"F. Wang","year":"2006","unstructured":"Wang, F., Huang, G.-D., Yu, F.: TCTL inevitability analysis of dense-time systems: from theory to engineering. IEEE Trans. Softw. Eng. 32(7), 510\u2013526 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"29_CR155","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/s11241-011-9122-0","volume":"47","author":"F. Wang","year":"2011","unstructured":"Wang, F., Yao, L.-W., Yang, Y.-L.: Efficient verification of distributed real-time systems with broadcasting behaviors. Real-Time Syst. 47(4), 285\u2013318 (2011)","journal-title":"Real-Time Syst."},{"issue":"1","key":"29_CR156","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L. Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanz\u00e1lek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39\u201365 (2008)","journal-title":"Real-Time Syst."},{"key":"29_CR157","series-title":"IFIP Conference Proceedings","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-0-387-34878-0_18","volume-title":"Intl. Conf. on Formal Description Techniques (FORTE)","author":"W. Yi","year":"1995","unstructured":"Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Hogrefe, D., Leue, S. (eds.) Intl. Conf. on Formal Description Techniques (FORTE). IFIP Conference Proceedings, vol.\u00a06, pp.\u00a0243\u2013258. Chapman & Hall, London (1995)"},{"issue":"1\u20132","key":"29_CR158","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 123\u2013133 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"29_CR159","series-title":"LNCS","first-page":"273","volume-title":"Int. Workshop on Formal Modelling and Analysis of Timed Systems (FORMATS)","author":"S. Zennou","year":"2003","unstructured":"Zennou, S., Yguel, M., Niebert, Peter: ELSE: a new symbolic state generator for timed automata. In: Larsen, K.G., Niebert, P. (eds.) Int. Workshop on Formal Modelling and Analysis of Timed Systems (FORMATS). LNCS, vol.\u00a02791, pp.\u00a0273\u2013280. Springer, Heidelberg (2003)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T18:19:18Z","timestamp":1693678758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":159,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_29","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}