{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T02:01:30Z","timestamp":1791424890068,"version":"4.3.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540555643","type":"print"},{"value":"9783540472186","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/bfb0031987","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T01:36:29Z","timestamp":1134264989000},"page":"45-73","source":"Crossref","is-referenced-by-count":114,"title":["The theory of timed automata"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,26]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking for real-time systems. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, pages 414\u2013425, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking for probabilistic real-time systems. In Automata, Languages and Programming: Proceedings of the 18th ICALP, Lecture Notes in Computer Science 510, 1991.","DOI":"10.1007\/3-540-54233-7_128"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Tom\u00e1s Feder, and Thomas Henzinger. The benefits of relaxing punctuality. In Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, pages 139\u2013152, 1991.","DOI":"10.1145\/112600.112613"},{"key":"3_CR4","unstructured":"Rajeev Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford University, 1991."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, D.L. Dill, L.J. Hwang, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, pages 428\u2013439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"3_CR6","unstructured":"Richard B\u00fcchi. On a decision method in restricted second-order arithmetic. In Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science 1960, pages 1\u201312. Stanford University Press, 1962."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, I.A. Draghicescu, and R.P. Kurshan. A unified approach for showing language containment and equivalence between various types of \u03c9-automata. Technical report, Carnegie Mellon University, 1989.","DOI":"10.1007\/3-540-52590-4_43"},{"issue":"2","key":"3_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Edmund Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR9","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Yaacov Choueka. Theories of automata on \u03c9-tapes: a simplified approach. Journal of Computer and System Sciences, 8:117\u2013141, 1974.","journal-title":"Journal of Computer and System Sciences"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Costas Courcoubetis and Mihalis Yannakakis. Minimum and maximum delay problems in real-time systems. In Proceedings of the Third Workshop on Computer-Aided Verification, Aalborg University, Denmark, 1991.","DOI":"10.1007\/3-540-55179-4_37"},{"key":"3_CR11","unstructured":"David Dill and Howard Wong-Toi. Synthesizing processes and schedulers from temporal specifications. In Proceedings of the Second Workshop on Computer-Aided Verification, Rutgers University, 1990."},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. A. Emerson","year":"1982","unstructured":"E. Allen Emerson and Edmund M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241\u2013266, 1982.","journal-title":"Science of Computer Programming"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid and Pierre Wolper. A partial approach to model-checking. In Proceedings of the Sixth IEEE Symposium on Logic in Computer Science, pages 406\u2013415, 1991.","DOI":"10.1109\/LICS.1991.151664"},{"issue":"8","key":"3_CR14","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666\u2013677, 1978.","journal-title":"Communications of the ACM"},{"key":"3_CR15","unstructured":"John Hopcroft and Jeff Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979."},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/0022-0000(87)90036-5","volume":"35","author":"R. Kurshan","year":"1987","unstructured":"Robert Kurshan. Complementing deterministic B\u00fcchi automata in polynomial time. Journal of Computer and System Sciences, 35:59\u201371, 1987.","journal-title":"Journal of Computer and System Sciences"},{"key":"3_CR17","unstructured":"Leslie Lamport. What good is temporal logic? In R.E.A. Mason, editor, Information Processing 83: Proceedings of the Ninth IFIP World Computer Congress, pages 657\u2013668. Elsevier Science Publishers, 1983."},{"key":"3_CR18","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","volume":"9","author":"R. McNaughton","year":"1966","unstructured":"Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521\u2013530, 1966.","journal-title":"Information and Control"},{"key":"3_CR19","unstructured":"Zohar Manna and Amir Pnueli. The temporal framework for concurrent programs. In R.S. Boyer and J.S. Moore, editors, The correctness problem in Computer science, pages 215\u2013274. Academic Press, 1981."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46\u201377, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In Current Trends in Concurrency, Lecture Notes in Computer Science 224, pages 510\u2013584. Springer-Verlag, 1986.","DOI":"10.1007\/BFb0027047"},{"key":"3_CR22","unstructured":"Hartley Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Shmuel Safra. On the complexity of \u03c9-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 319\u2013327, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"issue":"2-3","key":"3_CR24","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A. Prasad Sistla","year":"1987","unstructured":"A. Prasad Sistla, Moshe Vardi, and Pierre Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic. Theoretical Computer Science, 49, 1987.","journal-title":"Theoretical Computer Science"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Wolfgang Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133\u2013191. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"3_CR26","unstructured":"Moshe Vardi. Verification of concurrent programs \u2014 the automata-theoretic framework. In Proceedings of the Second IEEE Symposium on Logic in Computer Science, pages 167\u2013176, 1987."},{"key":"3_CR27","unstructured":"Moshe Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First IEEE Symposium on Logic in Computer Science, pages 332\u2013344, 1986."},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Howard Wong-Toi and Girard Hoffmann. The control of dense real-time discrete event systems. 1991.","DOI":"10.21236\/ADA325997"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Pierre Wolper, Moshe Vardi, and A. Prasad Sistla. Reasoning about infinite computation paths. In Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, pages 185\u2013194, 1983.","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","Real-Time: Theory in Practice"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031987","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T17:21:05Z","timestamp":1683307265000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031987"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540555643","9783540472186"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/bfb0031987","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992]]}}}