{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:46:50Z","timestamp":1762458410910,"version":"build-2065373602"},"reference-count":13,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,10,1]],"date-time":"2003-10-01T00:00:00Z","timestamp":1064966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2003,10,1]],"date-time":"2003-10-01T00:00:00Z","timestamp":1064966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3589,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,10]]},"DOI":"10.1016\/s1571-0661(04)81050-8","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"210-225","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":24,"title":["Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems"],"prefix":"10.1016","volume":"89","author":[{"given":"K\u00e5re Jelling","family":"Kristoffersen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Pedersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrik Reif","family":"Andersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB1","doi-asserted-by":"crossref","unstructured":"K. Havelund, G. Ruso. Monitoring Java Programs with Java PathExplorer. First Workshop on Runtime Verification (RV'01), Paris, France, 23 July 2001. Electronic Notes in Theoretical Computer Science, Volume 55, Number 2, 2001","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB2","unstructured":"D. Giannakopoulou, K. Havelund. Automata-Based Verification of Temporal Properties on Running Programs. Automated Software Engineering 2001 (ASE'01), San Diego, California, 26\u201329 November 2001, IEEE Computer Society."},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB3","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple onthe -fly automatic verification of linear temporal logic. Proc. 15th International Symposium on Protocol Specification, Testing and Verification (PSTV XV), pp 318, Chapman and Hall, 1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"No. 5","key":"10.1016\/S1571-0661(04)81050-8_NEWBIB4","first-page":"279","article-title":"The Model Checker SPIN. IEEE Trans. on Software Engineering","volume":"23","author":"Holzmann","year":"1997","journal-title":"Vol."},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB5","article-title":"Temporal Business Solutions","author":"Corp","year":"2000","journal-title":"The DB Rover"},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB6","series-title":"Logics and Models of Real Time: A Survey. Real Time: Theory in Practice, Lecture Notes in Computer Science 600","first-page":"74","author":"Alur","year":"1992"},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB7","doi-asserted-by":"crossref","unstructured":"T. Henzinger. It's About Time: Real-Time Logics Reviewed. Proceedings of the Ninth International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 1466, Springer-Verlag, 1998, pp. 439\u2013454.","DOI":"10.1007\/BFb0055640"},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB8","unstructured":"K. Havelund, G. Ruso. Monitoring Programs using Rewriting. Automated Software Engineering 2001 (ASE'01), San Diego, California, 26\u201329 November 2001, IEEE Computer Society."},{"year":"2001","series-title":"Model Checking","author":"Clarke","key":"10.1016\/S1571-0661(04)81050-8_NEWBIB9"},{"journal-title":"Three Events that Defines an REA Methodology for Systems Analysis, Design and Implementation","year":"2001","author":"David","key":"10.1016\/S1571-0661(04)81050-8_NEWBIB10"},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB11","unstructured":"K. G. Larsen, P. Pettersson and W. Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. Proceedings of the 16th IEEE Real-Time Systems Symposium, Pisa, Italy, 5\u20137 December, 1995."},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB12","doi-asserted-by":"crossref","unstructured":"H. R. Andersen. Partial Model Checking (Extended Abstract). Proceedings of LICS'95. La Jolla, San Diego, June 26\u201329, 1995, IEEE Computer Society Press, pp. 398\u2013407.","DOI":"10.1109\/LICS.1995.523274"},{"key":"10.1016\/S1571-0661(04)81050-8_NEWBIB13","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A Lattice-Theoretical Fixpoint Theorem and its Applications","volume":"55","author":"Tarski","year":"1955","journal-title":"Pacific. J. Math."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104810508?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104810508?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:07:01Z","timestamp":1761610021000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104810508"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,10]]},"references-count":13,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,10]]}},"alternative-id":["S1571066104810508"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)81050-8","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2003,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)81050-8","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2003 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}