{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:19:58Z","timestamp":1778498398642,"version":"3.51.4"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2004,5,1]],"date-time":"2004-05-01T00:00:00Z","timestamp":1083369600000},"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":[[2004,5]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            Since the seminal work of Zhou Chaochen, M. R. Hansen, and P. Sestoft on decidability of dense-time Duration Calculus [ZHS93] it is well known that decidable fragments of Duration Calculus can only be obtained through withdrawal of much of the interesting vocabulary of this logic. While this was formerly taken as an indication that key-press verification of implementations with respect to elaborate Duration Calculus specifications were also impossible, we show that the model property is well decidable for\n            <jats:italic>realistic<\/jats:italic>\n            designs which feature natural constraints on their switching dynamics.\n          <\/jats:p>\n          <jats:p>The key issue is that the classical undecidability results rely on a notion of validity of a formula that refers to a class of models which is considerably richer than the possible behaviours of actual embedded real-time systems: that of finitely variable trajectories. By analysing two suitably sparser model classes we obtain model-checking procedures for rich subsets of Duration Calculus. Together with undecidability results also obtained, this sheds light upon the exact borderline between decidability and undecidability of Duration Calculi and related logics.<\/jats:p>","DOI":"10.1007\/s00165-004-0032-y","type":"journal-article","created":{"date-parts":[[2004,4,26]],"date-time":"2004-04-26T10:37:58Z","timestamp":1082975878000},"page":"121-139","source":"Crossref","is-referenced-by-count":18,"title":["Model-checking dense-time Duration Calculus"],"prefix":"10.1145","volume":"16","author":[{"given":"Martin","family":"Fr\u00e4nzle","sequence":"first","affiliation":[{"name":"Informatics and Mathematical Modelling, Technical University of Denmark, Richard Petersens Plads, Bldg. 322, DK-2800 Kgs, Lyngby, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"Winskel G (ed) 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97)","author":"Asarin E","year":"1997"},{"issue":"2","key":"p_2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur R","year":"1994","journal-title":"Theor Comp Sci"},{"key":"p_3","volume-title":"Wolper P (ed) Computer Aided Verification (CAV '95), vol 939 of Lecture Notes in Computer Science","author":"Bouajjani A","year":"1995"},{"key":"p_4","first-page":"256","volume-title":"Olderog E-R, Steffen B (eds) Correct system design - Recent insights and advances, vol 1710 of Lecture Notes in Computer Science","author":"Fr\u00e4nzle M","year":"1999"},{"key":"p_6","first-page":"168","volume-title":"Jonsson B, Parrow J (eds) Formal techniques in real-time and fault-tolerant systems (FTRTFT '96), vol 1135 of Lecture notes in computer science","author":"Fr\u00e4 M","year":"1996"},{"key":"p_7","volume-title":"Technische Fakult\u00e4t der Christian-Albrechts-Universit\u00e4t Kiel, Germany. Available as Bericht Nr. 9710","author":"Fr\u00e4 M","year":"1997"},{"issue":"3","key":"p_8","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BF01211086","article-title":"Duration calculus: logical foundations","volume":"9","author":"Hansen MR","year":"1997","journal-title":"Formal Aspects Comput"},{"key":"p_9","first-page":"3","volume-title":"Shannon CE, McCarthy J (eds) Automata studies","author":"Kle SC","year":"1956"},{"key":"p_10","volume-title":"Technische Fakult\u00e4t der Christian-Albrechts-Universit\u00e4t Kiel, Germany","author":"Lak Y","year":"1996"},{"key":"p_11","volume-title":"Formal techniques in real-time and fault-tolerant systems (FTRTFT '94), vol 863 of Lecture notes in computer science","author":"Ld H","year":"1994"},{"key":"p_12","volume-title":"Proc. AMS symposium on complexity of computation","author":"Meyer AR","year":"1973"},{"issue":"1","key":"p_14","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/32.210306","article-title":"Specifying and verifying requirements of real-time systems","volume":"19","author":"Ravn AP","year":"1993","journal-title":"IEEE Trans Softw Eng"},{"key":"p_15","first-page":"186","volume-title":"Ravn AP, Rischel H (eds) Formal techniques in real-time and fault-tolerant systems (FTRTFT'98), vol 1486 of Lecture Notes in computer science","author":"Satpathy M","year":"1998"},{"key":"p_16","first-page":"133","volume-title":"Automata on infinite objects. In: van Leeuwen J (ed) Handbook of Theoretical Computer Science, vol B: Formal Models and Semantics","author":"Tho W","year":"1990"},{"key":"p_17","first-page":"1","volume-title":"Meyer EW, Puech C (eds) Symposium on theoretical aspects of computer science (STACS 95), vol 900 of Lecture notes in computer science","author":"Tho W","year":"1995"},{"key":"p_18","volume-title":"Technische Fakult\u00e4t der Christian-Albrechts-Universit\u00e4t Kiel, Germany","author":"Wil T","year":"1994"},{"key":"p_19","first-page":"694","volume-title":"Langmaack et al (eds)","author":"Wil T"},{"issue":"5","key":"p_20","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","article-title":"A calculus of durations","volume":"40","author":"Chaochen Z","year":"1991","journal-title":"Inf Process Lett"},{"key":"p_21","first-page":"58","volume-title":"Enjalbert P, Finkel A, Wagner KW (eds) Symposium on theoretical aspects of computer science (STACS 93), vol 665 of Lecture notes in computer science","author":"Chaochen Z","year":"1993"},{"key":"p_22","first-page":"86","volume-title":"Langmaack et al (eds)","author":"Chaochen Z"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0032-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0032-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0032-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:34:00Z","timestamp":1641483240000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0032-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,5]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,5]]}},"alternative-id":["10.1007\/s00165-004-0032-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0032-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,5]]}}}