{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T06:00:51Z","timestamp":1774332051244,"version":"3.50.1"},"reference-count":114,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1997,5,1]],"date-time":"1997-05-01T00:00:00Z","timestamp":862444800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1997,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The Duration Calculus (abbreviated DC) represents a logical approach for formal design of real-time systems, where real numbers are used to model time and Boolean valued functions over time are used to model states and events of real-time systems. Since its introduction, DC has been applied to many case studies and it has been extended in several directions. The aim of this paper is to provide a thorough presentation of the logic.<\/jats:p>","DOI":"10.1007\/bf01211086","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T15:42:36Z","timestamp":1109346156000},"page":"283-330","source":"Crossref","is-referenced-by-count":91,"title":["Duration calculus: Logical foundations"],"prefix":"10.1145","volume":"9","author":[{"given":"Michael R.","family":"Hansen","sequence":"first","affiliation":[{"name":"Department of Information Technology, Technical University of Denmark, Building 344, DK-2800, Lyngby, Denmark"}]},{"given":"Zhou","family":"Chaochen","sequence":"additional","affiliation":[{"name":"International Institute for Software Technology, United Nations University, Macau"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/182.358434"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(84)90008-0"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Alur R. Courcoubetis C. and Dill D.: Model-Checking for Real-Time Systems. In Fifth Annual IEEE Symp. on Logic in Computer Science IEEE Press 1990 pages 414\u2013425.","DOI":"10.1109\/LICS.1990.113766"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Alur R. Courcoubetis C. Henzinger T. and Ho P-H.: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In [GNR93] pages 209\u2013229.","DOI":"10.1007\/3-540-57318-6_30"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Alur R. and Dill D.: The Theory of Timed Automata. In Real-Time: Theory in Practice LNCS 600 Springer-Verlag 1992 pages 45\u201373.","DOI":"10.1007\/BFb0031987"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Alur R. Feder T. and Henzinger T.: The Benefits of Relaxing Punctuality. In Tenth Annual ACM Symposium on Principles of Distributed Computing ACM Press 1991 pages 139\u2013152.","DOI":"10.1145\/112600.112613"},{"key":"e_1_2_1_2_7_2","unstructured":"Benthem J. F. A. K. van: The Logic of Time . D. Reidel publishing Company 1983."},{"key":"e_1_2_1_2_8_2","unstructured":"Bird R.: Programs and Machines . John Wiley & Sons 1976."},{"key":"e_1_2_1_2_9_2","first-page":"60","article-title":"A ProCoS Project Description: ESPRIT BRA 3104","volume":"39","author":"Bj\u00f8rner D.","year":"1989","journal-title":"Bulletin of the EATCS"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bouajjani A. Echahed R. and Robbana R.: Verifying Invariance Properties of Timed Systems with Duration Variables. In [LRV94] pages 193\u2013210.","DOI":"10.1007\/3-540-58468-4_166"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Bouajjani A. Echahed R. and Sifakis J.: On Model Checking for Real-Time Properties with Durations. In Eights Annual IEEE Symp. on Logic in Computer Science IEEE Press 1993 pages 147\u2013159.","DOI":"10.1109\/LICS.1993.287592"},{"key":"e_1_2_1_2_12_2","unstructured":"Brien S.: A time Interval Calculus . Master's thesis Programming Research Group Computing Laboratory Oxford University 1991."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Chan P. and Dang Van Hung: Duration Calculus Specification of Scheduling for Tasks with Shared Resources. In Asian Computing Science Conference 1995 LNCS 1023 Springer-Verlag 1995 pages 365\u2013380.","DOI":"10.1007\/3-540-60688-2_56"},{"key":"e_1_2_1_2_14_2","volume-title":"UNU\/IIST Report No. 25, UNU\/IIST","author":"Van Dang Hung","year":"1994"},{"key":"e_1_2_1_2_15_2","volume-title":"UNU\/IIST Report No. 35, UNU\/IIST","author":"Van Dang Hung","year":"1994"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Dietz C.: Graphical Formalization of Real-Time Requirements . Technical report Fachbereich Informatik Oldenburg University 1996.","DOI":"10.1007\/3-540-61648-9_51"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Dutertre B.: Complete Proof Systems for First Order Interval Temporal Logic. In Tenth Annual IEEE Symp. on Logic in Computer Science IEEE Press 1995 pages 36\u201343.","DOI":"10.1109\/LICS.1995.523242"},{"key":"e_1_2_1_2_18_2","volume-title":"Report no. CSD-TR-94-3","author":"Dutertre B.","year":"1995"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Engel M. Kubica M. Madey J. Parnas D. L. Ravn A. P. and Schouwen A. J. van: A Formal Approach to Computer Systems Requirements Documentation. In [GNR93] pages 452\u2013474.","DOI":"10.1007\/3-540-57318-6_40"},{"key":"e_1_2_1_2_20_2","unstructured":"Engel M. and Rischel H.: Dagstuhl-Seminar Specification Problem \u2014 a Duration Calculus Solution . Department of Computer Science Technical University of Denmark \u2014 Private Communication 1993."},{"key":"e_1_2_1_2_21_2","unstructured":"Fr\u00e4nzle M.: Controller Design from Temporal Logic: Undecidability need not matter PhD thesis Kiel University submitted December 1996."},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Goswami A. Bell Michael and Joseph Mathai: ISL: An Interval Logic for the Specification of Real-Time Programs. In Formal Techniques in Real-Time and Fault-Tolerant Systems LNCS 571 Springer-Verlag 1991 pages 1\u201320.","DOI":"10.1007\/3-540-55092-5_1"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Grossman R. L. Nerode A. Ravn A. P. and Rischel H. (eds).: Hybrid Systems LNCS 736 Springer-Verlag 1993.","DOI":"10.1007\/3-540-57318-6"},{"key":"e_1_2_1_2_24_2","volume-title":"PhD thesis","author":"Hale R.","year":"1988"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Halpern J. Moskowski B. and Manna Z.: A Hardware Semantics based on Temporal Intervals. In ICALP'83 LNCS 154 Springer-Verlag 1983 pages 278\u2013291.","DOI":"10.1007\/BFb0036915"},{"key":"e_1_2_1_2_26_2","unstructured":"Halpern J. Y. and Shoham Y.: A Propositional Modal Logic of Time Intervals. In Symposium on Logic in Computer Science IEEE Press 1986 pages 279\u2013292."},{"key":"e_1_2_1_2_27_2","unstructured":"K. M. Hansen Ravn A. P. and Stavridou V.: From Safety Analysis to Formal Specification . Technical report Department of Information Technology Technical University of Denmark 1996."},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213605"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Hansen M. R. and Zhou Chaochen: Semantics and Completeness of Duration Calculus. In Real-Time: Theory in Practice LNCS 600 Springer-Verlag 1992 pages 209\u2013225.","DOI":"10.1007\/BFb0031994"},{"key":"e_1_2_1_2_30_2","volume-title":"TAU'92: 1992 Workshop on Timing Issues in the Specification and Synthesis of Digital Systems","author":"Hansen M. R.","year":"1992"},{"key":"e_1_2_1_2_31_2","volume-title":"Report no. OLD MRH 1\/1, ProCoS II, ESPRIT BRA 7071","author":"Hansen M. R.","year":"1993"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00145-9"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Harel E. Lichtenstein O. and Pnueli A.: Explicit Clock Temporal Logic. In Symp. on Logic in Comp. Sci. IEEE press 1990 pages 402\u2013413.","DOI":"10.1109\/LICS.1990.113765"},{"key":"e_1_2_1_2_34_2","unstructured":"He Jifeng: From CSP to Hybrid Systems. In A Classical Mind: Essays in Honour of C.A.R. Hoare Prentice Hall 1994 pages 171\u2013190."},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"He Jifeng and Bowen J.: Time Interval Semantics and Implementation of a Real-Time Programming Language. In 1992 Euromicro Workshop on Real-Time Systems . IEEE Press 1992.","DOI":"10.1109\/EMWRT.1992.637480"},{"issue":"9","key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","first-page":"734","DOI":"10.1093\/comjnl\/38.9.734","article-title":"A Case Study of Optimization","volume":"38","author":"He Weidong","year":"1995","journal-title":"The Computer Journal"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Hooman J.: Correctness of Real Time Systems by Construction. In [LRV94] pages 19\u201340.","DOI":"10.1007\/3-540-58468-4_158"},{"key":"e_1_2_1_2_38_2","unstructured":"Hopcroft J. E. and Ullman J. D.: Introduction to Automata Theory Languages and Computation . Addison-Wesley 1979."},{"key":"e_1_2_1_2_39_2","unstructured":"Hughes G. E. and Crestwell M. J.: An Introduction to Modal Logic . Routledge 1968."},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00258426"},{"key":"e_1_2_1_2_41_2","unstructured":"Inal R.: Modular Specification of Real-Time Systems. In 1994 Euromicro Workshop on Real-Time Systems IEEE Press 1994."},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.5555\/12868.12870"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Kapur A. Henzinger T. Manna Z. and Pnueli A.: Proving Safety Properties of Hybrid Systems. In [LRV94] pages 431\u2013454.","DOI":"10.1007\/3-540-58468-4_177"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Kesten Y. Pnueli A. Sifakis J. and Yovine S.: Integration Graphs: A Class of Decidable Hybrid Systems. In [GNR93] pages 179\u2013208.","DOI":"10.1007\/3-540-57318-6_29"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Koymans R.: Specifying Message Passing and Time-Critical Systems with Temporal Logic . LNCS 651 Springer-Verlag 1992.","DOI":"10.1007\/3-540-56283-4"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"K\u00e4\u00e4ramees M.: Transforming Designs Towards Implementations. In 1995 Euromicro Workshop on Real-Time Systems IEEE Press 1995 pages 197\u2013204.","DOI":"10.1109\/EMWRTS.1995.514312"},{"key":"e_1_2_1_2_48_2","volume-title":"Master's thesis","author":"K\u00e4\u00e4ramees M.","year":"1995"},{"key":"e_1_2_1_2_49_2","unstructured":"Lakhnech Y.: Specification and Verification of Hybrid and Real-Time Systems . PhD thesis Kiel University 1996."},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Lakhnech Y. and Hooman J.: Reasoning about Durations in Metric Temporal Logic. In [LRV94] pages 488\u2013510.","DOI":"10.1007\/3-540-58468-4_180"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Lamport L.: Hybrid Systems in TLA+. In [GNR93] pages 77\u2013102.","DOI":"10.1007\/3-540-57318-6_25"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Langmack H. Roever W.-P. de and Vytopil J. (eds).: Formal Techniques in Real-Time and Fault-Tolerant Systems LNCS 863 Springer-Verlag 1994.","DOI":"10.1007\/3-540-58468-4"},{"key":"e_1_2_1_2_53_2","unstructured":"Li Xiaoshan: A Mean Value Calculus . PhD thesis Software Institute Academia Sinica 1993."},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Li Xuandong and Dang Van Hung: Checking Linear Duration Invariants by Linear Programming. In Concurrency and Parallelism Programming Network and Security LNCS 1179 Springer-Verlag 1996.","DOI":"10.1007\/BFb0027804"},{"key":"e_1_2_1_2_55_2","first-page":"30","volume-title":"Dependable Computing and Fault-Tolerant Systems Vol. 7: Responsive Computer Systems","author":"Liu Zhiming","year":"1993"},{"issue":"1","key":"e_1_2_1_2_56_2","first-page":"49","article-title":"Towards a Calculus of Systems Dependability","volume":"1","author":"Zhiming Liu","year":"1994","journal-title":"High Integrity Systems"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems . Springer Verlag 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A.: Verifying Hybrid Systems. In [GNR93] pages 4\u201335.","DOI":"10.1007\/3-540-57318-6_22"},{"key":"e_1_2_1_2_59_2","volume-title":"UNU\/IIST Report No. 77, UNU\/IIST","author":"Mao Xiaoguang","year":"1996"},{"key":"e_1_2_1_2_60_2","unstructured":"Masiero P. C. Ravn A. P. and Rischel H.: Refinement of Real-Time Specifications . Report no. ID\/DTH PCM 1\/1 ProCoS II ESPRIT BRA 7071 Department of Computer Science Technical University of Denmark 1993."},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Melliar-Smith P. M.: Extending Interval Logic to Real Time Systems. In Temporal Logic in Specification LNCS 398 Springer-Verlag 1987 pages 224\u2013242.","DOI":"10.1007\/3-540-51803-7_29"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_1_2_63_2","unstructured":"Moszkowski B.: Reasoning about Digital Circuits . PhD thesis Stanford University 1983."},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1985.1662795"},{"key":"e_1_2_1_2_65_2","unstructured":"Moszkowski B.: Compositional Reasoning about Projected and Infinite Time. In First IEEE Intl. Conf. on Engineering of Complex Computer Systems IEEE press 1995."},{"key":"e_1_2_1_2_66_2","doi-asserted-by":"publisher","DOI":"10.5555\/6240"},{"key":"e_1_2_1_2_67_2","unstructured":"Moszkowski B.: Some Very Compositional Temporal Properties. In Programming Concepts Methods and Calculi IFIP Transactions Vol. A-56 North-Holland 1994 pages 307\u2013326."},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"M\u00f8rk S. Godskesen J. C. Hansen M. R. and Sharp R.: A Timed Semantics for SDL. In Formal Description Techniques IX: Theory application and tools Chapman & Hall 1996 pages 295\u2013309.","DOI":"10.1007\/978-0-387-35079-0_18"},{"key":"e_1_2_1_2_69_2","doi-asserted-by":"crossref","unstructured":"Nicollin X. Olivero A. Sifakis J. and Yovine S.: An Approach to the Description and Analysis of Hybrid Systems. In [GNR93] pages 149\u2013178.","DOI":"10.1007\/3-540-57318-6_28"},{"key":"e_1_2_1_2_70_2","unstructured":"Olderog E-R. Ravn A. P. and Skakkeb\u00e6k J. U.: Refining System Requirements to Program Specifications. In Formal Methods in Real-Time Systems Trends in Software-Engineering Chapter 5 Wiley 1996 pages 107\u2013134."},{"key":"e_1_2_1_2_71_2","volume-title":"Technical report","author":"Owre S.","year":"1993"},{"key":"e_1_2_1_2_72_2","volume-title":"Report no. TCS-95\/9","author":"Pandya P. K.","year":"1995"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","unstructured":"Pandya P. K.: Weak Chop Inverses and Liveness in Duration Calculus. In Formal Techniques in Real-Time and Fault-Tolerant Systems LNCS 1135 Springer-Verlag 1996 pages 148\u2013167.","DOI":"10.1007\/3-540-61648-9_39"},{"key":"e_1_2_1_2_74_2","volume-title":"Report no. TCS-95\/3","author":"Pandya P. K.","year":"1995"},{"key":"e_1_2_1_2_75_2","unstructured":"Pandya P. K. Ramakrishna Y. S. and Shyamasundar R. K.: A Compositional Semantics of Esterel in Duration Calculus. In Proc. Second AMAST workshop on Real-Time systems: Models and Proofs Bordeux June 1995."},{"key":"e_1_2_1_2_76_2","unstructured":"Petersen J. L. and Rischel H.: Formalizing Requirements and Design for a Production Cell System. In Symposium ADPM '94: Automatisation des Processus Mixtes: Les Systemes Dynamiques Hybrides Belgian Institute of Automatic Control IBRA 1994 pages 37\u201346."},{"key":"e_1_2_1_2_77_2","doi-asserted-by":"crossref","unstructured":"Ravn A. P. Rischel H. Holdgaard M. Eriksen T. J. Conrad F. and Andersen T. O.: Hybrid Control of a Robot \u2014 a case study. In Hybrid Systems II LNCS 999 Springer-Verlag 1995 pages 391\u2013404.","DOI":"10.1007\/3-540-60472-3_20"},{"key":"e_1_2_1_2_78_2","volume-title":"Doctoral Dissertation, ID-TR: 1995-170","author":"Ravn A. P.","year":"1995"},{"key":"e_1_2_1_2_79_2","unstructured":"Ravn A. P. and Rischel H.: Requirements Capture for embedded real-time systems. In Proceedings of IMACS-MCTS'91 Symposium on Modelling and Control of Technological Systems Villeneuve d'Ascq France May 7\u201310 volume 2 IMACS 1991 pages 147\u2013152."},{"key":"e_1_2_1_2_80_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.210306"},{"key":"e_1_2_1_2_81_2","unstructured":"Rischel H.: A Duration Calculus Proof of Fischer's Mutual Exclusion Protocol . Report no. DTH HR 4\/1 ProCoS II ESPRIT BRA 7071 Department of Computer Science Technical University Of Denmark 1992."},{"key":"e_1_2_1_2_82_2","unstructured":"Rosner R. and Pnueli A.: A Choppy Logic. In First Annual IEEE Symp. on Logic in Computer Science IEEE Press 1986 pages 306\u2013313."},{"key":"e_1_2_1_2_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00262866"},{"key":"e_1_2_1_2_84_2","doi-asserted-by":"crossref","unstructured":"Schenke M.: Specification and Transformation of Reactive Systems with Time Restrictions and Concurrency. In [LRV94] pages 605\u2013620.","DOI":"10.1007\/3-540-58468-4_186"},{"key":"e_1_2_1_2_85_2","unstructured":"Schenke M.: Requirements to Programs: A Development Methodology for Real Time Systems Part 2 . Technical report Fachbereich Informatik Universit\u00e4t Oldenburg 1995. (To appear in Acta Informatica.)"},{"key":"e_1_2_1_2_86_2","unstructured":"Schenke M. and Olderog E.-R.: Requirements to Programs: A Development Methodology for Real Time Systems Part 1 . Technical report Fachbereich Informatik Universit\u00e4t Oldenburg 1995."},{"key":"e_1_2_1_2_87_2","doi-asserted-by":"crossref","unstructured":"Schwartz R. L. Melliar-Smith P. M. and Vogt F. H.: An Interval Logic for Higher-Level Temporal Reasoning. In Second Annual ACM Symposium on Principles of Distributed Computing ACM 1983 pages 173\u2013186.","DOI":"10.1145\/800221.806720"},{"key":"e_1_2_1_2_88_2","doi-asserted-by":"crossref","unstructured":"Sipma H. B. and Manna Z.: Specification and Verification of Controlled Systems. In [LRV94] pages 641\u2013659.","DOI":"10.1007\/3-540-58468-4_188"},{"key":"e_1_2_1_2_89_2","doi-asserted-by":"crossref","unstructured":"Skakkeb\u00e6k J. U.: Liveness and Fairness in Duration Calculus. In CONCUR'94: Concurrency Theory LNCS 836 Springer Verlag 1994 pages 283\u2013298.","DOI":"10.1007\/978-3-540-48654-1_23"},{"key":"e_1_2_1_2_90_2","unstructured":"Skakkeb\u00e6k J. U.: A Verification Assistant for a Real-Time Logic . PhD thesis Department of Computer Science Technical University of Denmark 1994."},{"key":"e_1_2_1_2_91_2","doi-asserted-by":"crossref","unstructured":"Skakkeb\u00e6k J. U. Ravn A. P. Rischel H. and Zhou Chaochen: Specification of Embedded Real-Time Systems. In Proceedings of 1992 Euromicro Workshop on Real-Time Systems IEEE Press 1992.","DOI":"10.1109\/EMWRT.1992.637481"},{"key":"e_1_2_1_2_92_2","volume-title":"Report no. SRI-CSL-93-10","author":"Skakkeb\u00e6k J. U.","year":"1993"},{"key":"e_1_2_1_2_93_2","doi-asserted-by":"crossref","unstructured":"Skakkeb\u00e6k J. U. and Shankar N.: Towards a Duration Calculus Proof Assistant in PVS. In [LRV94] pages 660\u2013679.","DOI":"10.1007\/3-540-58468-4_189"},{"key":"e_1_2_1_2_94_2","unstructured":"Skakkeb\u00e6k J. U. and Sestoft P.: Checking Validity of Duration Calculus Formulas . Report no. ID\/DTH JUS 3\/1 ProCoS II ESPRIT BRA 7071 Department of Computer Science Technical University of Denmark 1994."},{"key":"e_1_2_1_2_95_2","unstructured":"S\u00f8rensen E. V Ravn A. P. and Rischel H.: Control Program for a Gas Burner: Part 1: Informal Requirements ProCoS Case Study 1 . Report no. ID\/DTH EVS2 ProCoS ESPRIT BRA 3104 Department of Computer Science Technical University of Denmark 1990."},{"key":"e_1_2_1_2_96_2","doi-asserted-by":"publisher","DOI":"10.2307\/2268577"},{"key":"e_1_2_1_2_97_2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093635589"},{"key":"e_1_2_1_2_98_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.453"},{"key":"e_1_2_1_2_99_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00205-D"},{"key":"e_1_2_1_2_100_2","unstructured":"Widjaja Belawati H. Chen Zongji He Weidong and Zhou Chaochen: A Cooperative Design for Hybrid Control Systems. In Logic and Software Engineering International Workshop in Honor of Chih-Sung Tang World Scientific 1996 pages 127\u2013150."},{"key":"e_1_2_1_2_101_2","unstructured":"Xu Qiwen and Yang Zengyu: Derivation of Control Programs: a Heating System. Presented at the 4th International Conference on Hybrid Systems Ithaca NY USA 1996."},{"key":"e_1_2_1_2_102_2","doi-asserted-by":"crossref","unstructured":"Xu Quiwen and He Weidong: Hierarchical Design of a Chemical Concentration Control System. In Hybrid Systems III LNCS 1066 Springer-Verlag 1996 pages 270\u2013281.","DOI":"10.1007\/BFb0020952"},{"key":"e_1_2_1_2_103_2","doi-asserted-by":"crossref","unstructured":"Yu Xinyao Wang Ji Zhou Chaochen and Pandya Paritosh K.: Formal Design of Hybrid Systems. In [LRV94] pages 738\u2013755.","DOI":"10.1007\/3-540-58468-4_193"},{"key":"e_1_2_1_2_104_2","doi-asserted-by":"crossref","unstructured":"Zheng Yuhua and Zhou Chaochen: A Formal Proof of the Deadline Driven Scheduler. In [LRV94] pages 756\u2013775.","DOI":"10.1007\/3-540-58468-4_194"},{"key":"e_1_2_1_2_105_2","volume-title":"UNU\/IIST Report No. 91, UNU\/IIST","author":"Zhou Chaochen","year":"1996"},{"key":"e_1_2_1_2_106_2","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen and Hansen M. R.: Chopping a Point. In BCS-FACS 7th refinement workshop Electronic Workshops in Computing Springer-Verlag 1996.","DOI":"10.14236\/ewic\/RW1996.4"},{"key":"e_1_2_1_2_107_2","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen Hansen M. R. Ravn A. P. and Rischel H.: Duration Specifications for Shared Processors. In Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems LNCS 571 Springer-Verlag 1991 pages 21\u201332.","DOI":"10.1007\/3-540-55092-5_2"},{"key":"e_1_2_1_2_108_2","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen Hansen M.R. and Sestoft P.: Decidability and Undecidability Results for Duration Calculus. In STACS'93 LNCS 665 Springer-Verlag 1993 pages 58\u201368.","DOI":"10.1007\/3-540-56503-5_8"},{"key":"e_1_2_1_2_109_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"e_1_2_1_2_110_2","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen Dang Van Hung and Li Xiaoshan: A Duration Calculus with Infinite Intervals. In Fundamentals of Computation Theory LNCS 965 Springer-Verlag 1995 pages 16\u201341.","DOI":"10.1007\/3-540-60249-6_39"},{"key":"e_1_2_1_2_111_2","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen Wang Ji and Ravn Anders P.: A Formal Description of Hybrid Systems. In Hybrid Systems III LNCS 1066 Springer-Verlag 1996 pages 511\u2013530.","DOI":"10.1007\/BFb0020972"},{"key":"e_1_2_1_2_112_2","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen Zhang Jingzhong Yang Lu and Li Xiaoshan: Linear Duration Invariants. In [LRV94] pages 86\u2013109.","DOI":"10.1007\/3-540-58468-4_161"},{"key":"e_1_2_1_2_113_2","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen Ravn A. P. and Hansen M. R.: An Extended Duration Calculus for Hybrid Systems. In [GNR93] pages 36\u201359.","DOI":"10.1007\/3-540-57318-6_23"},{"key":"e_1_2_1_2_114_2","unstructured":"Zhou Chaochen and Li Xiaoshan: A Mean Value Calculus of Durations. In A Classical Mind: Essays in Honour of C. A. R. Hoare Prentice Hall 1994 pages 431\u2013451."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211086.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211086\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211086","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,23]],"date-time":"2024-12-23T23:06:02Z","timestamp":1734995162000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211086"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,5]]},"references-count":114,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,5]]}},"alternative-id":["10.1007\/BF01211086"],"URL":"https:\/\/doi.org\/10.1007\/bf01211086","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,5]]}}}