{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,1]],"date-time":"2023-04-01T08:51:08Z","timestamp":1680339068019},"reference-count":30,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2001,4,1]],"date-time":"2001-04-01T00:00:00Z","timestamp":986083200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4490,"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":[[2001,4]]},"DOI":"10.1016\/s0304-3975(00)00101-8","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T21:51:54Z","timestamp":1027633914000},"page":"31-62","source":"Crossref","is-referenced-by-count":18,"title":["Decidability of model checking with the temporal logic EF"],"prefix":"10.1016","volume":"256","author":[{"given":"Richard","family":"Mayr","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00101-8_BIB1","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","article-title":"Algebra of communicating processes with abstraction","volume":"37","author":"Bergstra","year":"1985","journal-title":"Theoret. Comput. Sci. (TCS)"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB2","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, O. Maler, Reachability analysis of pushdown automata: application to model checking, in: Internat. Conf. on Concurrency Theory (CONCUR\u201997), Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB3","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, P. Habermehl, Constrained properties, semilinear systems, and Petri nets, in: Ugo Montanari, Vladimiro Sassone (Eds.), Proc. CONCUR\u201996, Lecture Notes in Computer Science, Vol. 1119, Springer, Berlin, 1996.","DOI":"10.1007\/3-540-61604-7_71"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB4","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, R. Mayr, Model checking lossy vector addition systems, in: Proc. STACS\u201999, Lecture Notes in Computer Science, Vol. 1563, Springer, Berlin, 1999.","DOI":"10.1007\/3-540-49116-3_30"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB5","series-title":"Verifying Temporal Properties of Systems","author":"Bradfield","year":"1992"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB6","doi-asserted-by":"crossref","unstructured":"O. Burkart, D. Caucal, B. Steffen (Eds.), Bisimulation collapse and the process taxonomy, in: U. Montanari, V. Sassone, Proc. CONCUR\u201996, Lecture Notes in Computer Science, Vol. 1119, Springer, Berlin, 1996.","DOI":"10.1007\/3-540-61604-7_59"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB7","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(05)80680-2","article-title":"More infinite results","volume":"5","author":"Burkart","year":"1997","journal-title":"Electron. Notes Theoret. Comput. Sci. (ENTCS)"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB8","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","article-title":"On the regular structure of prefix rewriting","volume":"106","author":"Caucal","year":"1992","journal-title":"J. Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00101-8_BIB9","unstructured":"S. Christensen, Decidability and decomposition in process algebras, Ph.D. Thesis, Edinburgh University, 1993."},{"key":"10.1016\/S0304-3975(00)00101-8_BIB10","doi-asserted-by":"crossref","unstructured":"J. Esparza, On the decidability of model checking for several \u03bc-calculi and Petri nets, in: Trees in Algebra and Programming \u2013 CAAP\u201994, Lecture Notes in Computer Science, Vol. 787, Springer, Berlin, 1994.","DOI":"10.1007\/BFb0017477"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB11","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s002360050074","article-title":"Decidability of model checking for infinite-state concurrent systems","volume":"34","author":"Esparza","year":"1997","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(00)00101-8_BIB12","first-page":"353","article-title":"On the model checking problem for branching time logics and Basic Parallel Processes","volume":"Vol. 939","author":"Esparza","year":"1995"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB13","doi-asserted-by":"crossref","unstructured":"P. Jan\u010dar, Decidability questions for bisimilarity of Petri nets and some related problems, in: Proc. STACS\u201994, Lecture Notes in Computer Science, Vol. 775, Springer, Berlin, 1994.","DOI":"10.1007\/3-540-57785-8_173"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB14","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0304-3975(95)00037-W","article-title":"Undecidability of bisimilarity for Petri nets and some related problems","volume":"148","author":"Jan\u010dar","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00101-8_BIB15","doi-asserted-by":"crossref","unstructured":"P. Jan\u010dar, A. Ku\u010dera, R. Mayr, Deciding bisimulation-like equivalences with finite-state processes, in: Proc. ICALP\u201998, Lecture Notes in Computer Science, Vol. 1443, Springer, Berlin, 1998.","DOI":"10.1007\/BFb0055053"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB16","unstructured":"A. Kucera, Regularity is decidable for normed PA Processes in polynomial time, in: foundations of Software Technology and Theoretical Computer Science (FST&TCS\u201996), Lecture Notes in Computer Science, Vol. 1180, Springer, Berlin, 1996."},{"key":"10.1016\/S0304-3975(00)00101-8_BIB17","doi-asserted-by":"crossref","unstructured":"D. Lugiez, Ph. Schnoebelen, The regular viewpoint on PA-processes, in: Proc. CONCUR\u201998, Lecture Notes in Computer Science, Vol. 1466, Springer, Berlin, 1998.","DOI":"10.1007\/BFb0055615"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB18","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1006\/inco.1999.2826","article-title":"Process rewrite systems","volume":"156","author":"Mayr","year":"2000","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(00)00101-8_BIB19","doi-asserted-by":"crossref","unstructured":"R. Mayr, Weak bisimulation and model checking for Basic Parallel Processes, in: Foundations of Software Technology and Theoretical Computer Science (FST&TCS\u201996), Lecture Notes in Computer Science, Vol. 1180, Springer, Berlin, 1996.","DOI":"10.1007\/3-540-62034-6_40"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB20","doi-asserted-by":"crossref","unstructured":"R. Mayr, Combining Petri nets and PA-processes, in: M. Abadi, Takayasu Ito (Eds.), Internat. Symp. on Theoretical Aspects of Computer Software (TACS\u201997), Lecture Notes in Computer Science, Vol. 1281, Springer, Berlin, 1997.","DOI":"10.1007\/BFb0014567"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB21","doi-asserted-by":"crossref","unstructured":"R. Mayr, Model checking PA-processes, in: Internat. Conf. on Concurrency Theory (CONCUR\u201997), Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997.","DOI":"10.1007\/3-540-63141-0_23"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB22","doi-asserted-by":"crossref","unstructured":"R. Mayr, Process rewrite systems, Electron. Notes Theoret. Comput. Sci. (ENTCS) 7 (1997), Proc. Expressiveness in Concurrency (EXPRESS\u201997).","DOI":"10.1016\/S1571-0661(05)80473-6"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB23","unstructured":"R. Mayr, Decidability and complexity of model checking problems for infinite-state systems, Ph.D. Thesis, TU-M\u00fcnchen, 1998."},{"key":"10.1016\/S0304-3975(00)00101-8_BIB24","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(05)80256-7","article-title":"Strict lower bounds for model checking BPA","volume":"18","author":"Mayr","year":"1998","journal-title":"Electron. Notes Theoret. Comput. Sci. (ENTCS)"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB25","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB26","doi-asserted-by":"crossref","unstructured":"F. Moller, Infinite Results, in: Ugo Montanari, Vladimiro Sassone (Eds.), Proc. CONCUR\u201996, Lecture Notes in Computer Science, Vol. 1119, Springer, Berlin, 1996.","DOI":"10.1007\/3-540-61604-7_56"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB27","series-title":"The temporal logic of programs, in: FOCS\u201977","author":"Pnueli","year":"1977"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB28","unstructured":"Ph. Schnoebelen, Decomposable and regular languages and the shuffle operator, in: EATCS Bulletin, Vol. 67, European Association of Theoretical Computer Science, February, 1999."},{"key":"10.1016\/S0304-3975(00)00101-8_BIB29","doi-asserted-by":"crossref","unstructured":"I. Walukiewicz, Pushdown processes: games and model checking, in: Internat. Conf. on Computer Aided Verification (CAV\u201996), Lecture Notes in Computer Science, Vol. 1102, Springer, Berlin, 1996.","DOI":"10.1007\/3-540-61474-5_58"},{"key":"10.1016\/S0304-3975(00)00101-8_BIB30","doi-asserted-by":"crossref","unstructured":"I. Walukiewicz, Pushdown processes: games and model checking, Technical Report RS-96-54, BRICS, Aarhus, Denmark, 1996, Longer version of a CAV\u201996 paper.","DOI":"10.7146\/brics.v3i54.20057"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500001018?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500001018?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T21:00:11Z","timestamp":1555707611000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500001018"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,4]]},"references-count":30,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2001,4]]}},"alternative-id":["S0304397500001018"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00101-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,4]]}}}