{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T23:19:55Z","timestamp":1648595995080},"reference-count":41,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,6,1]],"date-time":"2003-06-01T00:00:00Z","timestamp":1054425600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3735,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,6]]},"DOI":"10.1016\/s0304-3975(02)00447-4","type":"journal-article","created":{"date-parts":[[2003,5,13]],"date-time":"2003-05-13T04:04:58Z","timestamp":1052798698000},"page":"103-133","source":"Crossref","is-referenced-by-count":2,"title":["On temporal logic versus datalog"],"prefix":"10.1016","volume":"303","author":[{"given":"Ir\u00e8ne","family":"Guessarian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eug\u00e9nie","family":"Foustoucos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Theodore","family":"Andronikos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Foto","family":"Afrati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(02)00447-4_BIB1","series-title":"Foundations of Databases","author":"Abiteboul","year":"1995"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB2","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1023\/A:1004275029985","article-title":"Modal languages and bounded fragments of predicate logic","volume":"27","author":"Andreka","year":"1998","journal-title":"J. Philos. Logic"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB3","series-title":"Finite Transition Systems, Semantics of communicating systems, C.A.R. Hoare International series","author":"Arnold","year":"1994"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB4","article-title":"Rudiments of \u03bc-calculus","volume":"Vol. 146","author":"Arnold","year":"2001"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB5","first-page":"341","article-title":"Fixpoint alternation: arithmetic, transition systems, and the binary tree","volume":"33","author":"Bradfield","year":"1999","journal-title":"in: Theoretical Informatics and Applications"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB6","series-title":"Handbook of Process Algebra","first-page":"293","article-title":"Modal logics and \u03bc-calculi: an introduction","author":"Bradfield","year":"2001"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB7","series-title":"TACAS\u201998, Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/BFb0054183","article-title":"Set-based analysis of reactive infinite-state systems","author":"Charatonik","year":"1998"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB8","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM TOPLAS, Vol. 8, 1986, pp. 244\u2013263.","DOI":"10.1145\/5397.5399"},{"issue":"2","key":"10.1016\/S0304-3975(02)00447-4_BIB9","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1023\/A:1005732517165","article-title":"Toupie","volume":"19","author":"Corsini","year":"1997","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB10","series-title":"Logic programming and model checking, in PLAP\/ALP\u201998","first-page":"1","volume":"Vol. 85","year":"1998"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB11","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","article-title":"CTL* and ECTL* as fragments of the modal \u03bc-calculus","volume":"126","author":"Dam","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB12","first-page":"997","article-title":"Temporal and modal logic","volume":"2","author":"Emerson","year":"1990","journal-title":"Handbook of Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB13","series-title":"Descriptive Complexity and Finite Models","article-title":"Model checking and the \u03bc-calculus","author":"Emerson","year":"1997"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB14","series-title":"ICALP\u201980","first-page":"169","article-title":"Characterizing correctness properties of parallel programs using fixpoints","volume":"Vol. 85","author":"Emerson","year":"1980"},{"issue":"1","key":"10.1016\/S0304-3975(02)00447-4_BIB15","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"Sometimes and not never revisited","volume":"33","author":"Emerson","year":"1986","journal-title":"J. Assoc. Comput."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB16","unstructured":"E.A. Emerson, C.L. Lei, Efficient model checking in fragments of the propositional \u03bc-calculus, in: Proceedings of the First Symposium on Logic in Computer Science, 1986, pp. 267\u2013278."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB17","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, C.L. Lei, Modalities for model checking: branching time logic strikes back, Sci. Comput. Programming (1987) 275\u2013306.","DOI":"10.1016\/0167-6423(87)90036-0"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0743-1066(87)90018-5","article-title":"A note on the complexity of the satisfiability of modal Horn clauses","volume":"4","author":"Fari\u00f1as del Cerro","year":"1987","journal-title":"Logic Programming"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB19","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/504077.504079","article-title":"Datalog LITE","volume":"3","author":"Gottlob","year":"2002","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB20","series-title":"Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree, ICALP\u201987","first-page":"269","volume":"Vol. 267","year":"1987"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB21","series-title":"CAV\u201997","first-page":"291","article-title":"Model checking and transitive-closure logic","volume":"Vol. 1254","author":"Immermann","year":"1997"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB22","doi-asserted-by":"crossref","unstructured":"D. Janin, G. Lenzi, Relating levels of the \u03bc-calculus hierarchy with levels of the monadic hierarchy, in: LICS\u201901, IEEE Press, New York, 2001.","DOI":"10.1109\/LICS.2001.932510"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB23","unstructured":"D. Janin, I. Walukiewicz, On the expressive completeness of the propositional \u03bc-calculus with respect to the monadic second order logic, in CONCUR\u201996, Lecture Notes in Computer Science, Vol. 1119, Springer, Berlin, pp. 263\u2013277."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB24","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional \u03bc-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"10.1016\/S0304-3975(02)00447-4_BIB25","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","article-title":"An automata-theoretic approach to branching-time model checking","volume":"47","author":"Kupferman","year":"2000","journal-title":"JACM"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB26","doi-asserted-by":"crossref","unstructured":"L. Lamport, Sometimes is sometimes \u201cnot never\u201d-on the temporal logic of programs, in: Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, 1980, pp. 174\u2013185.","DOI":"10.1145\/567446.567463"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB27","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1992"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB28","doi-asserted-by":"crossref","unstructured":"F. Moller, A. Rabinovich, On the expressive power of CTL*, in: Proceedings of the LICS\u201999, Trento, Italy, 1999.","DOI":"10.1109\/LICS.1999.782631"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB29","unstructured":"L.A. Nguyen, The Modal Query Language MDatalog, Fundamenta Informaticae, http:\/\/www.mimuw.edu.pl\/~nguyen\/, 2001, submitted for publication."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(97)00039-X","article-title":"Fixed point characterization of infinite behavior of finite-state systems, TCS Fundamental Study","volume":"189","author":"Niwi\u0144ski","year":"1997","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB31","unstructured":"D. Park, Fixpoint induction and proof of program semantics, in: Machine Intelligence, Vol. 5, Edinburgh University Press (1969) 59\u201378."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB32","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, in: Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, 1977, pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB33","series-title":"CAV\u201997","first-page":"143","article-title":"Efficient model checking using tabled resolution","volume":"Vol. 1254","author":"Ramakrishnan","year":"1997"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB34","first-page":"133","article-title":"Automata on infinite objects","volume":"1","author":"Thomas","year":"1990","journal-title":"Handbook Theoret. Comput. Sci."},{"issue":"3","key":"10.1016\/S0304-3975(02)00447-4_BIB35","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1145\/3979.3980","article-title":"Implementation of logical query languages for databases","volume":"10","author":"Ullman","year":"1985","journal-title":"ACM Trans. Database Systems"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB36","series-title":"Database and Knowledge-Base Systems, Vols. I and II","author":"Ullman","year":"1989"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB37","unstructured":"M. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, Proceedings of the First Symposium on Logic in Computer Science, 1986, pp. 322\u2013331."},{"issue":"1","key":"10.1016\/S0304-3975(02)00447-4_BIB38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning about infinite computation","volume":"115","author":"Vardi","year":"1994","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB39","unstructured":"T. Wilke, CTL+ is exponentially more succinct than CTL,in: Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science,Lecture Notes in Computer Science, Vol. 1738, Springer, Berlin, pp. 110\u2013121."},{"key":"10.1016\/S0304-3975(02)00447-4_BIB40","doi-asserted-by":"crossref","unstructured":"P. Wolper, Temporal logic can be more expressive, in: Proceedings of the 22nd IEEE Symposium on Foundations of Computer Science, 1981, pp. 340\u2013348.","DOI":"10.1109\/SFCS.1981.44"},{"key":"10.1016\/S0304-3975(02)00447-4_BIB41","doi-asserted-by":"crossref","unstructured":"P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, in: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, Tucson, 1983, pp. 185\u2013194.","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502004474?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502004474?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T12:52:35Z","timestamp":1553172755000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397502004474"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,6]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,6]]}},"alternative-id":["S0304397502004474"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(02)00447-4","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2003,6]]}}}