{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:19Z","timestamp":1761611299763},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616481"},{"type":"electronic","value":"9783540706533"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61648-9_48","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:09:47Z","timestamp":1330276187000},"page":"306-326","source":"Crossref","is-referenced-by-count":11,"title":["Model checking for extended timed temporal logics"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yassine","family":"Lakhnech","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Yovine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In LICS'90. IEEE, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and D. Dill. A Theory of Timed Automata. TCS, 126, 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, T. Feder, and T. Henzinger. The Benefits of Relaxing Punctuality. In PODC'91, 1991.","DOI":"10.1145\/112600.112613"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger. A Really Temporal Logic. In FOCS'89. IEEE, 1989.","DOI":"10.1109\/SFCS.1989.63473"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger. Back to the Future: Towards a Theory of Timed Regular Languages. In FOCS'92. IEEE, 1992.","DOI":"10.1109\/SFCS.1992.267774"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"D. Bosscher, I. Polak, and F. Vaandrager. Verification of an audio control protocol. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, FTRTFT'94: Formal Techniques in Real-Time and Fault-Taulerant Systems, pages 170\u2013192. Lecture Notes in Computer Science 863, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58468-4_165"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"A. Bouajjani and Y. Lakhnech. Temporal Logic + Timed Automata: Expressiveness and Decidability. In CONCUR'95. LNCS 962, 1995.","DOI":"10.1007\/3-540-60218-6_40"},{"key":"18_CR8","volume-title":"Two examples of verification of multirate timed automata with KRONOS","author":"C. Daws","year":"1995","unstructured":"C. Daws and S. Yovine. Two examples of verification of multirate timed automata with KRONOS. In Proc. 1995 IEEE Real-Time Systems Symposium, RTSS'95, Pisa, Italy, December 1995. IEEE Computer Society Press."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"T. Hafer and W. Thomas. Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree. In ICALP'87. LNCS 267, 1987.","DOI":"10.1007\/3-540-18088-5_22"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model-Checking for Real-Time Systems. In LICS'92. IEEE, 1992.","DOI":"10.1109\/LICS.1992.185551"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"P-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In Proc. 7th Computer-Aided Verification, Li\u00e8ge, Belgium, July 1995.","DOI":"10.1007\/3-540-60045-0_64"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The Glory of the Past. In Conf. Logics of Programs. LNCS 193, 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. A Hierarchy of Temporal Properties. In PODC'90. ACM, 1990.","DOI":"10.1145\/93385.93442"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"W. Thomas. Computation Tree Logic and Regular \u03c9-Languages. LNCS 354, 1989.","DOI":"10.1007\/BFb0013041"},{"key":"18_CR15","unstructured":"M.Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. In LICS'86. IEEE, 1986."},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Th. Wilke. Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata. In FTRTFT'94. LNCS 863, 1994.","DOI":"10.1007\/3-540-58468-4_191"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"P. Wolper. Temporal Logic Can Be More Expressive. Inform. and Cont., 56, 1983.","DOI":"10.1016\/S0019-9958(83)80051-5"}],"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_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:09:03Z","timestamp":1605629343000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61648-9_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616481","9783540706533"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-61648-9_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}