{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:04Z","timestamp":1776333544741,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540584681","type":"print"},{"value":"9783540489849","type":"electronic"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58468-4_191","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:16:20Z","timestamp":1330254980000},"page":"694-715","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":80,"title":["Specifying timed state sequences in powerful decidable logics and timed automata"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Wilke","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"35_CR1","volume-title":"PhD thesis","author":"R. Alur","year":"1991","unstructured":"R. Alur. \u201cTechniques for Automatic Verification of Real-time Systems\u201d. PhD thesis, Stanford University, California (1991)."},{"issue":"1","key":"35_CR2","first-page":"1","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Inform. and Control104(1), 1\u201334 (1993).","journal-title":"Inform. and Control"},{"key":"35_CR3","series-title":"Vol. 736 of \u201cLecture Notes in Computer Science\u201d","volume-title":"Hybrid Systems","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, \u201cHybrid Systems\u201d, vol. 736 of \u201cLecture Notes in Computer Science\u201d. Springer-Verlag, Berlin (1993)."},{"issue":"2","key":"35_CR4","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill. A theory of timed automata. Theoret. Comput. Sci.126(2), 183\u2013235 (1994).","journal-title":"Theoret. Comput. Sci."},{"key":"35_CR5","series-title":"Vol. 443 of \u201cLecture Notes in Computer Science\u201d","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming: 17th International Colloquium","author":"R. Alur","year":"1990","unstructured":"R. Alur and D. L. Dill. Automata for modeling real-time systems. In M. S. Paterson, editor, \u201cAutomata, Languages and Programming: 17th International Colloquium\u201d, vol. 443 of \u201cLecture Notes in Computer Science\u201d, pp. 322\u2013335, Warwick, England (1990). European Assoc. Theoret. Comput. Sci., Springer-Verlag."},{"key":"35_CR6","first-page":"139","volume-title":"The benefits of relaxing punctuality","author":"R. Alur","year":"1991","unstructured":"R. Alur, T. Feder, and T. A. Henzinger. The benefits of relaxing punctuality. In \u201cProceedings of the 10th ACM Symposium on Principles of Distributed Computing\u201d, pp. 139\u2013152, Montreal, Qu ebec, Canada (1991). ACM Press."},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger. A really temporal logic. In \u201cProceedings of the 30th Annual Symposium on Foundations of Computer Science\u201d, pp. 164\u2013169. IEEE Computer Society Press (1989).","DOI":"10.1109\/SFCS.1989.63473"},{"key":"35_CR8","doi-asserted-by":"crossref","first-page":"390","DOI":"10.21236\/ADA323441","volume-title":"Real-time logics: complexity and expressiveness","author":"R. Alur","year":"1990","unstructured":"R. Alur and T. Henzinger. Real-time logics: complexity and expressiveness. In \u201cFifth Annual IEEE Symposium on Logic in Computer Science\u201d, pp. 390\u2013401, Philadelphia, Pennsylvania (1990). IEEE Computer Society Press."},{"key":"35_CR9","series-title":"Vol. 600 of \u201cLecture Notes in Computer Science\u201d","first-page":"74","volume-title":"Real-Time: Theory in Practice","author":"R. Alur","year":"1991","unstructured":"R. Alur and T. A. Henzinger. Logics and models of real-time: a survey. In J. W. de Bakker, C. Huizing, W. de Roever, and G. Rozenberg, editors, \u201cReal-Time: Theory in Practice\u201d, vol. 600 of \u201cLecture Notes in Computer Science\u201d, pp. 74\u2013106, Mook, The Netherlands (1991). Springer-Verlag."},{"key":"35_CR10","first-page":"177","volume-title":"Back to the future: towards a theory of timed regular languages","author":"R. Alur","year":"1992","unstructured":"R. Alur and T. A. Henzinger. Back to the future: towards a theory of timed regular languages. In \u201c33rd Annual Symposium on Foundations of Computer Science\u201d, pp. 177\u2013186, Pittsburgh, Pennsylvania (1992). IEEE Computer Society Press."},{"issue":"1","key":"35_CR11","first-page":"35","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur and T. A. Henzinger. Real-time logics: complexity and expressiveness. Inform. and Control104(1), 35\u201377 (1993).","journal-title":"Inform. and Control"},{"key":"35_CR12","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J. R. B\u00fcchi","year":"1960","unstructured":"J. R. B\u00fcchi. Weak second-order arithmetic and finite automata. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik6, 66\u201392 (1960).","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"key":"35_CR13","unstructured":"J. R. B\u00fcchi. On a decision method in restricted second-order arithmetic. In E. Nagel, P. Suppes, and A. Tarski, editors, \u201cLogic, Methodology, and Philosophy of Science: Proc. of the 1960 International Congress\u201d, pp. 1\u201311. Stanford University Press (1962)."},{"key":"35_CR14","first-page":"302","volume-title":"Lecture Notes in Computer Science","author":"K. \u010der\u0101ns","year":"1992","unstructured":"K. \u010der\u0101ns. Decidability of bisimulation equivalences for parallel timer processes. In G. v. Bochmann and D. K. Probst, editors, \u201cComputer Aided Verification, Fourth International Workshop, CAV '92'\u201d vol. 663 of \u201cLecture Notes in Computer Science\u201d, pp. 302\u2013315, Montreal, Canada (1992). Springer-Verlag."},{"issue":"5","key":"35_CR15","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1991","unstructured":"Z. Chaochen, C. Hoare, and A. Ravn. A calculus of durations. Information Processing Letters40(5), 269\u2013276 (1991).","journal-title":"Information Processing Letters"},{"key":"35_CR16","series-title":"Vol. 700 of \u201cLecture Notes in Computer Science\u201d","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/3-540-56939-1_84","volume-title":"Automata, Languages and Programming: 20th International Colloquium","author":"W. Ebinger","year":"1993","unstructured":"W. Ebinger and A. Muscholl. Logical definability on infinite traces. In A. Lingas, R. Karlsson, and S. Carlsson, editors, \u201cAutomata, Languages and Programming: 20th International Colloquium\u201d, vol. 700 of \u201cLecture Notes in Computer Science\u201d, pp. 335\u2013346, Lund, Sweden (1993). European Assoc. Theoret. Cornput. Sci., Springer-Verlag."},{"key":"35_CR17","series-title":"Vol. 600 of \u201cLecture Notes in Computer Science\u201d","first-page":"226","volume-title":"Real-Time: Theory in Practice","author":"T. A. Henzinger","year":"1991","unstructured":"T. A. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In J. W. de Bakker, C. Huizing, W. de Roever, and G. Rozenberg, editors, \u201cReal-Time: Theory in Practice\u201d, vol. 600 of \u201cLecture Notes in Computer Science\u201d, pp. 226\u2013251, Mook, The Netherlands (1991). Springer-Verlag."},{"key":"35_CR18","doi-asserted-by":"crossref","unstructured":"R. Koymans, J. Vytopil, and W. P. de Roever. Real-time programming and asynchronous message passing. In \u201cProceedings of the Second Annual ACM Symposium on Principles of Distributed Computing\u201d, pp. 187\u2013197. ACM Press (1983).","DOI":"10.1145\/800221.806721"},{"key":"35_CR19","first-page":"380","volume-title":"A logic of concrete time intervals","author":"H. R. Lewis","year":"1990","unstructured":"H. R. Lewis. A logic of concrete time intervals. In \u201cFifth Annual IEEE Symposium on Logic in Computer Science\u201d, pp. 380\u2013389, Philadelphia, Pennsylvania (1990). IEEE Computer Society Press."},{"issue":"2","key":"35_CR20","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1007\/BF01191722","volume":"30","author":"Z. Manna","year":"1993","unstructured":"Z. Manna and A. Pnueli. Models for reactivity. Acta Information30(2), 609\u2013678 (Oct. 1993).","journal-title":"Acta Information"},{"key":"35_CR21","first-page":"591","volume-title":"Lecture Notes in Computer Science","author":"A. Pnueli","year":"1992","unstructured":"A. Pnueli and Y. Kesten. Timed and hybrid Statecharts and their textual representation. In J. Vytopil, editor, \u201cFormal Techniques in Real-time and Faulttolerant Systems: Second International Symposium, Nijmegen, The Netherlands\u201d, vol. 571 of \u201cLecture Notes in Computer Science\u201d, pp. 591\u2013620, Nijmegen, The Netherlands (Jan. 1992). Springer-Verlag."},{"key":"35_CR22","first-page":"1","volume":"141","author":"M. O. Rabin","year":"1969","unstructured":"M. O. Rabin. Decidability of second-order theories and finite automata on infinite trees. Trans. Amer. Math. Soc.141, 1\u201335 (1969).","journal-title":"Trans. Amer. Math. Soc."},{"issue":"1","key":"35_CR23","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J. W. Thatcher","year":"1968","unstructured":"J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem of second-order arithmetic. Math. Systems Theory2(1), 57\u201381 (1968).","journal-title":"Math. Systems Theory"},{"key":"35_CR24","unstructured":"Th. Wilke. Automaten und Logiken zur Beschreibung zeitabh\u00c4ngiger Systeme. Technical Report 9407, Christian-Albrechts-Universit\u00c4t zu Kiel, Institut f\u00fcr Informatik und Praktische Mathematik (July 1994)."},{"key":"35_CR25","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal logic can be more expressive. Inform. and Control56, 72\u201399 (1983).","journal-title":"Inform. and Control"},{"key":"35_CR26","doi-asserted-by":"crossref","unstructured":"P. Wolper, M. Y. Vardi, and A. P. Sistla. Reasoning about infinite computation paths. In \u201c24th Annual Symposium on Foundations of Computer Science\u201d, pp. 185\u2013194. IEEE Computer Society Press (1983).","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58468-4_191","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:54:04Z","timestamp":1578509644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58468-4_191"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584681","9783540489849"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-58468-4_191","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}