{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:29:29Z","timestamp":1725564569696},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208037"},{"type":"electronic","value":"9783540246220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_12","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T11:33:53Z","timestamp":1283686433000},"page":"122-134","source":"Crossref","is-referenced-by-count":1,"title":["Checking Interval Based Properties for Reactive Systems"],"prefix":"10.1007","author":[{"given":"Pei","family":"Yu","sequence":"first","affiliation":[]},{"given":"Xu","family":"Qiwen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","volume-title":"Logic, Methodology and Philosophy of Science","author":"J.R. Buchi","year":"1960","unstructured":"Buchi, J.R.: On a Decision Method in Restricted Second Order Arithmetic. In: Nagel, et al. (eds.) Logic, Methodology and Philosophy of Science, Stanford Univ. Press, Stanford (1960)"},{"key":"12_CR2","unstructured":"Alpern, B., Schneider, F.B.: Recognizing Safety and Liveness. TR 86\u2013727 (1986)"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining Liveness. Information Processing Letters\u00a021, 181\u2013185 (1985)","journal-title":"Information Processing Letters"},{"key":"12_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BF01211086","volume":"9","author":"M.R. Hansen","year":"1997","unstructured":"Hansen, M.R., Chaochen, Z.: Duration Calculus: Logical Foundations. Formal Aspects of Computing\u00a09, 283\u2013330 (1997)","journal-title":"Formal Aspects of Computing"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1996","unstructured":"Henriksen, J.G., Jensen, J., Jorgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic Second-order Logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, Springer, Heidelberg (1996)"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The SPIN Model Checker. IEEE Trans. on Software Engineering\u00a023, 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"12_CR8","unstructured":"The Grail+ Project. Department of Computer Science, University of Western Ontario, Canada, http:\/\/www.csd.uwo.ca\/research\/grail\/"},{"issue":"2","key":"12_CR9","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering\u00a0SE-3(2), 125\u2013143 (1977)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"12_CR10","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B. Moszkowski","year":"1985","unstructured":"Moszkowski, B.: A Temporal Logic for Multilevel Reasoning about Hardware. IEEE Computer\u00a018(2), 10\u201319 (1985)","journal-title":"IEEE Computer"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1109\/ICECCS.1995.479336","volume-title":"Proc. of the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 1995)","author":"B. Moszkowski","year":"1995","unstructured":"Moszkowski, B.: Compositional reasoning about projected and infinite time. In: Proc. of the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 1995), pp. 238\u2013245. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"12_CR12","unstructured":"Pandya, P.K.: Specifying and Deciding Quantified Discrete-Time Duration Calculus Formulae using DCVALID. In: Proc. of Workshop on Real-time Tools, Aalborg, Denmark (2001), TCS00-PKP-1, Tata Institute of Fundamental Research, Mumbai, India (2000)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/3-540-45319-9_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.K. Pandya","year":"2001","unstructured":"Pandya, P.K.: Model checking CTL[DC]. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 559. Springer, Heidelberg (2001)"},{"issue":"1&2","key":"12_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(96)80701-8","volume":"166","author":"Y.S. Ramakrishna","year":"1996","unstructured":"Ramakrishna, Y.S., Melliar-Smith, P.M., Moser, L.E., Dillon, L.K., Kuttys, G.: Interval Logics and Their Decision Procedures, Part I: An Interval Logic. Theoretical Computer Science\u00a0166(1&2), 1\u201347 (1996)","journal-title":"Theoretical Computer Science"},{"key":"12_CR15","unstructured":"Skakkeb\u00e6k, J.U.: A Verification Assistant for Real-time Logic. PhD. Thesis, Department of Computer Science, Technical University of Denmark (1994)"},{"key":"12_CR16","unstructured":"Hanpin, W., Qiwen, X.: Completeness of temporal logics over infinite intervals. Technical Report 158, UNU\/IIST, Macau, Accepted by Applied Discrete Mathematics, Elsevier (1999)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-44667-2_7","volume-title":"Lectures on Formal Methods and Performance Analysis","author":"P. Wolper","year":"2001","unstructured":"Wolper, P.: Constructing automata from temporal logic formula: a tutorial. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol.\u00a02090, pp. 261\u2013277. Springer, Heidelberg (2001)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Yu, P., Qiwen, X.: Checking Interval Based Properties for Reactive Systems. Technical Report 283, UNU\/IIST, Macau. (2003)","DOI":"10.1007\/978-3-540-24622-0_12"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/3-540-60249-6_39","volume-title":"Fundamentals of Computation Theory","author":"Z. Chaochen","year":"1995","unstructured":"Chaochen, Z., Van Hung, D., Xiaoshan, L.: A Duration Calculus with Infinite Intervals. In: Reichel, H. (ed.) FCT 1995. LNCS, vol.\u00a0965, pp. 16\u201341. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24622-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T17:41:08Z","timestamp":1559583668000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}