{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:19:23Z","timestamp":1778498363061,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540616481","type":"print"},{"value":"9783540706533","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61648-9_40","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:09:41Z","timestamp":1330294181000},"page":"168-187","source":"Crossref","is-referenced-by-count":8,"title":["Synthesizing controllers from Duration Calculus"],"prefix":"10.1007","author":[{"given":"Martin","family":"Fr\u00e4nzle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J. R. B\u00fcchi","year":"1969","unstructured":"J. R. B\u00fcchi and L. H. Landweber. Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc., 138:295\u2013311, 1969.","journal-title":"Trans. Amer. Math. Soc."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Yassine Lakhnech, and Riadh Robbana. From duration calculus to linear hybrid automata. In Pierre Wolper, editor, Computer Aided Verification (CAV '95), volume 939 of Lecture Notes in Computer Science. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60045-0_51"},{"key":"10_CR3","volume-title":"ProCoS Technical Report Kiel MF 17\/3","author":"M. Fr\u00e4nzle","year":"1995","unstructured":"Martin Fr\u00e4nzle. A discrete model of VLSI dynamics in hybrid control applications. ProCoS Technical Report Kiel MF 17\/3, Christian-Albrechts Universit\u00e4t Kiel, Germany, April 1995."},{"key":"10_CR4","volume-title":"Dissertation, Institut f\u00fcr Informatik und Prakt","author":"M. Fr\u00e4nzle","year":"1996","unstructured":"Martin Fr\u00e4nzle. Controller Design from Temporal Logic: Undecidability need not matter. Dissertation, Institut f\u00fcr Informatik und Prakt. Mathematik der Christian-Albrechts-Universit\u00e4t Kiel, Germany, to appear 1996."},{"issue":"6A","key":"10_CR5","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1007\/BF01213605","volume":"6","author":"M. R. Hansen","year":"1994","unstructured":"Michael R. Hansen. Model-checking discrete duration calculus. Formal Aspects of Computing, 6(6A):826\u2013845, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"10_CR6","unstructured":"Jifeng He, C. A. R. Hoare, Martin Fr\u00e4nzle, Markus M\u00fcller-Olm, Ernst-R\u00fcdiger Olderog, Michael Schenke, Michael R. Hansen, Anders P. Ravn, and Hans Rischel. Provably correct systems. In Langmaack et al. [LdRV94], pages 288\u2013335."},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What's decidable about hybrid automata. In Proceedings of the Twenty-Seventh Annual ACM Symposium on the Theory of Computing, pages 373\u2013382. ACM, 1995.","DOI":"10.1145\/225058.225162"},{"key":"10_CR8","volume-title":"Constructing circuits from decidable duration calculus","author":"M. R. Hansen","year":"1993","unstructured":"Michael R. Hansen and Ernst-R\u00fcdiger Olderog. Constructing circuits from decidable duration calculus. Unpublished Note, Fachbereich Informatik, Universit\u00e4t Oldenburg, Germany, June 1993."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"H. Langmaack, W.-P. de Roever, and J. Vytopil, editors. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT '94), volume 863 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58468-4"},{"issue":"2","key":"10_CR10","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B. Moszkowski","year":"1985","unstructured":"Ben Moszkowski. A temporal logic for multi-level reasoning about hardware. IEEE Computer, 18(2):10\u201319, 1985.","journal-title":"IEEE Computer"},{"issue":"1","key":"10_CR11","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/32.210306","volume":"19","author":"A. P. Ravn","year":"1993","unstructured":"Anders P. Ravn, Hans Rischel, and Kirsten M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, 19(1):41\u201355, January 1993.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10_CR12","first-page":"3","volume-title":"The Mathematical Theory of Communication","author":"C. E. Shannon","year":"1949","unstructured":"Claude E. Shannon. The mathematical theory of communication. In The Mathematical Theory of Communication, pages 3\u201391. The University of Illinois Press: Urbana, 1949."},{"key":"10_CR13","unstructured":"Jens Ulrik Skakkeb\u00e6k and Peter Sestoft. Checking validity of duration calculus formulas. ProCoS Technical Report ID\/DTH JUS 3\/1, Technical University of Denmark, March 1994."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Wolfgang Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 4, pages 133\u2013191. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Thomas Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In Langmaack et al. [LdRV94], pages 694\u2013715.","DOI":"10.1007\/3-540-58468-4_191"},{"issue":"5","key":"10_CR16","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1991","unstructured":"Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269\u2013276, 1991.","journal-title":"Information Processing Letters"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen, Michael R. Hansen, and Peter Sestoft. Decidability and undecidability results for duration calculus. In P. Enjalbert, A. Finkel, and K. W. Wagner, editors, Symposium on Theoretical Aspects of Computer Science (STACS 93), volume 665 of Lecture Notes in Computer Science, pages 58\u201368. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56503-5_8"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen, Zhang Jingzhong, Yang Lu, and Li Xiaoshan. Linear duration invariants. In Langmaack et al. [LdRV94], pages 86\u2013109.","DOI":"10.1007\/3-540-58468-4_161"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61648-9_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:09:00Z","timestamp":1605647340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61648-9_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616481","9783540706533"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61648-9_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}